MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  distrnq Structured version   Visualization version   GIF version

Theorem distrnq 10763
Description: Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
distrnq (𝐴 ·Q (𝐡 +Q 𝐢)) = ((𝐴 ·Q 𝐡) +Q (𝐴 ·Q 𝐢))

Proof of Theorem distrnq
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulcompi 10698 . . . . . . . . . . . . 13 ((1st β€˜π΄) Β·N (1st β€˜π΅)) = ((1st β€˜π΅) Β·N (1st β€˜π΄))
21oveq1i 7317 . . . . . . . . . . . 12 (((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) = (((1st β€˜π΅) Β·N (1st β€˜π΄)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))
3 fvex 6817 . . . . . . . . . . . . 13 (1st β€˜π΅) ∈ V
4 fvex 6817 . . . . . . . . . . . . 13 (1st β€˜π΄) ∈ V
5 fvex 6817 . . . . . . . . . . . . 13 (2nd β€˜π΄) ∈ V
6 mulcompi 10698 . . . . . . . . . . . . 13 (π‘₯ Β·N 𝑦) = (𝑦 Β·N π‘₯)
7 mulasspi 10699 . . . . . . . . . . . . 13 ((π‘₯ Β·N 𝑦) Β·N 𝑧) = (π‘₯ Β·N (𝑦 Β·N 𝑧))
8 fvex 6817 . . . . . . . . . . . . 13 (2nd β€˜πΆ) ∈ V
93, 4, 5, 6, 7, 8caov411 7536 . . . . . . . . . . . 12 (((1st β€˜π΅) Β·N (1st β€˜π΄)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) = (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜π΅) Β·N (2nd β€˜πΆ)))
102, 9eqtri 2764 . . . . . . . . . . 11 (((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) = (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜π΅) Β·N (2nd β€˜πΆ)))
11 mulcompi 10698 . . . . . . . . . . . . 13 ((1st β€˜π΄) Β·N (1st β€˜πΆ)) = ((1st β€˜πΆ) Β·N (1st β€˜π΄))
1211oveq1i 7317 . . . . . . . . . . . 12 (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅))) = (((1st β€˜πΆ) Β·N (1st β€˜π΄)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))
13 fvex 6817 . . . . . . . . . . . . 13 (1st β€˜πΆ) ∈ V
14 fvex 6817 . . . . . . . . . . . . 13 (2nd β€˜π΅) ∈ V
1513, 4, 5, 6, 7, 14caov411 7536 . . . . . . . . . . . 12 (((1st β€˜πΆ) Β·N (1st β€˜π΄)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅))) = (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))
1612, 15eqtri 2764 . . . . . . . . . . 11 (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅))) = (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))
1710, 16oveq12i 7319 . . . . . . . . . 10 ((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))) = ((((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜π΅) Β·N (2nd β€˜πΆ))) +N (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))))
18 distrpi 10700 . . . . . . . . . 10 (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))) = ((((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜π΅) Β·N (2nd β€˜πΆ))) +N (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))))
19 mulasspi 10699 . . . . . . . . . 10 (((2nd β€˜π΄) Β·N (1st β€˜π΄)) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))) = ((2nd β€˜π΄) Β·N ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))))
2017, 18, 193eqtr2i 2770 . . . . . . . . 9 ((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))) = ((2nd β€˜π΄) Β·N ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))))
21 mulasspi 10699 . . . . . . . . . 10 (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) = ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))))
2214, 5, 8, 6, 7caov12 7532 . . . . . . . . . . 11 ((2nd β€˜π΅) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) = ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))
2322oveq2i 7318 . . . . . . . . . 10 ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))) = ((2nd β€˜π΄) Β·N ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))))
2421, 23eqtri 2764 . . . . . . . . 9 (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) = ((2nd β€˜π΄) Β·N ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))))
2520, 24opeq12i 4814 . . . . . . . 8 ⟨((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))), (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))⟩ = ⟨((2nd β€˜π΄) Β·N ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))))⟩
26 elpqn 10727 . . . . . . . . . . 11 (𝐴 ∈ Q β†’ 𝐴 ∈ (N Γ— N))
27263ad2ant1 1133 . . . . . . . . . 10 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ 𝐴 ∈ (N Γ— N))
28 xp2nd 7896 . . . . . . . . . 10 (𝐴 ∈ (N Γ— N) β†’ (2nd β€˜π΄) ∈ N)
2927, 28syl 17 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (2nd β€˜π΄) ∈ N)
30 xp1st 7895 . . . . . . . . . . 11 (𝐴 ∈ (N Γ— N) β†’ (1st β€˜π΄) ∈ N)
3127, 30syl 17 . . . . . . . . . 10 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (1st β€˜π΄) ∈ N)
32 elpqn 10727 . . . . . . . . . . . . . 14 (𝐡 ∈ Q β†’ 𝐡 ∈ (N Γ— N))
33323ad2ant2 1134 . . . . . . . . . . . . 13 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ 𝐡 ∈ (N Γ— N))
34 xp1st 7895 . . . . . . . . . . . . 13 (𝐡 ∈ (N Γ— N) β†’ (1st β€˜π΅) ∈ N)
3533, 34syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (1st β€˜π΅) ∈ N)
36 elpqn 10727 . . . . . . . . . . . . . 14 (𝐢 ∈ Q β†’ 𝐢 ∈ (N Γ— N))
37363ad2ant3 1135 . . . . . . . . . . . . 13 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ 𝐢 ∈ (N Γ— N))
38 xp2nd 7896 . . . . . . . . . . . . 13 (𝐢 ∈ (N Γ— N) β†’ (2nd β€˜πΆ) ∈ N)
3937, 38syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (2nd β€˜πΆ) ∈ N)
40 mulclpi 10695 . . . . . . . . . . . 12 (((1st β€˜π΅) ∈ N ∧ (2nd β€˜πΆ) ∈ N) β†’ ((1st β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N)
4135, 39, 40syl2anc 585 . . . . . . . . . . 11 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((1st β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N)
42 xp1st 7895 . . . . . . . . . . . . 13 (𝐢 ∈ (N Γ— N) β†’ (1st β€˜πΆ) ∈ N)
4337, 42syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (1st β€˜πΆ) ∈ N)
44 xp2nd 7896 . . . . . . . . . . . . 13 (𝐡 ∈ (N Γ— N) β†’ (2nd β€˜π΅) ∈ N)
4533, 44syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (2nd β€˜π΅) ∈ N)
46 mulclpi 10695 . . . . . . . . . . . 12 (((1st β€˜πΆ) ∈ N ∧ (2nd β€˜π΅) ∈ N) β†’ ((1st β€˜πΆ) Β·N (2nd β€˜π΅)) ∈ N)
4743, 45, 46syl2anc 585 . . . . . . . . . . 11 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((1st β€˜πΆ) Β·N (2nd β€˜π΅)) ∈ N)
48 addclpi 10694 . . . . . . . . . . 11 ((((1st β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N ∧ ((1st β€˜πΆ) Β·N (2nd β€˜π΅)) ∈ N) β†’ (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))) ∈ N)
4941, 47, 48syl2anc 585 . . . . . . . . . 10 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))) ∈ N)
50 mulclpi 10695 . . . . . . . . . 10 (((1st β€˜π΄) ∈ N ∧ (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))) ∈ N) β†’ ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))) ∈ N)
5131, 49, 50syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))) ∈ N)
52 mulclpi 10695 . . . . . . . . . . 11 (((2nd β€˜π΅) ∈ N ∧ (2nd β€˜πΆ) ∈ N) β†’ ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N)
5345, 39, 52syl2anc 585 . . . . . . . . . 10 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N)
54 mulclpi 10695 . . . . . . . . . 10 (((2nd β€˜π΄) ∈ N ∧ ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N) β†’ ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))) ∈ N)
5529, 53, 54syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))) ∈ N)
56 mulcanenq 10762 . . . . . . . . 9 (((2nd β€˜π΄) ∈ N ∧ ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))) ∈ N ∧ ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))) ∈ N) β†’ ⟨((2nd β€˜π΄) Β·N ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))))⟩ ~Q ⟨((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))⟩)
5729, 51, 55, 56syl3anc 1371 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ⟨((2nd β€˜π΄) Β·N ((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))))⟩ ~Q ⟨((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))⟩)
5825, 57eqbrtrid 5116 . . . . . . 7 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ⟨((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))), (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))⟩ ~Q ⟨((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))⟩)
59 mulpipq2 10741 . . . . . . . . . 10 ((𝐴 ∈ (N Γ— N) ∧ 𝐡 ∈ (N Γ— N)) β†’ (𝐴 Β·pQ 𝐡) = ⟨((1st β€˜π΄) Β·N (1st β€˜π΅)), ((2nd β€˜π΄) Β·N (2nd β€˜π΅))⟩)
6027, 33, 59syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ 𝐡) = ⟨((1st β€˜π΄) Β·N (1st β€˜π΅)), ((2nd β€˜π΄) Β·N (2nd β€˜π΅))⟩)
61 mulpipq2 10741 . . . . . . . . . 10 ((𝐴 ∈ (N Γ— N) ∧ 𝐢 ∈ (N Γ— N)) β†’ (𝐴 Β·pQ 𝐢) = ⟨((1st β€˜π΄) Β·N (1st β€˜πΆ)), ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))⟩)
6227, 37, 61syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ 𝐢) = ⟨((1st β€˜π΄) Β·N (1st β€˜πΆ)), ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))⟩)
6360, 62oveq12d 7325 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) = (⟨((1st β€˜π΄) Β·N (1st β€˜π΅)), ((2nd β€˜π΄) Β·N (2nd β€˜π΅))⟩ +pQ ⟨((1st β€˜π΄) Β·N (1st β€˜πΆ)), ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))⟩))
64 mulclpi 10695 . . . . . . . . . 10 (((1st β€˜π΄) ∈ N ∧ (1st β€˜π΅) ∈ N) β†’ ((1st β€˜π΄) Β·N (1st β€˜π΅)) ∈ N)
6531, 35, 64syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((1st β€˜π΄) Β·N (1st β€˜π΅)) ∈ N)
66 mulclpi 10695 . . . . . . . . . 10 (((2nd β€˜π΄) ∈ N ∧ (2nd β€˜π΅) ∈ N) β†’ ((2nd β€˜π΄) Β·N (2nd β€˜π΅)) ∈ N)
6729, 45, 66syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((2nd β€˜π΄) Β·N (2nd β€˜π΅)) ∈ N)
68 mulclpi 10695 . . . . . . . . . 10 (((1st β€˜π΄) ∈ N ∧ (1st β€˜πΆ) ∈ N) β†’ ((1st β€˜π΄) Β·N (1st β€˜πΆ)) ∈ N)
6931, 43, 68syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((1st β€˜π΄) Β·N (1st β€˜πΆ)) ∈ N)
70 mulclpi 10695 . . . . . . . . . 10 (((2nd β€˜π΄) ∈ N ∧ (2nd β€˜πΆ) ∈ N) β†’ ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)) ∈ N)
7129, 39, 70syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)) ∈ N)
72 addpipq 10739 . . . . . . . . 9 (((((1st β€˜π΄) Β·N (1st β€˜π΅)) ∈ N ∧ ((2nd β€˜π΄) Β·N (2nd β€˜π΅)) ∈ N) ∧ (((1st β€˜π΄) Β·N (1st β€˜πΆ)) ∈ N ∧ ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)) ∈ N)) β†’ (⟨((1st β€˜π΄) Β·N (1st β€˜π΅)), ((2nd β€˜π΄) Β·N (2nd β€˜π΅))⟩ +pQ ⟨((1st β€˜π΄) Β·N (1st β€˜πΆ)), ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))⟩) = ⟨((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))), (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))⟩)
7365, 67, 69, 71, 72syl22anc 837 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (⟨((1st β€˜π΄) Β·N (1st β€˜π΅)), ((2nd β€˜π΄) Β·N (2nd β€˜π΅))⟩ +pQ ⟨((1st β€˜π΄) Β·N (1st β€˜πΆ)), ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))⟩) = ⟨((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))), (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))⟩)
7463, 73eqtrd 2776 . . . . . . 7 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) = ⟨((((1st β€˜π΄) Β·N (1st β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ))) +N (((1st β€˜π΄) Β·N (1st β€˜πΆ)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜π΅)))), (((2nd β€˜π΄) Β·N (2nd β€˜π΅)) Β·N ((2nd β€˜π΄) Β·N (2nd β€˜πΆ)))⟩)
75 relxp 5618 . . . . . . . . . 10 Rel (N Γ— N)
76 1st2nd 7912 . . . . . . . . . 10 ((Rel (N Γ— N) ∧ 𝐴 ∈ (N Γ— N)) β†’ 𝐴 = ⟨(1st β€˜π΄), (2nd β€˜π΄)⟩)
7775, 27, 76sylancr 588 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ 𝐴 = ⟨(1st β€˜π΄), (2nd β€˜π΄)⟩)
78 addpipq2 10738 . . . . . . . . . 10 ((𝐡 ∈ (N Γ— N) ∧ 𝐢 ∈ (N Γ— N)) β†’ (𝐡 +pQ 𝐢) = ⟨(((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))), ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))⟩)
7933, 37, 78syl2anc 585 . . . . . . . . 9 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐡 +pQ 𝐢) = ⟨(((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))), ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))⟩)
8077, 79oveq12d 7325 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ (𝐡 +pQ 𝐢)) = (⟨(1st β€˜π΄), (2nd β€˜π΄)⟩ Β·pQ ⟨(((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))), ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))⟩))
81 mulpipq 10742 . . . . . . . . 9 ((((1st β€˜π΄) ∈ N ∧ (2nd β€˜π΄) ∈ N) ∧ ((((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))) ∈ N ∧ ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)) ∈ N)) β†’ (⟨(1st β€˜π΄), (2nd β€˜π΄)⟩ Β·pQ ⟨(((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))), ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))⟩) = ⟨((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))⟩)
8231, 29, 49, 53, 81syl22anc 837 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (⟨(1st β€˜π΄), (2nd β€˜π΄)⟩ Β·pQ ⟨(((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅))), ((2nd β€˜π΅) Β·N (2nd β€˜πΆ))⟩) = ⟨((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))⟩)
8380, 82eqtrd 2776 . . . . . . 7 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ (𝐡 +pQ 𝐢)) = ⟨((1st β€˜π΄) Β·N (((1st β€˜π΅) Β·N (2nd β€˜πΆ)) +N ((1st β€˜πΆ) Β·N (2nd β€˜π΅)))), ((2nd β€˜π΄) Β·N ((2nd β€˜π΅) Β·N (2nd β€˜πΆ)))⟩)
8458, 74, 833brtr4d 5113 . . . . . 6 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) ~Q (𝐴 Β·pQ (𝐡 +pQ 𝐢)))
85 mulpqf 10748 . . . . . . . . . 10 Β·pQ :((N Γ— N) Γ— (N Γ— N))⟢(N Γ— N)
8685fovcl 7434 . . . . . . . . 9 ((𝐴 ∈ (N Γ— N) ∧ 𝐡 ∈ (N Γ— N)) β†’ (𝐴 Β·pQ 𝐡) ∈ (N Γ— N))
8727, 33, 86syl2anc 585 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ 𝐡) ∈ (N Γ— N))
8885fovcl 7434 . . . . . . . . 9 ((𝐴 ∈ (N Γ— N) ∧ 𝐢 ∈ (N Γ— N)) β†’ (𝐴 Β·pQ 𝐢) ∈ (N Γ— N))
8927, 37, 88syl2anc 585 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ 𝐢) ∈ (N Γ— N))
90 addpqf 10746 . . . . . . . . 9 +pQ :((N Γ— N) Γ— (N Γ— N))⟢(N Γ— N)
9190fovcl 7434 . . . . . . . 8 (((𝐴 Β·pQ 𝐡) ∈ (N Γ— N) ∧ (𝐴 Β·pQ 𝐢) ∈ (N Γ— N)) β†’ ((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) ∈ (N Γ— N))
9287, 89, 91syl2anc 585 . . . . . . 7 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) ∈ (N Γ— N))
9390fovcl 7434 . . . . . . . . 9 ((𝐡 ∈ (N Γ— N) ∧ 𝐢 ∈ (N Γ— N)) β†’ (𝐡 +pQ 𝐢) ∈ (N Γ— N))
9433, 37, 93syl2anc 585 . . . . . . . 8 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐡 +pQ 𝐢) ∈ (N Γ— N))
9585fovcl 7434 . . . . . . . 8 ((𝐴 ∈ (N Γ— N) ∧ (𝐡 +pQ 𝐢) ∈ (N Γ— N)) β†’ (𝐴 Β·pQ (𝐡 +pQ 𝐢)) ∈ (N Γ— N))
9627, 94, 95syl2anc 585 . . . . . . 7 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·pQ (𝐡 +pQ 𝐢)) ∈ (N Γ— N))
97 nqereq 10737 . . . . . . 7 ((((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) ∈ (N Γ— N) ∧ (𝐴 Β·pQ (𝐡 +pQ 𝐢)) ∈ (N Γ— N)) β†’ (((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) ~Q (𝐴 Β·pQ (𝐡 +pQ 𝐢)) ↔ ([Q]β€˜((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢))) = ([Q]β€˜(𝐴 Β·pQ (𝐡 +pQ 𝐢)))))
9892, 96, 97syl2anc 585 . . . . . 6 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)) ~Q (𝐴 Β·pQ (𝐡 +pQ 𝐢)) ↔ ([Q]β€˜((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢))) = ([Q]β€˜(𝐴 Β·pQ (𝐡 +pQ 𝐢)))))
9984, 98mpbid 231 . . . . 5 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ([Q]β€˜((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢))) = ([Q]β€˜(𝐴 Β·pQ (𝐡 +pQ 𝐢))))
10099eqcomd 2742 . . . 4 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ([Q]β€˜(𝐴 Β·pQ (𝐡 +pQ 𝐢))) = ([Q]β€˜((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢))))
101 mulerpq 10759 . . . 4 (([Q]β€˜π΄) Β·Q ([Q]β€˜(𝐡 +pQ 𝐢))) = ([Q]β€˜(𝐴 Β·pQ (𝐡 +pQ 𝐢)))
102 adderpq 10758 . . . 4 (([Q]β€˜(𝐴 Β·pQ 𝐡)) +Q ([Q]β€˜(𝐴 Β·pQ 𝐢))) = ([Q]β€˜((𝐴 Β·pQ 𝐡) +pQ (𝐴 Β·pQ 𝐢)))
103100, 101, 1023eqtr4g 2801 . . 3 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (([Q]β€˜π΄) Β·Q ([Q]β€˜(𝐡 +pQ 𝐢))) = (([Q]β€˜(𝐴 Β·pQ 𝐡)) +Q ([Q]β€˜(𝐴 Β·pQ 𝐢))))
104 nqerid 10735 . . . . . 6 (𝐴 ∈ Q β†’ ([Q]β€˜π΄) = 𝐴)
105104eqcomd 2742 . . . . 5 (𝐴 ∈ Q β†’ 𝐴 = ([Q]β€˜π΄))
1061053ad2ant1 1133 . . . 4 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ 𝐴 = ([Q]β€˜π΄))
107 addpqnq 10740 . . . . 5 ((𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐡 +Q 𝐢) = ([Q]β€˜(𝐡 +pQ 𝐢)))
1081073adant1 1130 . . . 4 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐡 +Q 𝐢) = ([Q]β€˜(𝐡 +pQ 𝐢)))
109106, 108oveq12d 7325 . . 3 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·Q (𝐡 +Q 𝐢)) = (([Q]β€˜π΄) Β·Q ([Q]β€˜(𝐡 +pQ 𝐢))))
110 mulpqnq 10743 . . . . 5 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q) β†’ (𝐴 Β·Q 𝐡) = ([Q]β€˜(𝐴 Β·pQ 𝐡)))
1111103adant3 1132 . . . 4 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·Q 𝐡) = ([Q]β€˜(𝐴 Β·pQ 𝐡)))
112 mulpqnq 10743 . . . . 5 ((𝐴 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·Q 𝐢) = ([Q]β€˜(𝐴 Β·pQ 𝐢)))
1131123adant2 1131 . . . 4 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·Q 𝐢) = ([Q]β€˜(𝐴 Β·pQ 𝐢)))
114111, 113oveq12d 7325 . . 3 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ ((𝐴 Β·Q 𝐡) +Q (𝐴 Β·Q 𝐢)) = (([Q]β€˜(𝐴 Β·pQ 𝐡)) +Q ([Q]β€˜(𝐴 Β·pQ 𝐢))))
115103, 109, 1143eqtr4d 2786 . 2 ((𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·Q (𝐡 +Q 𝐢)) = ((𝐴 Β·Q 𝐡) +Q (𝐴 Β·Q 𝐢)))
116 addnqf 10750 . . . 4 +Q :(Q Γ— Q)⟢Q
117116fdmi 6642 . . 3 dom +Q = (Q Γ— Q)
118 0nnq 10726 . . 3 Β¬ βˆ… ∈ Q
119 mulnqf 10751 . . . 4 Β·Q :(Q Γ— Q)⟢Q
120119fdmi 6642 . . 3 dom Β·Q = (Q Γ— Q)
121117, 118, 120ndmovdistr 7493 . 2 (Β¬ (𝐴 ∈ Q ∧ 𝐡 ∈ Q ∧ 𝐢 ∈ Q) β†’ (𝐴 Β·Q (𝐡 +Q 𝐢)) = ((𝐴 Β·Q 𝐡) +Q (𝐴 Β·Q 𝐢)))
122115, 121pm2.61i 182 1 (𝐴 Β·Q (𝐡 +Q 𝐢)) = ((𝐴 Β·Q 𝐡) +Q (𝐴 Β·Q 𝐢))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104  βŸ¨cop 4571   class class class wbr 5081   Γ— cxp 5598  Rel wrel 5605  β€˜cfv 6458  (class class class)co 7307  1st c1st 7861  2nd c2nd 7862  Ncnpi 10646   +N cpli 10647   Β·N cmi 10648   +pQ cplpq 10650   Β·pQ cmpq 10651   ~Q ceq 10653  Qcnq 10654  [Q]cerq 10656   +Q cplq 10657   Β·Q cmq 10658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-oprab 7311  df-mpo 7312  df-om 7745  df-1st 7863  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-1o 8328  df-oadd 8332  df-omul 8333  df-er 8529  df-ni 10674  df-pli 10675  df-mi 10676  df-lti 10677  df-plpq 10710  df-mpq 10711  df-enq 10713  df-nq 10714  df-erq 10715  df-plq 10716  df-mq 10717  df-1nq 10718
This theorem is referenced by:  ltaddnq  10776  halfnq  10778  addclprlem2  10819  distrlem1pr  10827  distrlem4pr  10828  prlem934  10835  prlem936  10849
  Copyright terms: Public domain W3C validator