Metamath Proof Explorer

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 𝐶 ) )