Theorem distrnq 10956

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.

Step	Hyp	Ref	Expression
1		mulcompi 10891	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐵)) = ((1st ‘𝐵) ·N (1st ‘𝐴))
2	1	oveq1i 7419	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))
3		fvex 6905	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐵) ∈ V
4		fvex 6905	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐴) ∈ V
5		fvex 6905	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐴) ∈ V
6		mulcompi 10891	. . . . . . . . . . . . 13 ⊢ (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥)
7		mulasspi 10892	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧))
8		fvex 6905	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐶) ∈ V
9	3, 4, 5, 6, 7, 8	caov411 7639	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
10	2, 9	eqtri 2761	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
11		mulcompi 10891	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐶)) = ((1st ‘𝐶) ·N (1st ‘𝐴))
12	11	oveq1i 7419	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵)))
13		fvex 6905	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐶) ∈ V
14		fvex 6905	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐵) ∈ V
15	13, 4, 5, 6, 7, 14	caov411 7639	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
16	12, 15	eqtri 2761	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
17	10, 16	oveq12i 7421	. . . . . . . . . 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 10893	. . . . . . . . . 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 10892	. . . . . . . . . 10 ⊢ (((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 2767	. . . . . . . . 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 10892	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))))
22	14, 5, 8, 6, 7	caov12 7635	. . . . . . . . . . 11 ⊢ ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶)))
23	22	oveq2i 7420	. . . . . . . . . 10 ⊢ ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
24	21, 23	eqtri 2761	. . . . . . . . 9 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
25	20, 24	opeq12i 4879	. . . . . . . 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 10920	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))
27	26	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 ∈ (N × N))
28		xp2nd 8008	. . . . . . . . . 10 ⊢ (𝐴 ∈ (N × N) → (2nd ‘𝐴) ∈ N)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐴) ∈ N)
30		xp1st 8007	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (N × N) → (1st ‘𝐴) ∈ N)
31	27, 30	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐴) ∈ N)
32		elpqn 10920	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Q → 𝐵 ∈ (N × N))
33	32	3ad2ant2 1135	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐵 ∈ (N × N))
34		xp1st 8007	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (1st ‘𝐵) ∈ N)
35	33, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐵) ∈ N)
36		elpqn 10920	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Q → 𝐶 ∈ (N × N))
37	36	3ad2ant3 1136	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐶 ∈ (N × N))
38		xp2nd 8008	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (2nd ‘𝐶) ∈ N)
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐶) ∈ N)
40		mulclpi 10888	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
41	35, 39, 40	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
42		xp1st 8007	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (1st ‘𝐶) ∈ N)
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐶) ∈ N)
44		xp2nd 8008	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (2nd ‘𝐵) ∈ N)
45	33, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐵) ∈ N)
46		mulclpi 10888	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
47	43, 45, 46	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
48		addclpi 10887	. . . . . . . . . . 11 ⊢ ((((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N ∧ ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
49	41, 47, 48	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
50		mulclpi 10888	. . . . . . . . . 10 ⊢ (((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 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵)))) ∈ N)
52		mulclpi 10888	. . . . . . . . . . 11 ⊢ (((2nd ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
53	45, 39, 52	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
54		mulclpi 10888	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
55	29, 53, 54	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
56		mulcanenq 10955	. . . . . . . . 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 ‘𝐶)))⟩)
57	29, 51, 55, 56	syl3anc 1372	. . . . . . . 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 ‘𝐶)))⟩)
58	25, 57	eqbrtrid 5184	. . . . . . 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 10934	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
60	27, 33, 59	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
61		mulpipq2 10934	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
62	27, 37, 61	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
63	60, 62	oveq12d 7427	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) = (⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩ +pQ ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩))
64		mulclpi 10888	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐵) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
65	31, 35, 64	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
66		mulclpi 10888	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
67	29, 45, 66	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
68		mulclpi 10888	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐶) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
69	31, 43, 68	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
70		mulclpi 10888	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
71	29, 39, 70	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
72		addpipq 10932	. . . . . . . . 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 ‘𝐶)))⟩)
73	65, 67, 69, 71, 72	syl22anc 838	. . . . . . . 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 ‘𝐶)))⟩)
74	63, 73	eqtrd 2773	. . . . . . 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 5695	. . . . . . . . . 10 ⊢ Rel (N × N)
76		1st2nd 8025	. . . . . . . . . 10 ⊢ ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
77	75, 27, 76	sylancr 588	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
78		addpipq2 10931	. . . . . . . . . 10 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
79	33, 37, 78	syl2anc 585	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
80	77, 79	oveq12d 7427	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) = (⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ·pQ ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩))
81		mulpipq 10935	. . . . . . . . 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 ‘𝐶)))⟩)
82	31, 29, 49, 53, 81	syl22anc 838	. . . . . . . 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 ‘𝐶)))⟩)
83	80, 82	eqtrd 2773	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) = ⟨((1st ‘𝐴) ·N (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵)))), ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶)))⟩)
84	58, 74, 83	3brtr4d 5181	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)))
85		mulpqf 10941	. . . . . . . . . 10 ⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
86	85	fovcl 7537	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) ∈ (N × N))
87	27, 33, 86	syl2anc 585	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) ∈ (N × N))
88	85	fovcl 7537	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) ∈ (N × N))
89	27, 37, 88	syl2anc 585	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) ∈ (N × N))
90		addpqf 10939	. . . . . . . . 9 ⊢ +pQ :((N × N) × (N × N))⟶(N × N)
91	90	fovcl 7537	. . . . . . . 8 ⊢ (((𝐴 ·pQ 𝐵) ∈ (N × N) ∧ (𝐴 ·pQ 𝐶) ∈ (N × N)) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
92	87, 89, 91	syl2anc 585	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
93	90	fovcl 7537	. . . . . . . . 9 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) ∈ (N × N))
94	33, 37, 93	syl2anc 585	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) ∈ (N × N))
95	85	fovcl 7537	. . . . . . . 8 ⊢ ((𝐴 ∈ (N × N) ∧ (𝐵 +pQ 𝐶) ∈ (N × N)) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
96	27, 94, 95	syl2anc 585	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
97		nqereq 10930	. . . . . . 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 585	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)) ↔ ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))))
99	84, 98	mpbid 231	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))))
100	99	eqcomd 2739	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))))
101		mulerpq 10952	. . . 4 ⊢ (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))
102		adderpq 10951	. . . 4 ⊢ (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)))
103	100, 101, 102	3eqtr4g 2798	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
104		nqerid 10928	. . . . . 6 ⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴)
105	104	eqcomd 2739	. . . . 5 ⊢ (𝐴 ∈ Q → 𝐴 = ([Q]‘𝐴))
106	105	3ad2ant1 1134	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ([Q]‘𝐴))
107		addpqnq 10933	. . . . 5 ⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
108	107	3adant1 1131	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
109	106, 108	oveq12d 7427	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))))
110		mulpqnq 10936	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
111	110	3adant3 1133	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
112		mulpqnq 10936	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
113	112	3adant2 1132	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
114	111, 113	oveq12d 7427	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
115	103, 109, 114	3eqtr4d 2783	. 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
116		addnqf 10943	. . . 4 ⊢ +Q :(Q × Q)⟶Q
117	116	fdmi 6730	. . 3 ⊢ dom +Q = (Q × Q)
118		0nnq 10919	. . 3 ⊢ ¬ ∅ ∈ Q
119		mulnqf 10944	. . . 4 ⊢ ·Q :(Q × Q)⟶Q
120	119	fdmi 6730	. . 3 ⊢ dom ·Q = (Q × Q)
121	117, 118, 120	ndmovdistr 7596	. 2 ⊢ (¬ (𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
122	115, 121	pm2.61i 182	1 ⊢ (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶))

Syntax hints:   ↔ wb 205   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ⟨cop 4635   class class class wbr 5149   × cxp 5675  Rel wrel 5682  ‘cfv 6544  (class class class)co 7409  1^st c1st 7973  2^nd c2nd 7974  Ncnpi 10839   +_N cpli 10840   ·_N cmi 10841   +_pQ cplpq 10843   ·_pQ cmpq 10844   ~_Q ceq 10846  Qcnq 10847  [Q]cerq 10849   +_Q cplq 10850   ·_Q cmq 10851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-omul 8471  df-er 8703  df-ni 10867  df-pli 10868  df-mi 10869  df-lti 10870  df-plpq 10903  df-mpq 10904  df-enq 10906  df-nq 10907  df-erq 10908  df-plq 10909  df-mq 10910  df-1nq 10911

This theorem is referenced by:  ltaddnq  10969  halfnq  10971  addclprlem2  11012  distrlem1pr  11020  distrlem4pr  11021  prlem934  11028  prlem936  11042