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