Step | Hyp | Ref
| Expression |
1 | | addasspi 9998 |
. . . . . . . 8
⊢
((((1^{st} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((1^{st} ‘𝐶) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))) = (((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))))) |
2 | | ovex 6902 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ V |
3 | | ovex 6902 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ V |
4 | | fvex 6417 |
. . . . . . . . . . 11
⊢
(2^{nd} ‘𝐶) ∈ V |
5 | | mulcompi 9999 |
. . . . . . . . . . 11
⊢ (𝑥
·_{N} 𝑦) = (𝑦 ·_{N} 𝑥) |
6 | | distrpi 10001 |
. . . . . . . . . . 11
⊢ (𝑥
·_{N} (𝑦 +_{N} 𝑧)) = ((𝑥 ·_{N} 𝑦) +_{N}
(𝑥
·_{N} 𝑧)) |
7 | 2, 3, 4, 5, 6 | caovdir 7094 |
. . . . . . . . . 10
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
·_{N} (2^{nd} ‘𝐶)) = ((((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
(2^{nd} ‘𝐶))
+_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐶))) |
8 | | mulasspi 10000 |
. . . . . . . . . . 11
⊢
(((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (2^{nd} ‘𝐶)) = ((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
9 | 8 | oveq1i 6880 |
. . . . . . . . . 10
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (2^{nd} ‘𝐶)) +_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐶)))
= (((1^{st} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐶))) |
10 | 7, 9 | eqtri 2828 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
·_{N} (2^{nd} ‘𝐶)) = (((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐶))) |
11 | 10 | oveq1i 6880 |
. . . . . . . 8
⊢
(((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) = ((((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐶))) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) |
12 | | ovex 6902 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ V |
13 | | ovex 6902 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ V |
14 | | fvex 6417 |
. . . . . . . . . . 11
⊢
(2^{nd} ‘𝐴) ∈ V |
15 | 12, 13, 14, 5, 6 | caovdir 7094 |
. . . . . . . . . 10
⊢
((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴)) = ((((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) ·_{N}
(2^{nd} ‘𝐴))
+_{N} (((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (2^{nd} ‘𝐴))) |
16 | | fvex 6417 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝐵) ∈ V |
17 | | mulasspi 10000 |
. . . . . . . . . . . 12
⊢ ((𝑥
·_{N} 𝑦) ·_{N} 𝑧) = (𝑥 ·_{N} (𝑦
·_{N} 𝑧)) |
18 | 16, 4, 14, 5, 17 | caov32 7087 |
. . . . . . . . . . 11
⊢
(((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
·_{N} (2^{nd} ‘𝐴)) = (((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐶)) |
19 | | mulasspi 10000 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (2^{nd} ‘𝐴)) = ((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))) |
20 | | mulcompi 9999 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
= ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)) |
21 | 20 | oveq2i 6881 |
. . . . . . . . . . . 12
⊢
((1^{st} ‘𝐶) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))) = ((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))) |
22 | 19, 21 | eqtri 2828 |
. . . . . . . . . . 11
⊢
(((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (2^{nd} ‘𝐴)) = ((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))) |
23 | 18, 22 | oveq12i 6882 |
. . . . . . . . . 10
⊢
((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
·_{N} (2^{nd} ‘𝐴)) +_{N}
(((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
(2^{nd} ‘𝐴)))
= ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) |
24 | 15, 23 | eqtri 2828 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴)) = ((((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴)) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))) |
25 | 24 | oveq2i 6881 |
. . . . . . . 8
⊢
(((1^{st} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) +_{N}
((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴))) = (((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))))) |
26 | 1, 11, 25 | 3eqtr4i 2838 |
. . . . . . 7
⊢
(((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) = (((1^{st} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴))) |
27 | | mulasspi 10000 |
. . . . . . 7
⊢
(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} (2^{nd} ‘𝐶)) = ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
28 | 26, 27 | opeq12i 4600 |
. . . . . 6
⊢
⟨(((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
(2^{nd} ‘𝐶))⟩ = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩ |
29 | | elpqn 10028 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
30 | 29 | 3ad2ant1 1156 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) |
31 | | elpqn 10028 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) |
32 | 31 | 3ad2ant2 1157 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) |
33 | | addpipq2 10039 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 +_{pQ} 𝐵) = ⟨(((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) |
34 | 30, 32, 33 | syl2anc 575 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
+_{pQ} 𝐵) = ⟨(((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) |
35 | | relxp 5328 |
. . . . . . . . 9
⊢ Rel
(N × N) |
36 | | elpqn 10028 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) |
37 | 36 | 3ad2ant3 1158 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) |
38 | | 1st2nd 7442 |
. . . . . . . . 9
⊢ ((Rel
(N × N) ∧ 𝐶 ∈ (N ×
N)) → 𝐶
= ⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩) |
39 | 35, 37, 38 | sylancr 577 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶 =
⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩) |
40 | 34, 39 | oveq12d 6888 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
+_{pQ} 𝐵) +_{pQ} 𝐶) = (⟨(((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ +_{pQ}
⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩)) |
41 | | xp1st 7426 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (N ×
N) → (1^{st} ‘𝐴) ∈ N) |
42 | 30, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐴) ∈ N) |
43 | | xp2nd 7427 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (N ×
N) → (2^{nd} ‘𝐵) ∈ N) |
44 | 32, 43 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐵) ∈ N) |
45 | | mulclpi 9996 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
46 | 42, 44, 45 | syl2anc 575 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
47 | | xp1st 7426 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (N ×
N) → (1^{st} ‘𝐵) ∈ N) |
48 | 32, 47 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐵) ∈ N) |
49 | | xp2nd 7427 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (N ×
N) → (2^{nd} ‘𝐴) ∈ N) |
50 | 30, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐴) ∈ N) |
51 | | mulclpi 9996 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐴)
∈ N) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
52 | 48, 50, 51 | syl2anc 575 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ N) |
53 | | addclpi 9995 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N ∧ ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))
∈ N) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
∈ N) |
54 | 46, 52, 53 | syl2anc 575 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
∈ N) |
55 | | mulclpi 9996 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
56 | 50, 44, 55 | syl2anc 575 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
57 | | xp1st 7426 |
. . . . . . . . 9
⊢ (𝐶 ∈ (N ×
N) → (1^{st} ‘𝐶) ∈ N) |
58 | 37, 57 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐶) ∈ N) |
59 | | xp2nd 7427 |
. . . . . . . . 9
⊢ (𝐶 ∈ (N ×
N) → (2^{nd} ‘𝐶) ∈ N) |
60 | 37, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐶) ∈ N) |
61 | | addpipq 10040 |
. . . . . . . 8
⊢
((((((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴)))
∈ N ∧ ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) ∧ ((1^{st} ‘𝐶) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N)) → (⟨(((1^{st} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ +_{pQ}
⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩) = ⟨(((((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
(2^{nd} ‘𝐶))⟩) |
62 | 54, 56, 58, 60, 61 | syl22anc 858 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (⟨(((1^{st} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
+_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ +_{pQ}
⟨(1^{st} ‘𝐶), (2^{nd} ‘𝐶)⟩) = ⟨(((((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
(2^{nd} ‘𝐶))⟩) |
63 | 40, 62 | eqtrd 2840 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
+_{pQ} 𝐵) +_{pQ} 𝐶) = ⟨(((((1^{st}
‘𝐴)
·_{N} (2^{nd} ‘𝐵)) +_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐴))) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
(2^{nd} ‘𝐶))⟩) |
64 | | 1st2nd 7442 |
. . . . . . . . 9
⊢ ((Rel
(N × N) ∧ 𝐴 ∈ (N ×
N)) → 𝐴
= ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
65 | 35, 30, 64 | sylancr 577 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴 =
⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
66 | | addpipq2 10039 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (N ×
N) ∧ 𝐶
∈ (N × N)) → (𝐵 +_{pQ} 𝐶) = ⟨(((1^{st}
‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩) |
67 | 32, 37, 66 | syl2anc 575 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
+_{pQ} 𝐶) = ⟨(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩) |
68 | 65, 67 | oveq12d 6888 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
+_{pQ} (𝐵 +_{pQ} 𝐶)) = (⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩
+_{pQ} ⟨(((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩)) |
69 | | mulclpi 9996 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
70 | 48, 60, 69 | syl2anc 575 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
71 | | mulclpi 9996 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐶) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
72 | 58, 44, 71 | syl2anc 575 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
73 | | addclpi 9995 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N ∧ ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) → (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
∈ N) |
74 | 70, 72, 73 | syl2anc 575 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
∈ N) |
75 | | mulclpi 9996 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N) → ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
76 | 44, 60, 75 | syl2anc 575 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
77 | | addpipq 10040 |
. . . . . . . 8
⊢
((((1^{st} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐴)
∈ N) ∧ ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
∈ N ∧ ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N)) → (⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ +_{pQ}
⟨(((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
78 | 42, 50, 74, 76, 77 | syl22anc 858 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ +_{pQ}
⟨(((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
79 | 68, 78 | eqtrd 2840 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
+_{pQ} (𝐵 +_{pQ} 𝐶)) = ⟨(((1^{st}
‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} ((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
·_{N} (2^{nd} ‘𝐴))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
80 | 28, 63, 79 | 3eqtr4a 2866 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
+_{pQ} 𝐵) +_{pQ} 𝐶) = (𝐴 +_{pQ} (𝐵 +_{pQ}
𝐶))) |
81 | 80 | fveq2d 6408 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ([Q]‘((𝐴 +_{pQ} 𝐵) +_{pQ}
𝐶)) =
([Q]‘(𝐴
+_{pQ} (𝐵 +_{pQ} 𝐶)))) |
82 | | adderpq 10059 |
. . . 4
⊢
(([Q]‘(𝐴 +_{pQ} 𝐵)) +_{Q}
([Q]‘𝐶)) = ([Q]‘((𝐴 +_{pQ}
𝐵)
+_{pQ} 𝐶)) |
83 | | adderpq 10059 |
. . . 4
⊢
(([Q]‘𝐴) +_{Q}
([Q]‘(𝐵
+_{pQ} 𝐶))) = ([Q]‘(𝐴 +_{pQ}
(𝐵
+_{pQ} 𝐶))) |
84 | 81, 82, 83 | 3eqtr4g 2865 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (([Q]‘(𝐴 +_{pQ} 𝐵)) +_{Q}
([Q]‘𝐶)) = (([Q]‘𝐴) +_{Q}
([Q]‘(𝐵
+_{pQ} 𝐶)))) |
85 | | addpqnq 10041 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
+_{Q} 𝐵) = ([Q]‘(𝐴 +_{pQ}
𝐵))) |
86 | 85 | 3adant3 1155 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
+_{Q} 𝐵) = ([Q]‘(𝐴 +_{pQ}
𝐵))) |
87 | | nqerid 10036 |
. . . . . 6
⊢ (𝐶 ∈ Q →
([Q]‘𝐶)
= 𝐶) |
88 | 87 | eqcomd 2812 |
. . . . 5
⊢ (𝐶 ∈ Q →
𝐶 =
([Q]‘𝐶)) |
89 | 88 | 3ad2ant3 1158 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶 =
([Q]‘𝐶)) |
90 | 86, 89 | oveq12d 6888 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
+_{Q} 𝐵) +_{Q} 𝐶) =
(([Q]‘(𝐴 +_{pQ} 𝐵)) +_{Q}
([Q]‘𝐶))) |
91 | | nqerid 10036 |
. . . . . 6
⊢ (𝐴 ∈ Q →
([Q]‘𝐴)
= 𝐴) |
92 | 91 | eqcomd 2812 |
. . . . 5
⊢ (𝐴 ∈ Q →
𝐴 =
([Q]‘𝐴)) |
93 | 92 | 3ad2ant1 1156 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴 =
([Q]‘𝐴)) |
94 | | addpqnq 10041 |
. . . . 5
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐵
+_{Q} 𝐶) = ([Q]‘(𝐵 +_{pQ}
𝐶))) |
95 | 94 | 3adant1 1153 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
+_{Q} 𝐶) = ([Q]‘(𝐵 +_{pQ}
𝐶))) |
96 | 93, 95 | oveq12d 6888 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
+_{Q} (𝐵 +_{Q} 𝐶)) =
(([Q]‘𝐴) +_{Q}
([Q]‘(𝐵
+_{pQ} 𝐶)))) |
97 | 84, 90, 96 | 3eqtr4d 2850 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
+_{Q} 𝐵) +_{Q} 𝐶) = (𝐴 +_{Q} (𝐵 +_{Q}
𝐶))) |
98 | | addnqf 10051 |
. . . 4
⊢
+_{Q} :(Q ×
Q)⟶Q |
99 | 98 | fdmi 6262 |
. . 3
⊢ dom
+_{Q} = (Q ×
Q) |
100 | | 0nnq 10027 |
. . 3
⊢ ¬
∅ ∈ Q |
101 | 99, 100 | ndmovass 7048 |
. 2
⊢ (¬
(𝐴 ∈ Q
∧ 𝐵 ∈
Q ∧ 𝐶
∈ Q) → ((𝐴 +_{Q} 𝐵) +_{Q}
𝐶) = (𝐴 +_{Q} (𝐵 +_{Q}
𝐶))) |
102 | 97, 101 | pm2.61i 176 |
1
⊢ ((𝐴 +_{Q}
𝐵)
+_{Q} 𝐶) = (𝐴 +_{Q} (𝐵 +_{Q}
𝐶)) |