Proof of Theorem mulassnq
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulasspi 10938 | . . . . . . 7
⊢
(((1st ‘𝐴) ·N
(1st ‘𝐵))
·N (1st ‘𝐶)) = ((1st ‘𝐴)
·N ((1st ‘𝐵) ·N
(1st ‘𝐶))) | 
| 2 |  | mulasspi 10938 | . . . . . . 7
⊢
(((2nd ‘𝐴) ·N
(2nd ‘𝐵))
·N (2nd ‘𝐶)) = ((2nd ‘𝐴)
·N ((2nd ‘𝐵) ·N
(2nd ‘𝐶))) | 
| 3 | 1, 2 | opeq12i 4877 | . . . . . 6
⊢
〈(((1st ‘𝐴) ·N
(1st ‘𝐵))
·N (1st ‘𝐶)), (((2nd ‘𝐴)
·N (2nd ‘𝐵)) ·N
(2nd ‘𝐶))〉 = 〈((1st
‘𝐴)
·N ((1st ‘𝐵) ·N
(1st ‘𝐶))), ((2nd ‘𝐴)
·N ((2nd ‘𝐵) ·N
(2nd ‘𝐶)))〉 | 
| 4 |  | elpqn 10966 | . . . . . . . . . 10
⊢ (𝐴 ∈ Q →
𝐴 ∈ (N
× N)) | 
| 5 | 4 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴
∈ (N × N)) | 
| 6 |  | elpqn 10966 | . . . . . . . . . 10
⊢ (𝐵 ∈ Q →
𝐵 ∈ (N
× N)) | 
| 7 | 6 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐵
∈ (N × N)) | 
| 8 |  | mulpipq2 10980 | . . . . . . . . 9
⊢ ((𝐴 ∈ (N ×
N) ∧ 𝐵
∈ (N × N)) → (𝐴 ·pQ 𝐵) = 〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) | 
| 9 | 5, 7, 8 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·pQ 𝐵) = 〈((1st ‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉) | 
| 10 |  | relxp 5702 | . . . . . . . . 9
⊢ Rel
(N × N) | 
| 11 |  | elpqn 10966 | . . . . . . . . . 10
⊢ (𝐶 ∈ Q →
𝐶 ∈ (N
× N)) | 
| 12 | 11 | 3ad2ant3 1135 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶
∈ (N × N)) | 
| 13 |  | 1st2nd 8065 | . . . . . . . . 9
⊢ ((Rel
(N × N) ∧ 𝐶 ∈ (N ×
N)) → 𝐶
= 〈(1st ‘𝐶), (2nd ‘𝐶)〉) | 
| 14 | 10, 12, 13 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶 =
〈(1st ‘𝐶), (2nd ‘𝐶)〉) | 
| 15 | 9, 14 | oveq12d 7450 | . . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·pQ 𝐵) ·pQ 𝐶) = (〈((1st
‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉 ·pQ
〈(1st ‘𝐶), (2nd ‘𝐶)〉)) | 
| 16 |  | xp1st 8047 | . . . . . . . . . 10
⊢ (𝐴 ∈ (N ×
N) → (1st ‘𝐴) ∈ N) | 
| 17 | 5, 16 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1st ‘𝐴) ∈ N) | 
| 18 |  | xp1st 8047 | . . . . . . . . . 10
⊢ (𝐵 ∈ (N ×
N) → (1st ‘𝐵) ∈ N) | 
| 19 | 7, 18 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1st ‘𝐵) ∈ N) | 
| 20 |  | mulclpi 10934 | . . . . . . . . 9
⊢
(((1st ‘𝐴) ∈ N ∧
(1st ‘𝐵)
∈ N) → ((1st ‘𝐴) ·N
(1st ‘𝐵))
∈ N) | 
| 21 | 17, 19, 20 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1st ‘𝐴) ·N
(1st ‘𝐵))
∈ N) | 
| 22 |  | xp2nd 8048 | . . . . . . . . . 10
⊢ (𝐴 ∈ (N ×
N) → (2nd ‘𝐴) ∈ N) | 
| 23 | 5, 22 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐴) ∈ N) | 
| 24 |  | xp2nd 8048 | . . . . . . . . . 10
⊢ (𝐵 ∈ (N ×
N) → (2nd ‘𝐵) ∈ N) | 
| 25 | 7, 24 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐵) ∈ N) | 
| 26 |  | mulclpi 10934 | . . . . . . . . 9
⊢
(((2nd ‘𝐴) ∈ N ∧
(2nd ‘𝐵)
∈ N) → ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) | 
| 27 | 23, 25, 26 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) | 
| 28 |  | xp1st 8047 | . . . . . . . . 9
⊢ (𝐶 ∈ (N ×
N) → (1st ‘𝐶) ∈ N) | 
| 29 | 12, 28 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (1st ‘𝐶) ∈ N) | 
| 30 |  | xp2nd 8048 | . . . . . . . . 9
⊢ (𝐶 ∈ (N ×
N) → (2nd ‘𝐶) ∈ N) | 
| 31 | 12, 30 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (2nd ‘𝐶) ∈ N) | 
| 32 |  | mulpipq 10981 | . . . . . . . 8
⊢
(((((1st ‘𝐴) ·N
(1st ‘𝐵))
∈ N ∧ ((2nd ‘𝐴) ·N
(2nd ‘𝐵))
∈ N) ∧ ((1st ‘𝐶) ∈ N ∧
(2nd ‘𝐶)
∈ N)) → (〈((1st ‘𝐴)
·N (1st ‘𝐵)), ((2nd ‘𝐴)
·N (2nd ‘𝐵))〉 ·pQ
〈(1st ‘𝐶), (2nd ‘𝐶)〉) = 〈(((1st
‘𝐴)
·N (1st ‘𝐵)) ·N
(1st ‘𝐶)),
(((2nd ‘𝐴)
·N (2nd ‘𝐵)) ·N
(2nd ‘𝐶))〉) | 
| 33 | 21, 27, 29, 31, 32 | syl22anc 838 | . . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (〈((1st ‘𝐴) ·N
(1st ‘𝐵)),
((2nd ‘𝐴)
·N (2nd ‘𝐵))〉 ·pQ
〈(1st ‘𝐶), (2nd ‘𝐶)〉) = 〈(((1st
‘𝐴)
·N (1st ‘𝐵)) ·N
(1st ‘𝐶)),
(((2nd ‘𝐴)
·N (2nd ‘𝐵)) ·N
(2nd ‘𝐶))〉) | 
| 34 | 15, 33 | eqtrd 2776 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·pQ 𝐵) ·pQ 𝐶) = 〈(((1st
‘𝐴)
·N (1st ‘𝐵)) ·N
(1st ‘𝐶)),
(((2nd ‘𝐴)
·N (2nd ‘𝐵)) ·N
(2nd ‘𝐶))〉) | 
| 35 |  | 1st2nd 8065 | . . . . . . . . 9
⊢ ((Rel
(N × N) ∧ 𝐴 ∈ (N ×
N)) → 𝐴
= 〈(1st ‘𝐴), (2nd ‘𝐴)〉) | 
| 36 | 10, 5, 35 | sylancr 587 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴 =
〈(1st ‘𝐴), (2nd ‘𝐴)〉) | 
| 37 |  | mulpipq2 10980 | . . . . . . . . 9
⊢ ((𝐵 ∈ (N ×
N) ∧ 𝐶
∈ (N × N)) → (𝐵 ·pQ 𝐶) = 〈((1st
‘𝐵)
·N (1st ‘𝐶)), ((2nd ‘𝐵)
·N (2nd ‘𝐶))〉) | 
| 38 | 7, 12, 37 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
·pQ 𝐶) = 〈((1st ‘𝐵)
·N (1st ‘𝐶)), ((2nd ‘𝐵)
·N (2nd ‘𝐶))〉) | 
| 39 | 36, 38 | oveq12d 7450 | . . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·pQ (𝐵 ·pQ 𝐶)) = (〈(1st
‘𝐴), (2nd
‘𝐴)〉
·pQ 〈((1st ‘𝐵)
·N (1st ‘𝐶)), ((2nd ‘𝐵)
·N (2nd ‘𝐶))〉)) | 
| 40 |  | mulclpi 10934 | . . . . . . . . 9
⊢
(((1st ‘𝐵) ∈ N ∧
(1st ‘𝐶)
∈ N) → ((1st ‘𝐵) ·N
(1st ‘𝐶))
∈ N) | 
| 41 | 19, 29, 40 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((1st ‘𝐵) ·N
(1st ‘𝐶))
∈ N) | 
| 42 |  | mulclpi 10934 | . . . . . . . . 9
⊢
(((2nd ‘𝐵) ∈ N ∧
(2nd ‘𝐶)
∈ N) → ((2nd ‘𝐵) ·N
(2nd ‘𝐶))
∈ N) | 
| 43 | 25, 31, 42 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((2nd ‘𝐵) ·N
(2nd ‘𝐶))
∈ N) | 
| 44 |  | mulpipq 10981 | . . . . . . . 8
⊢
((((1st ‘𝐴) ∈ N ∧
(2nd ‘𝐴)
∈ N) ∧ (((1st ‘𝐵) ·N
(1st ‘𝐶))
∈ N ∧ ((2nd ‘𝐵) ·N
(2nd ‘𝐶))
∈ N)) → (〈(1st ‘𝐴), (2nd ‘𝐴)〉 ·pQ
〈((1st ‘𝐵) ·N
(1st ‘𝐶)),
((2nd ‘𝐵)
·N (2nd ‘𝐶))〉) = 〈((1st
‘𝐴)
·N ((1st ‘𝐵) ·N
(1st ‘𝐶))), ((2nd ‘𝐴)
·N ((2nd ‘𝐵) ·N
(2nd ‘𝐶)))〉) | 
| 45 | 17, 23, 41, 43, 44 | syl22anc 838 | . . . . . . 7
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (〈(1st ‘𝐴), (2nd ‘𝐴)〉 ·pQ
〈((1st ‘𝐵) ·N
(1st ‘𝐶)),
((2nd ‘𝐵)
·N (2nd ‘𝐶))〉) = 〈((1st
‘𝐴)
·N ((1st ‘𝐵) ·N
(1st ‘𝐶))), ((2nd ‘𝐴)
·N ((2nd ‘𝐵) ·N
(2nd ‘𝐶)))〉) | 
| 46 | 39, 45 | eqtrd 2776 | . . . . . 6
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·pQ (𝐵 ·pQ 𝐶)) = 〈((1st
‘𝐴)
·N ((1st ‘𝐵) ·N
(1st ‘𝐶))), ((2nd ‘𝐴)
·N ((2nd ‘𝐵) ·N
(2nd ‘𝐶)))〉) | 
| 47 | 3, 34, 46 | 3eqtr4a 2802 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·pQ 𝐵) ·pQ 𝐶) = (𝐴 ·pQ (𝐵
·pQ 𝐶))) | 
| 48 | 47 | fveq2d 6909 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ([Q]‘((𝐴 ·pQ 𝐵)
·pQ 𝐶)) = ([Q]‘(𝐴
·pQ (𝐵 ·pQ 𝐶)))) | 
| 49 |  | mulerpq 10998 | . . . 4
⊢
(([Q]‘(𝐴 ·pQ 𝐵))
·Q ([Q]‘𝐶)) = ([Q]‘((𝐴
·pQ 𝐵) ·pQ 𝐶)) | 
| 50 |  | mulerpq 10998 | . . . 4
⊢
(([Q]‘𝐴) ·Q
([Q]‘(𝐵
·pQ 𝐶))) = ([Q]‘(𝐴
·pQ (𝐵 ·pQ 𝐶))) | 
| 51 | 48, 49, 50 | 3eqtr4g 2801 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (([Q]‘(𝐴 ·pQ 𝐵))
·Q ([Q]‘𝐶)) = (([Q]‘𝐴)
·Q ([Q]‘(𝐵 ·pQ 𝐶)))) | 
| 52 |  | mulpqnq 10982 | . . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
·Q 𝐵) = ([Q]‘(𝐴
·pQ 𝐵))) | 
| 53 | 52 | 3adant3 1132 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·Q 𝐵) = ([Q]‘(𝐴
·pQ 𝐵))) | 
| 54 |  | nqerid 10974 | . . . . . 6
⊢ (𝐶 ∈ Q →
([Q]‘𝐶)
= 𝐶) | 
| 55 | 54 | eqcomd 2742 | . . . . 5
⊢ (𝐶 ∈ Q →
𝐶 =
([Q]‘𝐶)) | 
| 56 | 55 | 3ad2ant3 1135 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐶 =
([Q]‘𝐶)) | 
| 57 | 53, 56 | oveq12d 7450 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·Q 𝐵) ·Q 𝐶) =
(([Q]‘(𝐴 ·pQ 𝐵))
·Q ([Q]‘𝐶))) | 
| 58 |  | nqerid 10974 | . . . . . 6
⊢ (𝐴 ∈ Q →
([Q]‘𝐴)
= 𝐴) | 
| 59 | 58 | eqcomd 2742 | . . . . 5
⊢ (𝐴 ∈ Q →
𝐴 =
([Q]‘𝐴)) | 
| 60 | 59 | 3ad2ant1 1133 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → 𝐴 =
([Q]‘𝐴)) | 
| 61 |  | mulpqnq 10982 | . . . . 5
⊢ ((𝐵 ∈ Q ∧
𝐶 ∈ Q)
→ (𝐵
·Q 𝐶) = ([Q]‘(𝐵
·pQ 𝐶))) | 
| 62 | 61 | 3adant1 1130 | . . . 4
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐵
·Q 𝐶) = ([Q]‘(𝐵
·pQ 𝐶))) | 
| 63 | 60, 62 | oveq12d 7450 | . . 3
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → (𝐴
·Q (𝐵 ·Q 𝐶)) =
(([Q]‘𝐴) ·Q
([Q]‘(𝐵
·pQ 𝐶)))) | 
| 64 | 51, 57, 63 | 3eqtr4d 2786 | . 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q
∧ 𝐶 ∈
Q) → ((𝐴
·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵
·Q 𝐶))) | 
| 65 |  | mulnqf 10990 | . . . 4
⊢ 
·Q :(Q ×
Q)⟶Q | 
| 66 | 65 | fdmi 6746 | . . 3
⊢ dom
·Q = (Q ×
Q) | 
| 67 |  | 0nnq 10965 | . . 3
⊢  ¬
∅ ∈ Q | 
| 68 | 66, 67 | ndmovass 7622 | . 2
⊢ (¬
(𝐴 ∈ Q
∧ 𝐵 ∈
Q ∧ 𝐶
∈ Q) → ((𝐴 ·Q 𝐵)
·Q 𝐶) = (𝐴 ·Q (𝐵
·Q 𝐶))) | 
| 69 | 64, 68 | pm2.61i 182 | 1
⊢ ((𝐴
·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵
·Q 𝐶)) |