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 
|- ( ( A +Q B ) +Q C ) = ( A +Q ( B +Q C ) )

Proof

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