Metamath Proof Explorer

Theorem distrnq

Description: Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion distrnq ( 𝐴 ·Q ( 𝐵 +Q 𝐶 ) ) = ( ( 𝐴 ·Q 𝐵 ) +Q ( 𝐴 ·Q 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mulcompi ⊢ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) = ( ( 1st ‘ 𝐵 ) ·N ( 1st ‘ 𝐴 ) )
2 1 oveq1i ⊢ ( ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 1st ‘ 𝐵 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) )
3 fvex ⊢ ( 1st ‘ 𝐵 ) ∈ V
4 fvex ⊢ ( 1st ‘ 𝐴 ) ∈ V
5 fvex ⊢ ( 2nd ‘ 𝐴 ) ∈ V
6 mulcompi ⊢ ( 𝑥 ·N 𝑦 ) = ( 𝑦 ·N 𝑥 )
7 mulasspi ⊢ ( ( 𝑥 ·N 𝑦 ) ·N 𝑧 ) = ( 𝑥 ·N ( 𝑦 ·N 𝑧 ) )
8 fvex ⊢ ( 2nd ‘ 𝐶 ) ∈ V
9 3 4 5 6 7 8 caov411 ⊢ ( ( ( 1st ‘ 𝐵 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
10 2 9 eqtri ⊢ ( ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
11 mulcompi ⊢ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) = ( ( 1st ‘ 𝐶 ) ·N ( 1st ‘ 𝐴 ) )
12 11 oveq1i ⊢ ( ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 1st ‘ 𝐶 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) )
13 fvex ⊢ ( 1st ‘ 𝐶 ) ∈ V
14 fvex ⊢ ( 2nd ‘ 𝐵 ) ∈ V
15 13 4 5 6 7 14 caov411 ⊢ ( ( ( 1st ‘ 𝐶 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) )
16 12 15 eqtri ⊢ ( ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) )
17 10 16 oveq12i ⊢ ( ( ( ( 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 ⊢ ( ( ( 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 ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐴 ) ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) )
20 17 18 19 3eqtr2i ⊢ ( ( ( ( 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 ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) )
22 14 5 8 6 7 caov12 ⊢ ( ( 2nd ‘ 𝐵 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) )
23 22 oveq2i ⊢ ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) )
24 21 23 eqtri ⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) )
25 20 24 opeq12i ⊢ ⟨ ( ( ( ( 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 ⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
27 26 3ad2ant1 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐴 ∈ ( N × N ) )
28 xp2nd ⊢ ( 𝐴 ∈ ( N × N ) → ( 2nd ‘ 𝐴 ) ∈ N )
29 27 28 syl ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 2nd ‘ 𝐴 ) ∈ N )
30 xp1st ⊢ ( 𝐴 ∈ ( N × N ) → ( 1st ‘ 𝐴 ) ∈ N )
31 27 30 syl ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 1st ‘ 𝐴 ) ∈ N )
32 elpqn ⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
33 32 3ad2ant2 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐵 ∈ ( N × N ) )
34 xp1st ⊢ ( 𝐵 ∈ ( N × N ) → ( 1st ‘ 𝐵 ) ∈ N )
35 33 34 syl ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 1st ‘ 𝐵 ) ∈ N )
36 elpqn ⊢ ( 𝐶 ∈ Q → 𝐶 ∈ ( N × N ) )
37 36 3ad2ant3 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐶 ∈ ( N × N ) )
38 xp2nd ⊢ ( 𝐶 ∈ ( N × N ) → ( 2nd ‘ 𝐶 ) ∈ N )
39 37 38 syl ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 2nd ‘ 𝐶 ) ∈ N )
40 mulclpi ⊢ ( ( ( 1st ‘ 𝐵 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
41 35 39 40 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
42 xp1st ⊢ ( 𝐶 ∈ ( N × N ) → ( 1st ‘ 𝐶 ) ∈ N )
43 37 42 syl ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 1st ‘ 𝐶 ) ∈ N )
44 xp2nd ⊢ ( 𝐵 ∈ ( N × N ) → ( 2nd ‘ 𝐵 ) ∈ N )
45 33 44 syl ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 2nd ‘ 𝐵 ) ∈ N )
46 mulclpi ⊢ ( ( ( 1st ‘ 𝐶 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
47 43 45 46 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
48 addclpi ⊢ ( ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ∧ ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ) → ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
49 41 47 48 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N )
50 mulclpi ⊢ ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ∈ N ) → ( ( 1st ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) ∈ N )
51 31 49 50 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 1st ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) ∈ N )
52 mulclpi ⊢ ( ( ( 2nd ‘ 𝐵 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
53 45 39 52 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
54 mulclpi ⊢ ( ( ( 2nd ‘ 𝐴 ) ∈ N ∧ ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) ∈ N )
55 29 53 54 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) ∈ N )
56 mulcanenq ⊢ ( ( ( 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 ‘ 𝐶 ) ) ) ⟩ )
57 29 51 55 56 syl3anc ⊢ ( ( 𝐴 ∈ 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 ‘ 𝐶 ) ) ) ⟩ )
58 25 57 eqbrtrid ⊢ ( ( 𝐴 ∈ 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 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐵 ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ )
60 27 33 59 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ 𝐵 ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ )
61 mulpipq2 ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐶 ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
62 27 37 61 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ 𝐶 ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
63 60 62 oveq12d ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) = ( ⟨ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ +pQ ⟨ ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ) )
64 mulclpi ⊢ ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 1st ‘ 𝐵 ) ∈ N ) → ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) ∈ N )
65 31 35 64 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) ∈ N )
66 mulclpi ⊢ ( ( ( 2nd ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
67 29 45 66 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
68 mulclpi ⊢ ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 1st ‘ 𝐶 ) ∈ N ) → ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) ∈ N )
69 31 43 68 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 1st ‘ 𝐴 ) ·N ( 1st ‘ 𝐶 ) ) ∈ N )
70 mulclpi ⊢ ( ( ( 2nd ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐶 ) ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
71 29 39 70 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐶 ) ) ∈ N )
72 addpipq ⊢ ( ( ( ( ( 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 ‘ 𝐶 ) ) ) ⟩ )
73 65 67 69 71 72 syl22anc ⊢ ( ( 𝐴 ∈ 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 ‘ 𝐶 ) ) ) ⟩ )
74 63 73 eqtrd ⊢ ( ( 𝐴 ∈ 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 ⊢ Rel ( N × N )
76 1st2nd ⊢ ( ( Rel ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
77 75 27 76 sylancr ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
78 addpipq2 ⊢ ( ( 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐵 +pQ 𝐶 ) = ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
79 33 37 78 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐵 +pQ 𝐶 ) = ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ )
80 77 79 oveq12d ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) = ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ·pQ ⟨ ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) , ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ⟩ ) )
81 mulpipq ⊢ ( ( ( ( 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 ‘ 𝐶 ) ) ) ⟩ )
82 31 29 49 53 81 syl22anc ⊢ ( ( 𝐴 ∈ 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 ‘ 𝐶 ) ) ) ⟩ )
83 80 82 eqtrd ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) = ⟨ ( ( 1st ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) +N ( ( 1st ‘ 𝐶 ) ·N ( 2nd ‘ 𝐵 ) ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐵 ) ·N ( 2nd ‘ 𝐶 ) ) ) ⟩ )
84 58 74 83 3brtr4d ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ~Q ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) )
85 mulpqf ⊢ ·pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )
86 85 fovcl ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐵 ) ∈ ( N × N ) )
87 27 33 86 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ 𝐵 ) ∈ ( N × N ) )
88 85 fovcl ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐴 ·pQ 𝐶 ) ∈ ( N × N ) )
89 27 37 88 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ 𝐶 ) ∈ ( N × N ) )
90 addpqf ⊢ +pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )
91 90 fovcl ⊢ ( ( ( 𝐴 ·pQ 𝐵 ) ∈ ( N × N ) ∧ ( 𝐴 ·pQ 𝐶 ) ∈ ( N × N ) ) → ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ∈ ( N × N ) )
92 87 89 91 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ∈ ( N × N ) )
93 90 fovcl ⊢ ( ( 𝐵 ∈ ( N × N ) ∧ 𝐶 ∈ ( N × N ) ) → ( 𝐵 +pQ 𝐶 ) ∈ ( N × N ) )
94 33 37 93 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐵 +pQ 𝐶 ) ∈ ( N × N ) )
95 85 fovcl ⊢ ( ( 𝐴 ∈ ( N × N ) ∧ ( 𝐵 +pQ 𝐶 ) ∈ ( N × N ) ) → ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) ∈ ( N × N ) )
96 27 94 95 syl2anc ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) ∈ ( N × N ) )
97 nqereq ⊢ ( ( ( ( 𝐴 ·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 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ~Q ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) ↔ ( [Q] ‘ ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ) = ( [Q] ‘ ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) ) ) )
99 84 98 mpbid ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( [Q] ‘ ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ) = ( [Q] ‘ ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) ) )
100 99 eqcomd ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( [Q] ‘ ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) ) = ( [Q] ‘ ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) ) )
101 mulerpq ⊢ ( ( [Q] ‘ 𝐴 ) ·Q ( [Q] ‘ ( 𝐵 +pQ 𝐶 ) ) ) = ( [Q] ‘ ( 𝐴 ·pQ ( 𝐵 +pQ 𝐶 ) ) )
102 adderpq ⊢ ( ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) +Q ( [Q] ‘ ( 𝐴 ·pQ 𝐶 ) ) ) = ( [Q] ‘ ( ( 𝐴 ·pQ 𝐵 ) +pQ ( 𝐴 ·pQ 𝐶 ) ) )
103 100 101 102 3eqtr4g ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( [Q] ‘ 𝐴 ) ·Q ( [Q] ‘ ( 𝐵 +pQ 𝐶 ) ) ) = ( ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) +Q ( [Q] ‘ ( 𝐴 ·pQ 𝐶 ) ) ) )
104 nqerid ⊢ ( 𝐴 ∈ Q → ( [Q] ‘ 𝐴 ) = 𝐴 )
105 104 eqcomd ⊢ ( 𝐴 ∈ Q → 𝐴 = ( [Q] ‘ 𝐴 ) )
106 105 3ad2ant1 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → 𝐴 = ( [Q] ‘ 𝐴 ) )
107 addpqnq ⊢ ( ( 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐵 +Q 𝐶 ) = ( [Q] ‘ ( 𝐵 +pQ 𝐶 ) ) )
108 107 3adant1 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐵 +Q 𝐶 ) = ( [Q] ‘ ( 𝐵 +pQ 𝐶 ) ) )
109 106 108 oveq12d ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·Q ( 𝐵 +Q 𝐶 ) ) = ( ( [Q] ‘ 𝐴 ) ·Q ( [Q] ‘ ( 𝐵 +pQ 𝐶 ) ) ) )
110 mulpqnq ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) )
111 110 3adant3 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·Q 𝐵 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) )
112 mulpqnq ⊢ ( ( 𝐴 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·Q 𝐶 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐶 ) ) )
113 112 3adant2 ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·Q 𝐶 ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐶 ) ) )
114 111 113 oveq12d ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( ( 𝐴 ·Q 𝐵 ) +Q ( 𝐴 ·Q 𝐶 ) ) = ( ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) ) +Q ( [Q] ‘ ( 𝐴 ·pQ 𝐶 ) ) ) )
115 103 109 114 3eqtr4d ⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·Q ( 𝐵 +Q 𝐶 ) ) = ( ( 𝐴 ·Q 𝐵 ) +Q ( 𝐴 ·Q 𝐶 ) ) )
116 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
117 116 fdmi ⊢ dom +Q = ( Q × Q )
118 0nnq ⊢ ¬ ∅ ∈ Q
119 mulnqf ⊢ ·Q : ( Q × Q ) ⟶ Q
120 119 fdmi ⊢ dom ·Q = ( Q × Q )
121 117 118 120 ndmovdistr ⊢ ( ¬ ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐴 ·Q ( 𝐵 +Q 𝐶 ) ) = ( ( 𝐴 ·Q 𝐵 ) +Q ( 𝐴 ·Q 𝐶 ) ) )
122 115 121 pm2.61i ⊢ ( 𝐴 ·Q ( 𝐵 +Q 𝐶 ) ) = ( ( 𝐴 ·Q 𝐵 ) +Q ( 𝐴 ·Q 𝐶 ) )