Step | Hyp | Ref
| Expression |
1 | | mulcompi 9756 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
= ((1^{st} ‘𝐵) ·_{N}
(1^{st} ‘𝐴)) |
2 | 1 | oveq1i 6700 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
= (((1^{st} ‘𝐵) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))) |
3 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(1^{st} ‘𝐵) ∈ V |
4 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(1^{st} ‘𝐴) ∈ V |
5 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(2^{nd} ‘𝐴) ∈ V |
6 | | mulcompi 9756 |
. . . . . . . . . . . . 13
⊢ (𝑥
·_{N} 𝑦) = (𝑦 ·_{N} 𝑥) |
7 | | mulasspi 9757 |
. . . . . . . . . . . . 13
⊢ ((𝑥
·_{N} 𝑦) ·_{N} 𝑧) = (𝑥 ·_{N} (𝑦
·_{N} 𝑧)) |
8 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(2^{nd} ‘𝐶) ∈ V |
9 | 3, 4, 5, 6, 7, 8 | caov411 6908 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐵) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
= (((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
10 | 2, 9 | eqtri 2673 |
. . . . . . . . . . 11
⊢
(((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
= (((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
11 | | mulcompi 9756 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
= ((1^{st} ‘𝐶) ·_{N}
(1^{st} ‘𝐴)) |
12 | 11 | oveq1i 6700 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
= (((1^{st} ‘𝐶) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))) |
13 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(1^{st} ‘𝐶) ∈ V |
14 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(2^{nd} ‘𝐵) ∈ V |
15 | 13, 4, 5, 6, 7, 14 | caov411 6908 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐶) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
= (((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))) |
16 | 12, 15 | eqtri 2673 |
. . . . . . . . . . 11
⊢
(((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))
= (((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐴))
·_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))) |
17 | 10, 16 | oveq12i 6702 |
. . . . . . . . . 10
⊢
((((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} (((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) = ((((2^{nd} ‘𝐴)
·_{N} (1^{st} ‘𝐴)) ·_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((2^{nd} ‘𝐴)
·_{N} (1^{st} ‘𝐴)) ·_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)))) |
18 | | distrpi 9758 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐴))
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))) = ((((2^{nd} ‘𝐴)
·_{N} (1^{st} ‘𝐴)) ·_{N}
((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((2^{nd} ‘𝐴)
·_{N} (1^{st} ‘𝐴)) ·_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)))) |
19 | | mulasspi 9757 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐴) ·_{N}
(1^{st} ‘𝐴))
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))) = ((2^{nd} ‘𝐴)
·_{N} ((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))))) |
20 | 17, 18, 19 | 3eqtr2i 2679 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} (((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))) = ((2^{nd} ‘𝐴)
·_{N} ((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))))) |
21 | | mulasspi 9757 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
= ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))) |
22 | 14, 5, 8, 6, 7 | caov12 6904 |
. . . . . . . . . . 11
⊢
((2^{nd} ‘𝐵) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) = ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))) |
23 | 22 | oveq2i 6701 |
. . . . . . . . . 10
⊢
((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))) = ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)))) |
24 | 21, 23 | eqtri 2673 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
= ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))) |
25 | 20, 24 | opeq12i 4438 |
. . . . . . . 8
⊢
⟨((((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} (((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))⟩ = ⟨((2^{nd}
‘𝐴)
·_{N} ((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))))⟩ |
26 | | elpqn 9785 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) |
27 | 26 | 3ad2ant1 1102 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) |
28 | | xp2nd 7243 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (N ×
N) → (2^{nd} ‘𝐴) ∈ N) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐴) ∈ N) |
30 | | xp1st 7242 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (N ×
N) → (1^{st} ‘𝐴) ∈ N) |
31 | 27, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐴) ∈ N) |
32 | | elpqn 9785 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) |
33 | 32 | 3ad2ant2 1103 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) |
34 | | xp1st 7242 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (N ×
N) → (1^{st} ‘𝐵) ∈ N) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐵) ∈ N) |
36 | | elpqn 9785 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) |
37 | 36 | 3ad2ant3 1104 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) |
38 | | xp2nd 7243 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (N ×
N) → (2^{nd} ‘𝐶) ∈ N) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐶) ∈ N) |
40 | | mulclpi 9753 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
41 | 35, 39, 40 | syl2anc 694 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
42 | | xp1st 7242 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (N ×
N) → (1^{st} ‘𝐶) ∈ N) |
43 | 37, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1^{st} ‘𝐶) ∈ N) |
44 | | xp2nd 7243 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (N ×
N) → (2^{nd} ‘𝐵) ∈ N) |
45 | 33, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2^{nd} ‘𝐵) ∈ N) |
46 | | mulclpi 9753 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝐶) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
47 | 43, 45, 46 | syl2anc 694 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
48 | | addclpi 9752 |
. . . . . . . . . . 11
⊢
((((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N ∧ ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))
∈ N) → (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
∈ N) |
49 | 41, 47, 48 | syl2anc 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))
∈ N) |
50 | | mulclpi 9753 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐴) ∈ N ∧
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))) ∈ N) →
((1^{st} ‘𝐴)
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))) ∈
N) |
51 | 31, 49, 50 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)))) ∈
N) |
52 | | mulclpi 9753 |
. . . . . . . . . . 11
⊢
(((2^{nd} ‘𝐵) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N) → ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
53 | 45, 39, 52 | syl2anc 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
54 | | mulclpi 9753 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) ∈ N) →
((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
∈ N) |
55 | 29, 53, 54 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))) ∈ N) |
56 | | mulcanenq 9820 |
. . . . . . . . 9
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
((1^{st} ‘𝐴)
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))) ∈ N ∧
((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))
∈ N) → ⟨((2^{nd} ‘𝐴) ·_{N}
((1^{st} ‘𝐴)
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))))⟩ ~_{Q}
⟨((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
57 | 29, 51, 55, 56 | syl3anc 1366 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ⟨((2^{nd} ‘𝐴) ·_{N}
((1^{st} ‘𝐴)
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵))))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐴) ·_{N}
((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))))⟩ ~_{Q}
⟨((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
58 | 25, 57 | syl5eqbr 4720 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ⟨((((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶)))
+_{N} (((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
·_{N} ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))⟩ ~_{Q}
⟨((1^{st} ‘𝐴) ·_{N}
(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵)))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
59 | | mulpipq2 9799 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·_{pQ} 𝐵) = ⟨((1^{st}
‘𝐴)
·_{N} (1^{st} ‘𝐵)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) |
60 | 27, 33, 59 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{pQ} 𝐵) = ⟨((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐵)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩) |
61 | | mulpipq2 9799 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐶
∈ (N × N)) → (𝐴 ·_{pQ} 𝐶) = ⟨((1^{st}
‘𝐴)
·_{N} (1^{st} ‘𝐶)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))⟩) |
62 | 27, 37, 61 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{pQ} 𝐶) = ⟨((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐶)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))⟩) |
63 | 60, 62 | oveq12d 6708 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·_{pQ} 𝐵) +_{pQ} (𝐴
·_{pQ} 𝐶)) = (⟨((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐵)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ +_{pQ}
⟨((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶)),
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))⟩)) |
64 | | mulclpi 9753 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐴) ∈ N ∧
(1^{st} ‘𝐵)
∈ N) → ((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
∈ N) |
65 | 31, 35, 64 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
∈ N) |
66 | | mulclpi 9753 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐵)
∈ N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
67 | 29, 45, 66 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) |
68 | | mulclpi 9753 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐴) ∈ N ∧
(1^{st} ‘𝐶)
∈ N) → ((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
∈ N) |
69 | 31, 43, 68 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
∈ N) |
70 | | mulclpi 9753 |
. . . . . . . . . 10
⊢
(((2^{nd} ‘𝐴) ∈ N ∧
(2^{nd} ‘𝐶)
∈ N) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
71 | 29, 39, 70 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))
∈ N) |
72 | | addpipq 9797 |
. . . . . . . . 9
⊢
(((((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵))
∈ N ∧ ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐵))
∈ N) ∧ (((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶))
∈ N ∧ ((2^{nd} ‘𝐴) ·_{N}
(2^{nd} ‘𝐶))
∈ N)) → (⟨((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐵)), ((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ +_{pQ}
⟨((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶)),
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))⟩) = ⟨((((1^{st}
‘𝐴)
·_{N} (1^{st} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐶)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))⟩) |
73 | 65, 67, 69, 71, 72 | syl22anc 1367 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (⟨((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐵)),
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵))⟩ +_{pQ}
⟨((1^{st} ‘𝐴) ·_{N}
(1^{st} ‘𝐶)),
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))⟩) = ⟨((((1^{st}
‘𝐴)
·_{N} (1^{st} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐶)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))⟩) |
74 | 63, 73 | eqtrd 2685 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·_{pQ} 𝐵) +_{pQ} (𝐴
·_{pQ} 𝐶)) = ⟨((((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶))) +_{N}
(((1^{st} ‘𝐴)
·_{N} (1^{st} ‘𝐶)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)))), (((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐵)) ·_{N}
((2^{nd} ‘𝐴)
·_{N} (2^{nd} ‘𝐶)))⟩) |
75 | | relxp 5160 |
. . . . . . . . . 10
⊢ Rel
(N × N) |
76 | | 1st2nd 7258 |
. . . . . . . . . 10
⊢ ((Rel
(N × N) ∧ 𝐴 ∈ (N ×
N)) → 𝐴
= ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
77 | 75, 27, 76 | sylancr 696 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴 =
⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
78 | | addpipq2 9796 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (N ×
N) ∧ 𝐶
∈ (N × N)) → (𝐵 +_{pQ} 𝐶) = ⟨(((1^{st}
‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩) |
79 | 33, 37, 78 | syl2anc 694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
+_{pQ} 𝐶) = ⟨(((1^{st} ‘𝐵)
·_{N} (2^{nd} ‘𝐶)) +_{N}
((1^{st} ‘𝐶)
·_{N} (2^{nd} ‘𝐵))), ((2^{nd} ‘𝐵)
·_{N} (2^{nd} ‘𝐶))⟩) |
80 | 77, 79 | oveq12d 6708 |
. . . . . . . 8
⊢ ((𝐴 ∈ 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} ‘𝐶))⟩)) |
81 | | mulpipq 9800 |
. . . . . . . . 9
⊢
((((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} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
82 | 31, 29, 49, 53, 81 | syl22anc 1367 |
. . . . . . . 8
⊢ ((𝐴 ∈ 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} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
83 | 80, 82 | eqtrd 2685 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)) = ⟨((1^{st}
‘𝐴)
·_{N} (((1^{st} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶))
+_{N} ((1^{st} ‘𝐶) ·_{N}
(2^{nd} ‘𝐵)))), ((2^{nd} ‘𝐴)
·_{N} ((2^{nd} ‘𝐵) ·_{N}
(2^{nd} ‘𝐶)))⟩) |
84 | 58, 74, 83 | 3brtr4d 4717 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·_{pQ} 𝐵) +_{pQ} (𝐴
·_{pQ} 𝐶)) ~_{Q} (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶))) |
85 | | mulpqf 9806 |
. . . . . . . . . 10
⊢
·_{pQ} :((N × N)
× (N × N))⟶(N
× N) |
86 | 85 | fovcl 6807 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·_{pQ} 𝐵) ∈ (N
× N)) |
87 | 27, 33, 86 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{pQ} 𝐵) ∈ (N ×
N)) |
88 | 85 | fovcl 6807 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐶
∈ (N × N)) → (𝐴 ·_{pQ} 𝐶) ∈ (N
× N)) |
89 | 27, 37, 88 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{pQ} 𝐶) ∈ (N ×
N)) |
90 | | addpqf 9804 |
. . . . . . . . 9
⊢
+_{pQ} :((N × N)
× (N × N))⟶(N
× N) |
91 | 90 | fovcl 6807 |
. . . . . . . 8
⊢ (((𝐴
·_{pQ} 𝐵) ∈ (N ×
N) ∧ (𝐴
·_{pQ} 𝐶) ∈ (N ×
N)) → ((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶)) ∈ (N ×
N)) |
92 | 87, 89, 91 | syl2anc 694 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·_{pQ} 𝐵) +_{pQ} (𝐴
·_{pQ} 𝐶)) ∈ (N ×
N)) |
93 | 90 | fovcl 6807 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (N ×
N) ∧ 𝐶
∈ (N × N)) → (𝐵 +_{pQ} 𝐶) ∈ (N
× N)) |
94 | 33, 37, 93 | syl2anc 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
+_{pQ} 𝐶) ∈ (N ×
N)) |
95 | 85 | fovcl 6807 |
. . . . . . . 8
⊢ ((𝐴 ∈ (N ×
N) ∧ (𝐵
+_{pQ} 𝐶) ∈ (N ×
N)) → (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)) ∈ (N
× N)) |
96 | 27, 94, 95 | syl2anc 694 |
. . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)) ∈ (N
× N)) |
97 | | nqereq 9795 |
. . . . . . 7
⊢ ((((𝐴
·_{pQ} 𝐵) +_{pQ} (𝐴
·_{pQ} 𝐶)) ∈ (N ×
N) ∧ (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)) ∈ (N
× N)) → (((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶)) ~_{Q} (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)) ↔
([Q]‘((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶))) = ([Q]‘(𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶))))) |
98 | 92, 96, 97 | syl2anc 694 |
. . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶)) ~_{Q} (𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)) ↔
([Q]‘((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶))) = ([Q]‘(𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶))))) |
99 | 84, 98 | mpbid 222 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ([Q]‘((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶))) = ([Q]‘(𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶)))) |
100 | 99 | eqcomd 2657 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ([Q]‘(𝐴 ·_{pQ} (𝐵 +_{pQ}
𝐶))) =
([Q]‘((𝐴 ·_{pQ} 𝐵) +_{pQ}
(𝐴
·_{pQ} 𝐶)))) |
101 | | mulerpq 9817 |
. . . 4
⊢
(([Q]‘𝐴) ·_{Q}
([Q]‘(𝐵
+_{pQ} 𝐶))) = ([Q]‘(𝐴
·_{pQ} (𝐵 +_{pQ} 𝐶))) |
102 | | adderpq 9816 |
. . . 4
⊢
(([Q]‘(𝐴 ·_{pQ} 𝐵)) +_{Q}
([Q]‘(𝐴
·_{pQ} 𝐶))) = ([Q]‘((𝐴
·_{pQ} 𝐵) +_{pQ} (𝐴
·_{pQ} 𝐶))) |
103 | 100, 101,
102 | 3eqtr4g 2710 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (([Q]‘𝐴) ·_{Q}
([Q]‘(𝐵
+_{pQ} 𝐶))) = (([Q]‘(𝐴
·_{pQ} 𝐵)) +_{Q}
([Q]‘(𝐴
·_{pQ} 𝐶)))) |
104 | | nqerid 9793 |
. . . . . 6
⊢ (𝐴 ∈ Q →
([Q]‘𝐴)
= 𝐴) |
105 | 104 | eqcomd 2657 |
. . . . 5
⊢ (𝐴 ∈ Q →
𝐴 =
([Q]‘𝐴)) |
106 | 105 | 3ad2ant1 1102 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴 =
([Q]‘𝐴)) |
107 | | addpqnq 9798 |
. . . . 5
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐵
+_{Q} 𝐶) = ([Q]‘(𝐵 +_{pQ}
𝐶))) |
108 | 107 | 3adant1 1099 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
+_{Q} 𝐶) = ([Q]‘(𝐵 +_{pQ}
𝐶))) |
109 | 106, 108 | oveq12d 6708 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{Q} (𝐵 +_{Q} 𝐶)) =
(([Q]‘𝐴) ·_{Q}
([Q]‘(𝐵
+_{pQ} 𝐶)))) |
110 | | mulpqnq 9801 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
·_{Q} 𝐵) = ([Q]‘(𝐴
·_{pQ} 𝐵))) |
111 | 110 | 3adant3 1101 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{Q} 𝐵) = ([Q]‘(𝐴
·_{pQ} 𝐵))) |
112 | | mulpqnq 9801 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐴
·_{Q} 𝐶) = ([Q]‘(𝐴
·_{pQ} 𝐶))) |
113 | 112 | 3adant2 1100 |
. . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{Q} 𝐶) = ([Q]‘(𝐴
·_{pQ} 𝐶))) |
114 | 111, 113 | oveq12d 6708 |
. . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·_{Q} 𝐵) +_{Q} (𝐴
·_{Q} 𝐶)) = (([Q]‘(𝐴
·_{pQ} 𝐵)) +_{Q}
([Q]‘(𝐴
·_{pQ} 𝐶)))) |
115 | 103, 109,
114 | 3eqtr4d 2695 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·_{Q} (𝐵 +_{Q} 𝐶)) = ((𝐴 ·_{Q} 𝐵) +_{Q}
(𝐴
·_{Q} 𝐶))) |
116 | | addnqf 9808 |
. . . 4
⊢
+_{Q} :(Q ×
Q)⟶Q |
117 | 116 | fdmi 6090 |
. . 3
⊢ dom
+_{Q} = (Q ×
Q) |
118 | | 0nnq 9784 |
. . 3
⊢ ¬
∅ ∈ Q |
119 | | mulnqf 9809 |
. . . 4
⊢
·_{Q} :(Q ×
Q)⟶Q |
120 | 119 | fdmi 6090 |
. . 3
⊢ dom
·_{Q} = (Q ×
Q) |
121 | 117, 118,
120 | ndmovdistr 6865 |
. 2
⊢ (¬
(𝐴 ∈ Q
∧ 𝐵 ∈
Q ∧ 𝐶
∈ Q) → (𝐴 ·_{Q} (𝐵 +_{Q}
𝐶)) = ((𝐴 ·_{Q} 𝐵) +_{Q}
(𝐴
·_{Q} 𝐶))) |
122 | 115, 121 | pm2.61i 176 |
1
⊢ (𝐴
·_{Q} (𝐵 +_{Q} 𝐶)) = ((𝐴 ·_{Q} 𝐵) +_{Q}
(𝐴
·_{Q} 𝐶)) |