Theorem 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	⊢ ( ( 𝐴 +Q 𝐵 ) +Q 𝐶 ) = ( 𝐴 +Q ( 𝐵 +Q 𝐶 ) )

Proof

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