distrnq

Description: Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	distrnq	$⊢ A \cdot_{𝑸} (B +_{𝑸} C) = (A \cdot_{𝑸} B) +_{𝑸} (A \cdot_{𝑸} C)$

Proof

Step	Hyp	Ref	Expression
1		mulcompi	$⊢ 1^{st} (A) \cdot_{𝑵} 1^{st} (B) = 1^{st} (B) \cdot_{𝑵} 1^{st} (A)$
2	1	oveq1i	$⊢ (1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = (1^{st} (B) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))$
3		fvex	$⊢ 1^{st} (B) \in V$
4		fvex	$⊢ 1^{st} (A) \in V$
5		fvex	$⊢ 2^{nd} (A) \in V$
6		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
7		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
8		fvex	$⊢ 2^{nd} (C) \in V$
9	3 4 5 6 7 8	caov411	$⊢ (1^{st} (B) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
10	2 9	eqtri	$⊢ (1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = (2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))$
11		mulcompi	$⊢ 1^{st} (A) \cdot_{𝑵} 1^{st} (C) = 1^{st} (C) \cdot_{𝑵} 1^{st} (A)$
12	11	oveq1i	$⊢ (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) = (1^{st} (C) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))$
13		fvex	$⊢ 1^{st} (C) \in V$
14		fvex	$⊢ 2^{nd} (B) \in V$
15	13 4 5 6 7 14	caov411	$⊢ (1^{st} (C) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))$
16	12 15	eqtri	$⊢ (1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))$
17	10 16	oveq12i	$⊢ ((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
18		distrpi	$⊢ (2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) = ((2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))$
19		mulasspi	$⊢ (2^{nd} (A) \cdot_{𝑵} 1^{st} (A)) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) = 2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))))$
20	17 18 19	3eqtr2i	$⊢ ((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) = 2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))))$
21		mulasspi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)))$
22	14 5 8 6 7	caov12	$⊢ 2^{nd} (B) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
23	22	oveq2i	$⊢ 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))$
24	21 23	eqtri	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))$
25	20 24	opeq12i	$⊢ ⟨((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))⟩ = ⟨2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))⟩$
26		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
27	26	3ad2ant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \in (𝑵 \times 𝑵)$
28		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
29	27 28	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \in 𝑵$
30		xp1st	$⊢ A \in (𝑵 \times 𝑵) \to 1^{st} (A) \in 𝑵$
31	27 30	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (A) \in 𝑵$
32		elpqn	$⊢ B \in 𝑸 \to B \in (𝑵 \times 𝑵)$
33	32	3ad2ant2	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B \in (𝑵 \times 𝑵)$
34		xp1st	$⊢ B \in (𝑵 \times 𝑵) \to 1^{st} (B) \in 𝑵$
35	33 34	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (B) \in 𝑵$
36		elpqn	$⊢ C \in 𝑸 \to C \in (𝑵 \times 𝑵)$
37	36	3ad2ant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C \in (𝑵 \times 𝑵)$
38		xp2nd	$⊢ C \in (𝑵 \times 𝑵) \to 2^{nd} (C) \in 𝑵$
39	37 38	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (C) \in 𝑵$
40		mulclpi	$⊢ (1^{st} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
41	35 39 40	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
42		xp1st	$⊢ C \in (𝑵 \times 𝑵) \to 1^{st} (C) \in 𝑵$
43	37 42	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (C) \in 𝑵$
44		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
45	33 44	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (B) \in 𝑵$
46		mulclpi	$⊢ (1^{st} (C) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
47	43 45 46	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
48		addclpi	$⊢ (1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵 \land 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \to (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
49	41 47 48	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵$
50		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \in 𝑵$
51	31 49 50	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \in 𝑵$
52		mulclpi	$⊢ (2^{nd} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
53	45 39 52	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
54		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) \in 𝑵$
55	29 53 54	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) \in 𝑵$
56		mulcanenq	$⊢ (2^{nd} (A) \in 𝑵 \land 1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)) \in 𝑵) \to ⟨2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))⟩ ~_{𝑸} ⟨1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
57	29 51 55 56	syl3anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ⟨2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)))⟩ ~_{𝑸} ⟨1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
58	25 57	eqbrtrid	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ⟨((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))⟩ ~_{𝑸} ⟨1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
59		mulpipq2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} B = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (B), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩$
60	27 33 59	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} B = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (B), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩$
61		mulpipq2	$⊢ (A \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} C = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
62	27 37 61	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} C = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
63	60 62	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C) = ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (B), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ +_{𝑝𝑸} ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩$
64		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 1^{st} (B) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 1^{st} (B) \in 𝑵$
65	31 35 64	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (A) \cdot_{𝑵} 1^{st} (B) \in 𝑵$
66		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
67	29 45 66	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
68		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 1^{st} (C) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 1^{st} (C) \in 𝑵$
69	31 43 68	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (A) \cdot_{𝑵} 1^{st} (C) \in 𝑵$
70		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
71	29 39 70	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
72		addpipq	$⊢ ((1^{st} (A) \cdot_{𝑵} 1^{st} (B) \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \land (1^{st} (A) \cdot_{𝑵} 1^{st} (C) \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C) \in 𝑵)) \to ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (B), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ +_{𝑝𝑸} ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ = ⟨((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))⟩$
73	65 67 69 71 72	syl22anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (B), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ +_{𝑝𝑸} ⟨1^{st} (A) \cdot_{𝑵} 1^{st} (C), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (C)⟩ = ⟨((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))⟩$
74	63 73	eqtrd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C) = ⟨((1^{st} (A) \cdot_{𝑵} 1^{st} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (A) \cdot_{𝑵} 1^{st} (C)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (C))⟩$
75		relxp	$⊢ Rel (𝑵 \times 𝑵)$
76		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
77	75 27 76	sylancr	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
78		addpipq2	$⊢ (B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to B +_{𝑝𝑸} C = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
79	33 37 78	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B +_{𝑝𝑸} C = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
80	77 79	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C) = ⟨1^{st} (A), 2^{nd} (A)⟩ \cdot_{𝑝𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
81		mulpipq	$⊢ ((1^{st} (A) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \land ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \in 𝑵 \land 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵)) \to ⟨1^{st} (A), 2^{nd} (A)⟩ \cdot_{𝑝𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩ = ⟨1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
82	31 29 49 53 81	syl22anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ⟨1^{st} (A), 2^{nd} (A)⟩ \cdot_{𝑝𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩ = ⟨1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
83	80 82	eqtrd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C) = ⟨1^{st} (A) \cdot_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
84	58 74 83	3brtr4d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C)) ~_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C))$
85		mulpqf	$⊢ \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
86	85	fovcl	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵)$
87	27 33 86	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵)$
88	85	fovcl	$⊢ (A \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} C \in (𝑵 \times 𝑵)$
89	27 37 88	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} C \in (𝑵 \times 𝑵)$
90		addpqf	$⊢ +_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
91	90	fovcl	$⊢ (A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵) \land A \cdot_{𝑝𝑸} C \in (𝑵 \times 𝑵)) \to (A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C) \in (𝑵 \times 𝑵)$
92	87 89 91	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C) \in (𝑵 \times 𝑵)$
93	90	fovcl	$⊢ (B \in (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to B +_{𝑝𝑸} C \in (𝑵 \times 𝑵)$
94	33 37 93	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B +_{𝑝𝑸} C \in (𝑵 \times 𝑵)$
95	85	fovcl	$⊢ (A \in (𝑵 \times 𝑵) \land B +_{𝑝𝑸} C \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C) \in (𝑵 \times 𝑵)$
96	27 94 95	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C) \in (𝑵 \times 𝑵)$
97		nqereq	$⊢ ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C) \in (𝑵 \times 𝑵) \land A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C) \in (𝑵 \times 𝑵)) \to (((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C)) ~_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C)) \leftrightarrow /_{𝑸} ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C)) = /_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C)))$
98	92 96 97	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C)) ~_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C)) \leftrightarrow /_{𝑸} ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C)) = /_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C)))$
99	84 98	mpbid	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to /_{𝑸} ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C)) = /_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C))$
100	99	eqcomd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to /_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C)) = /_{𝑸} ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C))$
101		mulerpq	$⊢ /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B +_{𝑝𝑸} C) = /_{𝑸} (A \cdot_{𝑝𝑸} (B +_{𝑝𝑸} C))$
102		adderpq	$⊢ /_{𝑸} (A \cdot_{𝑝𝑸} B) +_{𝑸} /_{𝑸} (A \cdot_{𝑝𝑸} C) = /_{𝑸} ((A \cdot_{𝑝𝑸} B) +_{𝑝𝑸} (A \cdot_{𝑝𝑸} C))$
103	100 101 102	3eqtr4g	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B +_{𝑝𝑸} C) = /_{𝑸} (A \cdot_{𝑝𝑸} B) +_{𝑸} /_{𝑸} (A \cdot_{𝑝𝑸} C)$
104		nqerid	$⊢ A \in 𝑸 \to /_{𝑸} (A) = A$
105	104	eqcomd	$⊢ A \in 𝑸 \to A = /_{𝑸} (A)$
106	105	3ad2ant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A = /_{𝑸} (A)$
107		addpqnq	$⊢ (B \in 𝑸 \land C \in 𝑸) \to B +_{𝑸} C = /_{𝑸} (B +_{𝑝𝑸} C)$
108	107	3adant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B +_{𝑸} C = /_{𝑸} (B +_{𝑝𝑸} C)$
109	106 108	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑸} (B +_{𝑸} C) = /_{𝑸} (A) \cdot_{𝑸} /_{𝑸} (B +_{𝑝𝑸} C)$
110		mulpqnq	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A \cdot_{𝑸} B = /_{𝑸} (A \cdot_{𝑝𝑸} B)$
111	110	3adant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑸} B = /_{𝑸} (A \cdot_{𝑝𝑸} B)$
112		mulpqnq	$⊢ (A \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑸} C = /_{𝑸} (A \cdot_{𝑝𝑸} C)$
113	112	3adant2	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑸} C = /_{𝑸} (A \cdot_{𝑝𝑸} C)$
114	111 113	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A \cdot_{𝑸} B) +_{𝑸} (A \cdot_{𝑸} C) = /_{𝑸} (A \cdot_{𝑝𝑸} B) +_{𝑸} /_{𝑸} (A \cdot_{𝑝𝑸} C)$
115	103 109 114	3eqtr4d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑸} (B +_{𝑸} C) = (A \cdot_{𝑸} B) +_{𝑸} (A \cdot_{𝑸} C)$
116		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
117	116	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
118		0nnq	$⊢ \neg \emptyset \in 𝑸$
119		mulnqf	$⊢ \cdot_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
120	119	fdmi	$⊢ dom \cdot_{𝑸} = 𝑸 \times 𝑸$
121	117 118 120	ndmovdistr	$⊢ \neg (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \cdot_{𝑸} (B +_{𝑸} C) = (A \cdot_{𝑸} B) +_{𝑸} (A \cdot_{𝑸} C)$
122	115 121	pm2.61i	$⊢ A \cdot_{𝑸} (B +_{𝑸} C) = (A \cdot_{𝑸} B) +_{𝑸} (A \cdot_{𝑸} C)$

Metamath Proof Explorer

Theorem distrnq

Proof