Step | Hyp | Ref
| Expression |
1 | | cplpq 9923 |
. 2
class
+_{pQ} |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cnpi 9919 |
. . . 4
class
N |
5 | 4, 4 | cxp 5275 |
. . 3
class
(N × N) |
6 | 2 | cv 1651 |
. . . . . . 7
class 𝑥 |
7 | | c1st 7364 |
. . . . . . 7
class
1^{st} |
8 | 6, 7 | cfv 6068 |
. . . . . 6
class
(1^{st} ‘𝑥) |
9 | 3 | cv 1651 |
. . . . . . 7
class 𝑦 |
10 | | c2nd 7365 |
. . . . . . 7
class
2^{nd} |
11 | 9, 10 | cfv 6068 |
. . . . . 6
class
(2^{nd} ‘𝑦) |
12 | | cmi 9921 |
. . . . . 6
class
·_{N} |
13 | 8, 11, 12 | co 6842 |
. . . . 5
class
((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦)) |
14 | 9, 7 | cfv 6068 |
. . . . . 6
class
(1^{st} ‘𝑦) |
15 | 6, 10 | cfv 6068 |
. . . . . 6
class
(2^{nd} ‘𝑥) |
16 | 14, 15, 12 | co 6842 |
. . . . 5
class
((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥)) |
17 | | cpli 9920 |
. . . . 5
class
+_{N} |
18 | 13, 16, 17 | co 6842 |
. . . 4
class
(((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦))
+_{N} ((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥))) |
19 | 15, 11, 12 | co 6842 |
. . . 4
class
((2^{nd} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦)) |
20 | 18, 19 | cop 4340 |
. . 3
class
⟨(((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦))
+_{N} ((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩ |
21 | 2, 3, 5, 5, 20 | cmpt2 6844 |
. 2
class (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨(((1^{st}
‘𝑥)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |
22 | 1, 21 | wceq 1652 |
1
wff
+_{pQ} = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨(((1^{st}
‘𝑥)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |