Theorem distrnq 10648

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 10583	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐵)) = ((1st ‘𝐵) ·N (1st ‘𝐴))
2	1	oveq1i 7265	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))
3		fvex 6769	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐵) ∈ V
4		fvex 6769	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐴) ∈ V
5		fvex 6769	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐴) ∈ V
6		mulcompi 10583	. . . . . . . . . . . . 13 ⊢ (𝑥 ·N 𝑦) = (𝑦 ·N 𝑥)
7		mulasspi 10584	. . . . . . . . . . . . 13 ⊢ ((𝑥 ·N 𝑦) ·N 𝑧) = (𝑥 ·N (𝑦 ·N 𝑧))
8		fvex 6769	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐶) ∈ V
9	3, 4, 5, 6, 7, 8	caov411 7482	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐵) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
10	2, 9	eqtri 2766	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐵) ·N (2nd ‘𝐶)))
11		mulcompi 10583	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝐴) ·N (1st ‘𝐶)) = ((1st ‘𝐶) ·N (1st ‘𝐴))
12	11	oveq1i 7265	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵)))
13		fvex 6769	. . . . . . . . . . . . 13 ⊢ (1st ‘𝐶) ∈ V
14		fvex 6769	. . . . . . . . . . . . 13 ⊢ (2nd ‘𝐵) ∈ V
15	13, 4, 5, 6, 7, 14	caov411 7482	. . . . . . . . . . . 12 ⊢ (((1st ‘𝐶) ·N (1st ‘𝐴)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
16	12, 15	eqtri 2766	. . . . . . . . . . 11 ⊢ (((1st ‘𝐴) ·N (1st ‘𝐶)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐵))) = (((2nd ‘𝐴) ·N (1st ‘𝐴)) ·N ((1st ‘𝐶) ·N (2nd ‘𝐵)))
17	10, 16	oveq12i 7267	. . . . . . . . . 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 10585	. . . . . . . . . 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 10584	. . . . . . . . . 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 2772	. . . . . . . . 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 10584	. . . . . . . . . 10 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))))
22	14, 5, 8, 6, 7	caov12 7478	. . . . . . . . . . 11 ⊢ ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶)))
23	22	oveq2i 7266	. . . . . . . . . 10 ⊢ ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶)))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
24	21, 23	eqtri 2766	. . . . . . . . 9 ⊢ (((2nd ‘𝐴) ·N (2nd ‘𝐵)) ·N ((2nd ‘𝐴) ·N (2nd ‘𝐶))) = ((2nd ‘𝐴) ·N ((2nd ‘𝐴) ·N ((2nd ‘𝐵) ·N (2nd ‘𝐶))))
25	20, 24	opeq12i 4806	. . . . . . . 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 10612	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))
27	26	3ad2ant1 1131	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 ∈ (N × N))
28		xp2nd 7837	. . . . . . . . . 10 ⊢ (𝐴 ∈ (N × N) → (2nd ‘𝐴) ∈ N)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐴) ∈ N)
30		xp1st 7836	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (N × N) → (1st ‘𝐴) ∈ N)
31	27, 30	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐴) ∈ N)
32		elpqn 10612	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Q → 𝐵 ∈ (N × N))
33	32	3ad2ant2 1132	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐵 ∈ (N × N))
34		xp1st 7836	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (1st ‘𝐵) ∈ N)
35	33, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐵) ∈ N)
36		elpqn 10612	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Q → 𝐶 ∈ (N × N))
37	36	3ad2ant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐶 ∈ (N × N))
38		xp2nd 7837	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (2nd ‘𝐶) ∈ N)
39	37, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐶) ∈ N)
40		mulclpi 10580	. . . . . . . . . . . 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 7836	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (N × N) → (1st ‘𝐶) ∈ N)
43	37, 42	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (1st ‘𝐶) ∈ N)
44		xp2nd 7837	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (N × N) → (2nd ‘𝐵) ∈ N)
45	33, 44	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (2nd ‘𝐵) ∈ N)
46		mulclpi 10580	. . . . . . . . . . . 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 10579	. . . . . . . . . . 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 10580	. . . . . . . . . 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 10580	. . . . . . . . . . 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 10580	. . . . . . . . . 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 10647	. . . . . . . . 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 1369	. . . . . . . 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 5105	. . . . . . 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 10626	. . . . . . . . . 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 10626	. . . . . . . . . 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 7273	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) = (⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩ +pQ ⟨((1st ‘𝐴) ·N (1st ‘𝐶)), ((2nd ‘𝐴) ·N (2nd ‘𝐶))⟩))
64		mulclpi 10580	. . . . . . . . . 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 10580	. . . . . . . . . 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 10580	. . . . . . . . . 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 10580	. . . . . . . . . 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 10624	. . . . . . . . 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 835	. . . . . . . 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 2778	. . . . . . 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 5598	. . . . . . . . . 10 ⊢ Rel (N × N)
76		1st2nd 7853	. . . . . . . . . 10 ⊢ ((Rel (N × N) ∧ 𝐴 ∈ (N × N)) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
77	75, 27, 76	sylancr 586	. . . . . . . . 9 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
78		addpipq2 10623	. . . . . . . . . 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 7273	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ (𝐵 +pQ 𝐶)) = (⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ·pQ ⟨(((1st ‘𝐵) ·N (2nd ‘𝐶)) +N ((1st ‘𝐶) ·N (2nd ‘𝐵))), ((2nd ‘𝐵) ·N (2nd ‘𝐶))⟩))
81		mulpipq 10627	. . . . . . . . 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 835	. . . . . . . 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 2778	. . . . . . 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 5102	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)) ~Q (𝐴 ·pQ (𝐵 +pQ 𝐶)))
85		mulpqf 10633	. . . . . . . . . 10 ⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
86	85	fovcl 7380	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) ∈ (N × N))
87	27, 33, 86	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐵) ∈ (N × N))
88	85	fovcl 7380	. . . . . . . . 9 ⊢ ((𝐴 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ·pQ 𝐶) ∈ (N × N))
89	27, 37, 88	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·pQ 𝐶) ∈ (N × N))
90		addpqf 10631	. . . . . . . . 9 ⊢ +pQ :((N × N) × (N × N))⟶(N × N)
91	90	fovcl 7380	. . . . . . . 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 7380	. . . . . . . . 9 ⊢ ((𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐵 +pQ 𝐶) ∈ (N × N))
94	33, 37, 93	syl2anc 583	. . . . . . . 8 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +pQ 𝐶) ∈ (N × N))
95	85	fovcl 7380	. . . . . . . 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 10622	. . . . . . 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 231	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))))
100	99	eqcomd 2744	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶))))
101		mulerpq 10644	. . . 4 ⊢ (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = ([Q]‘(𝐴 ·pQ (𝐵 +pQ 𝐶)))
102		adderpq 10643	. . . 4 ⊢ (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))) = ([Q]‘((𝐴 ·pQ 𝐵) +pQ (𝐴 ·pQ 𝐶)))
103	100, 101, 102	3eqtr4g 2804	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
104		nqerid 10620	. . . . . 6 ⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴)
105	104	eqcomd 2744	. . . . 5 ⊢ (𝐴 ∈ Q → 𝐴 = ([Q]‘𝐴))
106	105	3ad2ant1 1131	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → 𝐴 = ([Q]‘𝐴))
107		addpqnq 10625	. . . . 5 ⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
108	107	3adant1 1128	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐵 +Q 𝐶) = ([Q]‘(𝐵 +pQ 𝐶)))
109	106, 108	oveq12d 7273	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = (([Q]‘𝐴) ·Q ([Q]‘(𝐵 +pQ 𝐶))))
110		mulpqnq 10628	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
111	110	3adant3 1130	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵)))
112		mulpqnq 10628	. . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
113	112	3adant2 1129	. . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q 𝐶) = ([Q]‘(𝐴 ·pQ 𝐶)))
114	111, 113	oveq12d 7273	. . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)) = (([Q]‘(𝐴 ·pQ 𝐵)) +Q ([Q]‘(𝐴 ·pQ 𝐶))))
115	103, 109, 114	3eqtr4d 2788	. 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
116		addnqf 10635	. . . 4 ⊢ +Q :(Q × Q)⟶Q
117	116	fdmi 6596	. . 3 ⊢ dom +Q = (Q × Q)
118		0nnq 10611	. . 3 ⊢ ¬ ∅ ∈ Q
119		mulnqf 10636	. . . 4 ⊢ ·Q :(Q × Q)⟶Q
120	119	fdmi 6596	. . 3 ⊢ dom ·Q = (Q × Q)
121	117, 118, 120	ndmovdistr 7439	. 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 1085   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   class class class wbr 5070   × cxp 5578  Rel wrel 5585  ‘cfv 6418  (class class class)co 7255  1^st c1st 7802  2^nd c2nd 7803  Ncnpi 10531   +_N cpli 10532   ·_N cmi 10533   +_pQ cplpq 10535   ·_pQ cmpq 10536   ~_Q ceq 10538  Qcnq 10539  [Q]cerq 10541   +_Q cplq 10542   ·_Q cmq 10543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-oadd 8271  df-omul 8272  df-er 8456  df-ni 10559  df-pli 10560  df-mi 10561  df-lti 10562  df-plpq 10595  df-mpq 10596  df-enq 10598  df-nq 10599  df-erq 10600  df-plq 10601  df-mq 10602  df-1nq 10603

This theorem is referenced by:  ltaddnq  10661  halfnq  10663  addclprlem2  10704  distrlem1pr  10712  distrlem4pr  10713  prlem934  10720  prlem936  10734