Step | Hyp | Ref
| Expression |
1 | | cplpq 6253 |
. 2
class
+_{pQ} |
2 | | vx |
. . 3
setvar x |
3 | | vy |
. . 3
setvar y |
4 | | cnpi 6249 |
. . . 4
class
N |
5 | 4, 4 | cxp 4285 |
. . 3
class (N ×
N) |
6 | 2 | cv 1241 |
. . . . . . 7
class x |
7 | | c1st 5704 |
. . . . . . 7
class
1^{st} |
8 | 6, 7 | cfv 4844 |
. . . . . 6
class (1^{st}
‘x) |
9 | 3 | cv 1241 |
. . . . . . 7
class y |
10 | | c2nd 5705 |
. . . . . . 7
class
2^{nd} |
11 | 9, 10 | cfv 4844 |
. . . . . 6
class (2^{nd}
‘y) |
12 | | cmi 6251 |
. . . . . 6
class
·_{N} |
13 | 8, 11, 12 | co 5452 |
. . . . 5
class ((1^{st}
‘x)
·_{N} (2^{nd} ‘y)) |
14 | 9, 7 | cfv 4844 |
. . . . . 6
class (1^{st}
‘y) |
15 | 6, 10 | cfv 4844 |
. . . . . 6
class (2^{nd}
‘x) |
16 | 14, 15, 12 | co 5452 |
. . . . 5
class ((1^{st}
‘y)
·_{N} (2^{nd} ‘x)) |
17 | | cpli 6250 |
. . . . 5
class
+_{N} |
18 | 13, 16, 17 | co 5452 |
. . . 4
class (((1^{st}
‘x)
·_{N} (2^{nd} ‘y)) +_{N} ((1^{st}
‘y)
·_{N} (2^{nd} ‘x))) |
19 | 15, 11, 12 | co 5452 |
. . . 4
class ((2^{nd}
‘x)
·_{N} (2^{nd} ‘y)) |
20 | 18, 19 | cop 3369 |
. . 3
class ⟨(((1^{st}
‘x)
·_{N} (2^{nd} ‘y)) +_{N} ((1^{st}
‘y)
·_{N} (2^{nd} ‘x))), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩ |
21 | 2, 3, 5, 5, 20 | cmpt2 5454 |
. 2
class (x ∈
(N × N), y ∈
(N × N) ↦ ⟨(((1^{st}
‘x)
·_{N} (2^{nd} ‘y)) +_{N} ((1^{st}
‘y)
·_{N} (2^{nd} ‘x))), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) |
22 | 1, 21 | wceq 1242 |
1
wff +_{pQ}
= (x ∈
(N × N), y ∈
(N × N) ↦ ⟨(((1^{st}
‘x)
·_{N} (2^{nd} ‘y)) +_{N} ((1^{st}
‘y)
·_{N} (2^{nd} ‘x))), ((2^{nd} ‘x) ·_{N}
(2^{nd} ‘y))⟩) |