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 𝐶 ) )