addassnq

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

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

Proof

Step	Hyp	Ref	Expression
1		addasspi	$⊢ ((1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) = (1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))))$
2		ovex	$⊢ 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in V$
3		ovex	$⊢ 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in V$
4		fvex	$⊢ 2^{nd} (C) \in V$
5		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
6		distrpi	$⊢ x \cdot_{𝑵} (y +_{𝑵} z) = (x \cdot_{𝑵} y) +_{𝑵} (x \cdot_{𝑵} z)$
7	2 3 4 5 6	caovdir	$⊢ ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C) = ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C))$
8		mulasspi	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C) = 1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
9	8	oveq1i	$⊢ ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C)) = (1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C))$
10	7 9	eqtri	$⊢ ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C) = (1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C))$
11	10	oveq1i	$⊢ (((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) = ((1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)))$
12		ovex	$⊢ 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in V$
13		ovex	$⊢ 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in V$
14		fvex	$⊢ 2^{nd} (A) \in V$
15	12 13 14 5 6	caovdir	$⊢ ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A) = ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (A))$
16		fvex	$⊢ 1^{st} (B) \in V$
17		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
18	16 4 14 5 17	caov32	$⊢ (1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 2^{nd} (A) = (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C)$
19		mulasspi	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (A) = 1^{st} (C) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (A))$
20		mulcompi	$⊢ 2^{nd} (B) \cdot_{𝑵} 2^{nd} (A) = 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)$
21	20	oveq2i	$⊢ 1^{st} (C) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (A)) = 1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))$
22	19 21	eqtri	$⊢ (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (A) = 1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))$
23	18 22	oveq12i	$⊢ ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} ((1^{st} (C) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (A)) = ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)))$
24	15 23	eqtri	$⊢ ((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A) = ((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)))$
25	24	oveq2i	$⊢ (1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A)) = (1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))))$
26	1 11 25	3eqtr4i	$⊢ (((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) = (1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A))$
27		mulasspi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))$
28	26 27	opeq12i	$⊢ ⟨(((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C)⟩ = ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
29		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
30	29	3ad2ant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A \in (𝑵 \times 𝑵)$
31		elpqn	$⊢ B \in 𝑸 \to B \in (𝑵 \times 𝑵)$
32	31	3ad2ant2	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B \in (𝑵 \times 𝑵)$
33		addpipq2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A +_{𝑝𝑸} B = ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩$
34	30 32 33	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A +_{𝑝𝑸} B = ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩$
35		relxp	$⊢ Rel (𝑵 \times 𝑵)$
36		elpqn	$⊢ C \in 𝑸 \to C \in (𝑵 \times 𝑵)$
37	36	3ad2ant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C \in (𝑵 \times 𝑵)$
38		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land C \in (𝑵 \times 𝑵)) \to C = ⟨1^{st} (C), 2^{nd} (C)⟩$
39	35 37 38	sylancr	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C = ⟨1^{st} (C), 2^{nd} (C)⟩$
40	34 39	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A +_{𝑝𝑸} B) +_{𝑝𝑸} C = ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ +_{𝑝𝑸} ⟨1^{st} (C), 2^{nd} (C)⟩$
41		xp1st	$⊢ A \in (𝑵 \times 𝑵) \to 1^{st} (A) \in 𝑵$
42	30 41	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (A) \in 𝑵$
43		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
44	32 43	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (B) \in 𝑵$
45		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
46	42 44 45	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
47		xp1st	$⊢ B \in (𝑵 \times 𝑵) \to 1^{st} (B) \in 𝑵$
48	32 47	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (B) \in 𝑵$
49		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
50	30 49	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \in 𝑵$
51		mulclpi	$⊢ (1^{st} (B) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
52	48 50 51	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
53		addclpi	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵 \land 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in 𝑵) \to (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵$
54	46 52 53	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵$
55		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
56	50 44 55	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
57		xp1st	$⊢ C \in (𝑵 \times 𝑵) \to 1^{st} (C) \in 𝑵$
58	37 57	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (C) \in 𝑵$
59		xp2nd	$⊢ C \in (𝑵 \times 𝑵) \to 2^{nd} (C) \in 𝑵$
60	37 59	syl	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (C) \in 𝑵$
61		addpipq	$⊢ (((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵) \land (1^{st} (C) \in 𝑵 \land 2^{nd} (C) \in 𝑵)) \to ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ +_{𝑝𝑸} ⟨1^{st} (C), 2^{nd} (C)⟩ = ⟨(((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C)⟩$
62	54 56 58 60 61	syl22anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ +_{𝑝𝑸} ⟨1^{st} (C), 2^{nd} (C)⟩ = ⟨(((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C)⟩$
63	40 62	eqtrd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A +_{𝑝𝑸} B) +_{𝑝𝑸} C = ⟨(((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) \cdot_{𝑵} 2^{nd} (C)⟩$
64		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
65	35 30 64	sylancr	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
66		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)⟩$
67	32 37 66	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)⟩$
68	65 67	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A +_{𝑝𝑸} (B +_{𝑝𝑸} C) = ⟨1^{st} (A), 2^{nd} (A)⟩ +_{𝑝𝑸} ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C)⟩$
69		mulclpi	$⊢ (1^{st} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
70	48 60 69	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
71		mulclpi	$⊢ (1^{st} (C) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
72	58 44 71	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 1^{st} (C) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
73		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 𝑵$
74	70 72 73	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 𝑵$
75		mulclpi	$⊢ (2^{nd} (B) \in 𝑵 \land 2^{nd} (C) \in 𝑵) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
76	44 60 75	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to 2^{nd} (B) \cdot_{𝑵} 2^{nd} (C) \in 𝑵$
77		addpipq	$⊢ ((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)⟩ +_{𝑝𝑸} ⟨(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_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
78	42 50 74 76 77	syl22anc	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to ⟨1^{st} (A), 2^{nd} (A)⟩ +_{𝑝𝑸} ⟨(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_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
79	68 78	eqtrd	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A +_{𝑝𝑸} (B +_{𝑝𝑸} C) = ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))) +_{𝑵} (((1^{st} (B) \cdot_{𝑵} 2^{nd} (C)) +_{𝑵} (1^{st} (C) \cdot_{𝑵} 2^{nd} (B))) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (B) \cdot_{𝑵} 2^{nd} (C))⟩$
80	28 63 79	3eqtr4a	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A +_{𝑝𝑸} B) +_{𝑝𝑸} C = A +_{𝑝𝑸} (B +_{𝑝𝑸} C)$
81	80	fveq2d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to /_{𝑸} ((A +_{𝑝𝑸} B) +_{𝑝𝑸} C) = /_{𝑸} (A +_{𝑝𝑸} (B +_{𝑝𝑸} C))$
82		adderpq	$⊢ /_{𝑸} (A +_{𝑝𝑸} B) +_{𝑸} /_{𝑸} (C) = /_{𝑸} ((A +_{𝑝𝑸} B) +_{𝑝𝑸} C)$
83		adderpq	$⊢ /_{𝑸} (A) +_{𝑸} /_{𝑸} (B +_{𝑝𝑸} C) = /_{𝑸} (A +_{𝑝𝑸} (B +_{𝑝𝑸} C))$
84	81 82 83	3eqtr4g	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to /_{𝑸} (A +_{𝑝𝑸} B) +_{𝑸} /_{𝑸} (C) = /_{𝑸} (A) +_{𝑸} /_{𝑸} (B +_{𝑝𝑸} C)$
85		addpqnq	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A +_{𝑸} B = /_{𝑸} (A +_{𝑝𝑸} B)$
86	85	3adant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A +_{𝑸} B = /_{𝑸} (A +_{𝑝𝑸} B)$
87		nqerid	$⊢ C \in 𝑸 \to /_{𝑸} (C) = C$
88	87	eqcomd	$⊢ C \in 𝑸 \to C = /_{𝑸} (C)$
89	88	3ad2ant3	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to C = /_{𝑸} (C)$
90	86 89	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A +_{𝑸} B) +_{𝑸} C = /_{𝑸} (A +_{𝑝𝑸} B) +_{𝑸} /_{𝑸} (C)$
91		nqerid	$⊢ A \in 𝑸 \to /_{𝑸} (A) = A$
92	91	eqcomd	$⊢ A \in 𝑸 \to A = /_{𝑸} (A)$
93	92	3ad2ant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A = /_{𝑸} (A)$
94		addpqnq	$⊢ (B \in 𝑸 \land C \in 𝑸) \to B +_{𝑸} C = /_{𝑸} (B +_{𝑝𝑸} C)$
95	94	3adant1	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to B +_{𝑸} C = /_{𝑸} (B +_{𝑝𝑸} C)$
96	93 95	oveq12d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to A +_{𝑸} (B +_{𝑸} C) = /_{𝑸} (A) +_{𝑸} /_{𝑸} (B +_{𝑝𝑸} C)$
97	84 90 96	3eqtr4d	$⊢ (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A +_{𝑸} B) +_{𝑸} C = A +_{𝑸} (B +_{𝑸} C)$
98		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
99	98	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
100		0nnq	$⊢ \neg \emptyset \in 𝑸$
101	99 100	ndmovass	$⊢ \neg (A \in 𝑸 \land B \in 𝑸 \land C \in 𝑸) \to (A +_{𝑸} B) +_{𝑸} C = A +_{𝑸} (B +_{𝑸} C)$
102	97 101	pm2.61i	$⊢ (A +_{𝑸} B) +_{𝑸} C = A +_{𝑸} (B +_{𝑸} C)$

Metamath Proof Explorer

Theorem addassnq

Proof