Step | Hyp | Ref
| Expression |
1 | | fveq2 6545 |
. . . . 5
⊢ (𝑥 = 𝐴 → (1^{st} ‘𝑥) = (1^{st} ‘𝐴)) |
2 | 1 | oveq1d 7038 |
. . . 4
⊢ (𝑥 = 𝐴 → ((1^{st} ‘𝑥)
·_{N} (2^{nd} ‘𝑦)) = ((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝑦))) |
3 | | fveq2 6545 |
. . . . 5
⊢ (𝑥 = 𝐴 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝐴)) |
4 | 3 | oveq2d 7039 |
. . . 4
⊢ (𝑥 = 𝐴 → ((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥)) = ((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝐴))) |
5 | 2, 4 | oveq12d 7041 |
. . 3
⊢ (𝑥 = 𝐴 → (((1^{st} ‘𝑥)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥))) = (((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝐴)))) |
6 | 3 | oveq1d 7038 |
. . 3
⊢ (𝑥 = 𝐴 → ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦)) = ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝑦))) |
7 | 5, 6 | opeq12d 4724 |
. 2
⊢ (𝑥 = 𝐴 → ⟨(((1^{st} ‘𝑥)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩ = ⟨(((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝑦))⟩) |
8 | | fveq2 6545 |
. . . . 5
⊢ (𝑦 = 𝐵 → (2^{nd} ‘𝑦) = (2^{nd} ‘𝐵)) |
9 | 8 | oveq2d 7039 |
. . . 4
⊢ (𝑦 = 𝐵 → ((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝑦)) = ((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) |
10 | | fveq2 6545 |
. . . . 5
⊢ (𝑦 = 𝐵 → (1^{st} ‘𝑦) = (1^{st} ‘𝐵)) |
11 | 10 | oveq1d 7038 |
. . . 4
⊢ (𝑦 = 𝐵 → ((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝐴)) = ((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))) |
12 | 9, 11 | oveq12d 7041 |
. . 3
⊢ (𝑦 = 𝐵 → (((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝐴))) = (((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)))) |
13 | 8 | oveq2d 7039 |
. . 3
⊢ (𝑦 = 𝐵 → ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝑦)) = ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))) |
14 | 12, 13 | opeq12d 4724 |
. 2
⊢ (𝑦 = 𝐵 → ⟨(((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝑦))⟩ = ⟨(((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) |
15 | | df-plpq 10183 |
. 2
⊢
+_{pQ} = (𝑥 ∈ (N ×
N), 𝑦 ∈
(N × N) ↦ ⟨(((1^{st}
‘𝑥)
·_{N} (2^{nd} ‘𝑦)) +_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |
16 | | opex 5255 |
. 2
⊢
⟨(((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ ∈ V |
17 | 7, 14, 15, 16 | ovmpo 7173 |
1
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 +_{pQ} 𝐵) = ⟨(((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) |