Theorem distrnq 11030

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 10965	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐵)) = ((1st ‘𝐵) ·N (1st ‘𝐴))
2	1	oveq1i 7458	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))
3		fvex 6933	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐵) ∈ V
4		fvex 6933	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐴) ∈ V
5		fvex 6933	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐴) ∈ V
6		mulcompi 10965	. . . . . . . . . . . . 13 ⊢ (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥)
7		mulasspi 10966	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧))
8		fvex 6933	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐶) ∈ V
9	3, 4, 5, 6, 7, 8	caov411 7682	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
10	2, 9	eqtri 2768	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
11		mulcompi 10965	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐶)) = ((1st ‘𝐶) ·N (1st ‘𝐴))
12	11	oveq1i 7458	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵)))
13		fvex 6933	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐶) ∈ V
14		fvex 6933	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐵) ∈ V
15	13, 4, 5, 6, 7, 14	caov411 7682	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
16	12, 15	eqtri 2768	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
17	10, 16	oveq12i 7460	. . . . . . . . . 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 10967	. . . . . . . . . 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 10966	. . . . . . . . . 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 2774	. . . . . . . . 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 10966	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))))
22	14, 5, 8, 6, 7	caov12 7678	. . . . . . . . . . 11 ⊢ ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶)))
23	22	oveq2i 7459	. . . . . . . . . 10 ⊢ ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
24	21, 23	eqtri 2768	. . . . . . . . 9 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
25	20, 24	opeq12i 4902	. . . . . . . 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 10994	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))
27	26	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 ∈ (N × N))
28		xp2nd 8063	. . . . . . . . . 10 ⊢ (𝐴 ∈ (N × N) → (2nd ‘𝐴) ∈ N)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐴) ∈ N)
30		xp1st 8062	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (N × N) → (1st ‘𝐴) ∈ N)
31	27, 30	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐴) ∈ N)
32		elpqn 10994	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Q → 𝐵 ∈ (N × N))
33	32	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐵 ∈ (N × N))
34		xp1st 8062	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (1st ‘𝐵) ∈ N)
35	33, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐵) ∈ N)
36		elpqn 10994	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Q → 𝐶 ∈ (N × N))
37	36	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐶 ∈ (N × N))
38		xp2nd 8063	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (2nd ‘𝐶) ∈ N)
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐶) ∈ N)
40		mulclpi 10962	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
41	35, 39, 40	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
42		xp1st 8062	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (1st ‘𝐶) ∈ N)
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐶) ∈ N)
44		xp2nd 8063	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (2nd ‘𝐵) ∈ N)
45	33, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐵) ∈ N)
46		mulclpi 10962	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
47	43, 45, 46	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
48		addclpi 10961	. . . . . . . . . . 11 ⊢ ((((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N ∧ ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
49	41, 47, 48	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
50		mulclpi 10962	. . . . . . . . . 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 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵)))) ∈ N)
52		mulclpi 10962	. . . . . . . . . . 11 ⊢ (((2nd ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
53	45, 39, 52	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
54		mulclpi 10962	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
55	29, 53, 54	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
56		mulcanenq 11029	. . . . . . . . 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 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 ‘𝐶)))⟩)
58	25, 57	eqbrtrid 5201	. . . . . . 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 11008	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
60	27, 33, 59	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
61		mulpipq2 11008	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
62	27, 37, 61	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
63	60, 62	oveq12d 7466	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) = (⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩ +pQ ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩))
64		mulclpi 10962	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐵) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
65	31, 35, 64	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
66		mulclpi 10962	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
67	29, 45, 66	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
68		mulclpi 10962	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐶) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
69	31, 43, 68	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
70		mulclpi 10962	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
71	29, 39, 70	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
72		addpipq 11006	. . . . . . . . 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 2780	. . . . . . 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 5718	. . . . . . . . . 10 ⊢ Rel (N × N)
76		1st2nd 8080	. . . . . . . . . 10 ⊢ ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
77	75, 27, 76	sylancr 586	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
78		addpipq2 11005	. . . . . . . . . 10 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
79	33, 37, 78	syl2anc 583	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
80	77, 79	oveq12d 7466	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) = (⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ·pQ ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩))
81		mulpipq 11009	. . . . . . . . 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 2780	. . . . . . 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 5198	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)))
85		mulpqf 11015	. . . . . . . . . 10 ⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
86	85	fovcl 7578	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) ∈ (N × N))
87	27, 33, 86	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) ∈ (N × N))
88	85	fovcl 7578	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) ∈ (N × N))
89	27, 37, 88	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) ∈ (N × N))
90		addpqf 11013	. . . . . . . . 9 ⊢ +pQ :((N × N) × (N × N))⟶(N × N)
91	90	fovcl 7578	. . . . . . . 8 ⊢ (((𝐴 ·pQ 𝐵) ∈ (N × N) ∧ (𝐴 ·pQ 𝐶) ∈ (N × N)) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
92	87, 89, 91	syl2anc 583	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
93	90	fovcl 7578	. . . . . . . . 9 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) ∈ (N × N))
94	33, 37, 93	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) ∈ (N × N))
95	85	fovcl 7578	. . . . . . . 8 ⊢ ((𝐴 ∈ (N × N) ∧ (𝐵 +pQ 𝐶) ∈ (N × N)) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
96	27, 94, 95	syl2anc 583	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
97		nqereq 11004	. . . . . . 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 583	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)) ↔ ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))))
99	84, 98	mpbid 232	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))))
100	99	eqcomd 2746	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))))
101		mulerpq 11026	. . . 4 ⊢ (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))
102		adderpq 11025	. . . 4 ⊢ (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)))
103	100, 101, 102	3eqtr4g 2805	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
104		nqerid 11002	. . . . . 6 ⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴)
105	104	eqcomd 2746	. . . . 5 ⊢ (𝐴 ∈ Q → 𝐴 = ([Q]‘𝐴))
106	105	3ad2ant1 1133	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ([Q]‘𝐴))
107		addpqnq 11007	. . . . 5 ⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
108	107	3adant1 1130	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
109	106, 108	oveq12d 7466	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))))
110		mulpqnq 11010	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
111	110	3adant3 1132	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
112		mulpqnq 11010	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
113	112	3adant2 1131	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
114	111, 113	oveq12d 7466	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
115	103, 109, 114	3eqtr4d 2790	. 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
116		addnqf 11017	. . . 4 ⊢ +Q :(Q × Q)⟶Q
117	116	fdmi 6758	. . 3 ⊢ dom +Q = (Q × Q)
118		0nnq 10993	. . 3 ⊢ ¬ ∅ ∈ Q
119		mulnqf 11018	. . . 4 ⊢ ·Q :(Q × Q)⟶Q
120	119	fdmi 6758	. . 3 ⊢ dom ·Q = (Q × Q)
121	117, 118, 120	ndmovdistr 7639	. 2 ⊢ (¬ (𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
122	115, 121	pm2.61i 182	1 ⊢ (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶))

Syntax hints:   ↔ wb 206   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ⟨cop 4654   class class class wbr 5166   × cxp 5698  Rel wrel 5705  ‘cfv 6573  (class class class)co 7448  1^st c1st 8028  2^nd c2nd 8029  Ncnpi 10913   +_N cpli 10914   ·_N cmi 10915   +_pQ cplpq 10917   ·_pQ cmpq 10918   ~_Q ceq 10920  Qcnq 10921  [Q]cerq 10923   +_Q cplq 10924   ·_Q cmq 10925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-oadd 8526  df-omul 8527  df-er 8763  df-ni 10941  df-pli 10942  df-mi 10943  df-lti 10944  df-plpq 10977  df-mpq 10978  df-enq 10980  df-nq 10981  df-erq 10982  df-plq 10983  df-mq 10984  df-1nq 10985

This theorem is referenced by:  ltaddnq  11043  halfnq  11045  addclprlem2  11086  distrlem1pr  11094  distrlem4pr  11095  prlem934  11102  prlem936  11116