Theorem distrnq 11070

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 11005	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐵)) = ((1st ‘𝐵) ·N (1st ‘𝐴))
2	1	oveq1i 7450	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))
3		fvex 6918	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐵) ∈ V
4		fvex 6918	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐴) ∈ V
5		fvex 6918	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐴) ∈ V
6		mulcompi 11005	. . . . . . . . . . . . 13 ⊢ (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥)
7		mulasspi 11006	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧))
8		fvex 6918	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐶) ∈ V
9	3, 4, 5, 6, 7, 8	caov411 7674	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
10	2, 9	eqtri 2786	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
11		mulcompi 11005	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐶)) = ((1st ‘𝐶) ·N (1st ‘𝐴))
12	11	oveq1i 7450	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵)))
13		fvex 6918	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐶) ∈ V
14		fvex 6918	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐵) ∈ V
15	13, 4, 5, 6, 7, 14	caov411 7674	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
16	12, 15	eqtri 2786	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
17	10, 16	oveq12i 7452	. . . . . . . . . 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 11007	. . . . . . . . . 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 11006	. . . . . . . . . 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 2792	. . . . . . . . 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 11006	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))))
22	14, 5, 8, 6, 7	caov12 7670	. . . . . . . . . . 11 ⊢ ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶)))
23	22	oveq2i 7451	. . . . . . . . . 10 ⊢ ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
24	21, 23	eqtri 2786	. . . . . . . . 9 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
25	20, 24	opeq12i 4848	. . . . . . . 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 11034	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))
27	26	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 ∈ (N × N))
28		xp2nd 8055	. . . . . . . . . 10 ⊢ (𝐴 ∈ (N × N) → (2nd ‘𝐴) ∈ N)
29	27, 28	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐴) ∈ N)
30		xp1st 8054	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (N × N) → (1st ‘𝐴) ∈ N)
31	27, 30	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐴) ∈ N)
32		elpqn 11034	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Q → 𝐵 ∈ (N × N))
33	32	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐵 ∈ (N × N))
34		xp1st 8054	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (1st ‘𝐵) ∈ N)
35	33, 34	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐵) ∈ N)
36		elpqn 11034	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Q → 𝐶 ∈ (N × N))
37	36	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐶 ∈ (N × N))
38		xp2nd 8055	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (2nd ‘𝐶) ∈ N)
39	37, 38	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐶) ∈ N)
40		mulclpi 11002	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
41	35, 39, 40	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
42		xp1st 8054	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (1st ‘𝐶) ∈ N)
43	37, 42	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐶) ∈ N)
44		xp2nd 8055	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (2nd ‘𝐵) ∈ N)
45	33, 44	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐵) ∈ N)
46		mulclpi 11002	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
47	43, 45, 46	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
48		addclpi 11001	. . . . . . . . . . 11 ⊢ ((((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N ∧ ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
49	41, 47, 48	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
50		mulclpi 11002	. . . . . . . . . 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 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵)))) ∈ N)
52		mulclpi 11002	. . . . . . . . . . 11 ⊢ (((2nd ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
53	45, 39, 52	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
54		mulclpi 11002	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
55	29, 53, 54	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
56		mulcanenq 11069	. . . . . . . . 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 1399	. . . . . . . 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 5143	. . . . . . 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 11048	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
60	27, 33, 59	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
61		mulpipq2 11048	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
62	27, 37, 61	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
63	60, 62	oveq12d 7458	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) = (⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩ +pQ ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩))
64		mulclpi 11002	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐵) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
65	31, 35, 64	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
66		mulclpi 11002	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
67	29, 45, 66	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
68		mulclpi 11002	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐶) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
69	31, 43, 68	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
70		mulclpi 11002	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
71	29, 39, 70	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
72		addpipq 11046	. . . . . . . . 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 852	. . . . . . . 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 2798	. . . . . . 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 5673	. . . . . . . . . 10 ⊢ Rel (N × N)
76		1st2nd 8071	. . . . . . . . . 10 ⊢ ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
77	75, 27, 76	sylancr 599	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
78		addpipq2 11045	. . . . . . . . . 10 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
79	33, 37, 78	syl2anc 596	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
80	77, 79	oveq12d 7458	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) = (⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ·pQ ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩))
81		mulpipq 11049	. . . . . . . . 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 852	. . . . . . . 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 2798	. . . . . . 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 5140	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)))
85		mulpqf 11055	. . . . . . . . . 10 ⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
86	85	fovcl 7568	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) ∈ (N × N))
87	27, 33, 86	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) ∈ (N × N))
88	85	fovcl 7568	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) ∈ (N × N))
89	27, 37, 88	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) ∈ (N × N))
90		addpqf 11053	. . . . . . . . 9 ⊢ +pQ :((N × N) × (N × N))⟶(N × N)
91	90	fovcl 7568	. . . . . . . 8 ⊢ (((𝐴 ·pQ 𝐵) ∈ (N × N) ∧ (𝐴 ·pQ 𝐶) ∈ (N × N)) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
92	87, 89, 91	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
93	90	fovcl 7568	. . . . . . . . 9 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) ∈ (N × N))
94	33, 37, 93	syl2anc 596	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) ∈ (N × N))
95	85	fovcl 7568	. . . . . . . 8 ⊢ ((𝐴 ∈ (N × N) ∧ (𝐵 +pQ 𝐶) ∈ (N × N)) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
96	27, 94, 95	syl2anc 596	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
97		nqereq 11044	. . . . . . 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 596	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)) ↔ ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))))
99	84, 98	mpbid 235	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))))
100	99	eqcomd 2769	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))))
101		mulerpq 11066	. . . 4 ⊢ (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))
102		adderpq 11065	. . . 4 ⊢ (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)))
103	100, 101, 102	3eqtr4g 2823	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
104		nqerid 11042	. . . . . 6 ⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴)
105	104	eqcomd 2769	. . . . 5 ⊢ (𝐴 ∈ Q → 𝐴 = ([Q]‘𝐴))
106	105	3ad2ant1 1151	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ([Q]‘𝐴))
107		addpqnq 11047	. . . . 5 ⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
108	107	3adant1 1148	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
109	106, 108	oveq12d 7458	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))))
110		mulpqnq 11050	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
111	110	3adant3 1150	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
112		mulpqnq 11050	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
113	112	3adant2 1149	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
114	111, 113	oveq12d 7458	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
115	103, 109, 114	3eqtr4d 2808	. 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
116		addnqf 11057	. . . 4 ⊢ +Q :(Q × Q)⟶Q
117	116	fdmi 6740	. . 3 ⊢ dom +Q = (Q × Q)
118		0nnq 11033	. . 3 ⊢ ¬ ∅ ∈ Q
119		mulnqf 11058	. . . 4 ⊢ ·Q :(Q × Q)⟶Q
120	119	fdmi 6740	. . 3 ⊢ dom ·Q = (Q × Q)
121	117, 118, 120	ndmovdistr 7631	. 2 ⊢ (¬ (𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
122	115, 121	pm2.61i 184	1 ⊢ (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶))

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ⟨cop 4838   class class class wbr 5106   × cxp 5653  Rel wrel 5660  ‘cfv 6555  (class class class)co 7440  1^st c1st 8020  2^nd c2nd 8021  Ncnpi 10953   +_N cpli 10954   ·_N cmi 10955   +_pQ cplpq 10957   ·_pQ cmpq 10958   ~_Q ceq 10960  Qcnq 10961  [Q]cerq 10963   +_Q cplq 10964   ·_Q cmq 10965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-oadd 8505  df-omul 8506  df-er 8742  df-ni 10981  df-pli 10982  df-mi 10983  df-lti 10984  df-plpq 11017  df-mpq 11018  df-enq 11020  df-nq 11021  df-erq 11022  df-plq 11023  df-mq 11024  df-1nq 11025

This theorem is used by:  ltaddnq  11083  halfnq  11085  addclprlem2  11126  distrlem1pr  11134  distrlem4pr  11135  prlem934  11142  prlem936  11156