Theorem distrnq 11002

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 10937	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐵)) = ((1st ‘𝐵) ·N (1st ‘𝐴))
2	1	oveq1i 7442	. . . . . . . . . . . 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 10937	. . . . . . . . . . . . 13 ⊢ (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥)
7		mulasspi 10938	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧))
8		fvex 6918	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐶) ∈ V
9	3, 4, 5, 6, 7, 8	caov411 7666	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
10	2, 9	eqtri 2764	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
11		mulcompi 10937	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐶)) = ((1st ‘𝐶) ·N (1st ‘𝐴))
12	11	oveq1i 7442	. . . . . . . . . . . 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 7666	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
16	12, 15	eqtri 2764	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
17	10, 16	oveq12i 7444	. . . . . . . . . 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 10939	. . . . . . . . . 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 10938	. . . . . . . . . 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 2770	. . . . . . . . 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 10938	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))))
22	14, 5, 8, 6, 7	caov12 7662	. . . . . . . . . . 11 ⊢ ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶)))
23	22	oveq2i 7443	. . . . . . . . . 10 ⊢ ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
24	21, 23	eqtri 2764	. . . . . . . . 9 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
25	20, 24	opeq12i 4877	. . . . . . . 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 10966	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))
27	26	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 ∈ (N × N))
28		xp2nd 8048	. . . . . . . . . 10 ⊢ (𝐴 ∈ (N × N) → (2nd ‘𝐴) ∈ N)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐴) ∈ N)
30		xp1st 8047	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (N × N) → (1st ‘𝐴) ∈ N)
31	27, 30	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐴) ∈ N)
32		elpqn 10966	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Q → 𝐵 ∈ (N × N))
33	32	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐵 ∈ (N × N))
34		xp1st 8047	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (1st ‘𝐵) ∈ N)
35	33, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐵) ∈ N)
36		elpqn 10966	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Q → 𝐶 ∈ (N × N))
37	36	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐶 ∈ (N × N))
38		xp2nd 8048	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (2nd ‘𝐶) ∈ N)
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐶) ∈ N)
40		mulclpi 10934	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
41	35, 39, 40	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
42		xp1st 8047	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (1st ‘𝐶) ∈ N)
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐶) ∈ N)
44		xp2nd 8048	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (2nd ‘𝐵) ∈ N)
45	33, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐵) ∈ N)
46		mulclpi 10934	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
47	43, 45, 46	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N)
48		addclpi 10933	. . . . . . . . . . 11 ⊢ ((((1st ‘𝐵) ·N (2nd ‘𝐶)) ∈ N ∧ ((1st ‘𝐶) ·N (2nd ‘𝐵)) ∈ N) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
49	41, 47, 48	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))) ∈ N)
50		mulclpi 10934	. . . . . . . . . 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 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵)))) ∈ N)
52		mulclpi 10934	. . . . . . . . . . 11 ⊢ (((2nd ‘𝐵) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
53	45, 39, 52	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N)
54		mulclpi 10934	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ ((2nd ‘𝐵) ·N (2nd ‘𝐶)) ∈ N) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
55	29, 53, 54	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))) ∈ N)
56		mulcanenq 11001	. . . . . . . . 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 5177	. . . . . . 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 10980	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
60	27, 33, 59	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
61		mulpipq2 10980	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
62	27, 37, 61	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) = ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩)
63	60, 62	oveq12d 7450	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) = (⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩ +pQ ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩))
64		mulclpi 10934	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐵) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
65	31, 35, 64	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐵)) ∈ N)
66		mulclpi 10934	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐵) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
67	29, 45, 66	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐵)) ∈ N)
68		mulclpi 10934	. . . . . . . . . 10 ⊢ (((1st ‘𝐴) ∈ N ∧ (1st ‘𝐶) ∈ N) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
69	31, 43, 68	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((1st ‘𝐴) ·N (1st ‘𝐶)) ∈ N)
70		mulclpi 10934	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ∈ N ∧ (2nd ‘𝐶) ∈ N) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
71	29, 39, 70	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((2nd ‘𝐴) ·N (2nd ‘𝐶)) ∈ N)
72		addpipq 10978	. . . . . . . . 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 2776	. . . . . . 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 5702	. . . . . . . . . 10 ⊢ Rel (N × N)
76		1st2nd 8065	. . . . . . . . . 10 ⊢ ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
77	75, 27, 76	sylancr 587	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
78		addpipq2 10977	. . . . . . . . . 10 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
79	33, 37, 78	syl2anc 584	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) = ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩)
80	77, 79	oveq12d 7450	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) = (⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ·pQ ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩))
81		mulpipq 10981	. . . . . . . . 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 2776	. . . . . . 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 5174	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)))
85		mulpqf 10987	. . . . . . . . . 10 ⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
86	85	fovcl 7562	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) ∈ (N × N))
87	27, 33, 86	syl2anc 584	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) ∈ (N × N))
88	85	fovcl 7562	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) ∈ (N × N))
89	27, 37, 88	syl2anc 584	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) ∈ (N × N))
90		addpqf 10985	. . . . . . . . 9 ⊢ +pQ :((N × N) × (N × N))⟶(N × N)
91	90	fovcl 7562	. . . . . . . 8 ⊢ (((𝐴 ·pQ 𝐵) ∈ (N × N) ∧ (𝐴 ·pQ 𝐶) ∈ (N × N)) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
92	87, 89, 91	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ∈ (N × N))
93	90	fovcl 7562	. . . . . . . . 9 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) ∈ (N × N))
94	33, 37, 93	syl2anc 584	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) ∈ (N × N))
95	85	fovcl 7562	. . . . . . . 8 ⊢ ((𝐴 ∈ (N × N) ∧ (𝐵 +pQ 𝐶) ∈ (N × N)) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
96	27, 94, 95	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) ∈ (N × N))
97		nqereq 10976	. . . . . . 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 584	. . . . . 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 2742	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))))
101		mulerpq 10998	. . . 4 ⊢ (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))
102		adderpq 10997	. . . 4 ⊢ (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)))
103	100, 101, 102	3eqtr4g 2801	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
104		nqerid 10974	. . . . . 6 ⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴)
105	104	eqcomd 2742	. . . . 5 ⊢ (𝐴 ∈ Q → 𝐴 = ([Q]‘𝐴))
106	105	3ad2ant1 1133	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ([Q]‘𝐴))
107		addpqnq 10979	. . . . 5 ⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
108	107	3adant1 1130	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
109	106, 108	oveq12d 7450	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))))
110		mulpqnq 10982	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
111	110	3adant3 1132	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
112		mulpqnq 10982	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
113	112	3adant2 1131	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
114	111, 113	oveq12d 7450	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
115	103, 109, 114	3eqtr4d 2786	. 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
116		addnqf 10989	. . . 4 ⊢ +Q :(Q × Q)⟶Q
117	116	fdmi 6746	. . 3 ⊢ dom +Q = (Q × Q)
118		0nnq 10965	. . 3 ⊢ ¬ ∅ ∈ Q
119		mulnqf 10990	. . . 4 ⊢ ·Q :(Q × Q)⟶Q
120	119	fdmi 6746	. . 3 ⊢ dom ·Q = (Q × Q)
121	117, 118, 120	ndmovdistr 7623	. 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 1086   = wceq 1539   ∈ wcel 2107  ⟨cop 4631   class class class wbr 5142   × cxp 5682  Rel wrel 5689  ‘cfv 6560  (class class class)co 7432  1^st c1st 8013  2^nd c2nd 8014  Ncnpi 10885   +_N cpli 10886   ·_N cmi 10887   +_pQ cplpq 10889   ·_pQ cmpq 10890   ~_Q ceq 10892  Qcnq 10893  [Q]cerq 10895   +_Q cplq 10896   ·_Q cmq 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-oadd 8511  df-omul 8512  df-er 8746  df-ni 10913  df-pli 10914  df-mi 10915  df-lti 10916  df-plpq 10949  df-mpq 10950  df-enq 10952  df-nq 10953  df-erq 10954  df-plq 10955  df-mq 10956  df-1nq 10957

This theorem is referenced by:  ltaddnq  11015  halfnq  11017  addclprlem2  11058  distrlem1pr  11066  distrlem4pr  11067  prlem934  11074  prlem936  11088