Step |
Hyp |
Ref |
Expression |
1 |
|
addnqf |
|- +Q : ( Q. X. Q. ) --> Q. |
2 |
1
|
fdmi |
|- dom +Q = ( Q. X. Q. ) |
3 |
|
ltrelnq |
|- |
4 |
|
0nnq |
|- -. (/) e. Q. |
5 |
|
ordpinq |
|- ( ( A e. Q. /\ B e. Q. ) -> ( A ( ( 1st ` A ) .N ( 2nd ` B ) ) |
6 |
5
|
3adant3 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A ( ( 1st ` A ) .N ( 2nd ` B ) ) |
7 |
|
elpqn |
|- ( C e. Q. -> C e. ( N. X. N. ) ) |
8 |
7
|
3ad2ant3 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> C e. ( N. X. N. ) ) |
9 |
|
elpqn |
|- ( A e. Q. -> A e. ( N. X. N. ) ) |
10 |
9
|
3ad2ant1 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> A e. ( N. X. N. ) ) |
11 |
|
addpipq2 |
|- ( ( C e. ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> ( C +pQ A ) = <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. ) |
12 |
8 10 11
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +pQ A ) = <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. ) |
13 |
|
elpqn |
|- ( B e. Q. -> B e. ( N. X. N. ) ) |
14 |
13
|
3ad2ant2 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> B e. ( N. X. N. ) ) |
15 |
|
addpipq2 |
|- ( ( C e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( C +pQ B ) = <. ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` B ) ) >. ) |
16 |
8 14 15
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +pQ B ) = <. ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` B ) ) >. ) |
17 |
12 16
|
breq12d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C +pQ A ) <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . ) ) |
18 |
|
addpqnq |
|- ( ( C e. Q. /\ A e. Q. ) -> ( C +Q A ) = ( /Q ` ( C +pQ A ) ) ) |
19 |
18
|
ancoms |
|- ( ( A e. Q. /\ C e. Q. ) -> ( C +Q A ) = ( /Q ` ( C +pQ A ) ) ) |
20 |
19
|
3adant2 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +Q A ) = ( /Q ` ( C +pQ A ) ) ) |
21 |
|
addpqnq |
|- ( ( C e. Q. /\ B e. Q. ) -> ( C +Q B ) = ( /Q ` ( C +pQ B ) ) ) |
22 |
21
|
ancoms |
|- ( ( B e. Q. /\ C e. Q. ) -> ( C +Q B ) = ( /Q ` ( C +pQ B ) ) ) |
23 |
22
|
3adant1 |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( C +Q B ) = ( /Q ` ( C +pQ B ) ) ) |
24 |
20 23
|
breq12d |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C +Q A ) ( /Q ` ( C +pQ A ) ) |
25 |
|
lterpq |
|- ( ( C +pQ A ) ( /Q ` ( C +pQ A ) ) |
26 |
24 25
|
bitr4di |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( C +Q A ) ( C +pQ A ) |
27 |
|
xp2nd |
|- ( C e. ( N. X. N. ) -> ( 2nd ` C ) e. N. ) |
28 |
8 27
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` C ) e. N. ) |
29 |
|
mulclpi |
|- ( ( ( 2nd ` C ) e. N. /\ ( 2nd ` C ) e. N. ) -> ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. ) |
30 |
28 28 29
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. ) |
31 |
|
ltmpi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) e. N. -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) |
32 |
30 31
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) |
33 |
|
xp2nd |
|- ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. ) |
34 |
14 33
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` B ) e. N. ) |
35 |
|
mulclpi |
|- ( ( ( 2nd ` C ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 2nd ` C ) .N ( 2nd ` B ) ) e. N. ) |
36 |
28 34 35
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 2nd ` C ) .N ( 2nd ` B ) ) e. N. ) |
37 |
|
xp1st |
|- ( C e. ( N. X. N. ) -> ( 1st ` C ) e. N. ) |
38 |
8 37
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 1st ` C ) e. N. ) |
39 |
|
xp2nd |
|- ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. ) |
40 |
10 39
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( 2nd ` A ) e. N. ) |
41 |
|
mulclpi |
|- ( ( ( 1st ` C ) e. N. /\ ( 2nd ` A ) e. N. ) -> ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. ) |
42 |
38 40 41
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. ) |
43 |
|
mulclpi |
|- ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) e. N. /\ ( ( 1st ` C ) .N ( 2nd ` A ) ) e. N. ) -> ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. ) |
44 |
36 42 43
|
syl2anc |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. ) |
45 |
|
ltapi |
|- ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) e. N. -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) |
46 |
44 45
|
syl |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) |
47 |
32 46
|
bitrd |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) |
48 |
|
mulcompi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) |
49 |
|
fvex |
|- ( 1st ` A ) e. _V |
50 |
|
fvex |
|- ( 2nd ` B ) e. _V |
51 |
|
fvex |
|- ( 2nd ` C ) e. _V |
52 |
|
mulcompi |
|- ( x .N y ) = ( y .N x ) |
53 |
|
mulasspi |
|- ( ( x .N y ) .N z ) = ( x .N ( y .N z ) ) |
54 |
49 50 51 52 53 51
|
caov411 |
|- ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) |
55 |
48 54
|
eqtri |
|- ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) |
56 |
55
|
oveq2i |
|- ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) ) |
57 |
|
distrpi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) ) |
58 |
|
mulcompi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) |
59 |
56 57 58
|
3eqtr2i |
|- ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) |
60 |
|
mulcompi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) |
61 |
|
fvex |
|- ( 1st ` C ) e. _V |
62 |
|
fvex |
|- ( 2nd ` A ) e. _V |
63 |
61 62 51 52 53 50
|
caov411 |
|- ( ( ( 1st ` C ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) |
64 |
60 63
|
eqtri |
|- ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) |
65 |
|
mulcompi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) |
66 |
|
fvex |
|- ( 1st ` B ) e. _V |
67 |
66 62 51 52 53 51
|
caov411 |
|- ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 2nd ` C ) .N ( 2nd ` C ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) |
68 |
65 67
|
eqtri |
|- ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) |
69 |
64 68
|
oveq12i |
|- ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) |
70 |
|
distrpi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` C ) .N ( 2nd ` B ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) |
71 |
|
mulcompi |
|- ( ( ( 2nd ` C ) .N ( 2nd ` A ) ) .N ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` A ) ) ) |
72 |
69 70 71
|
3eqtr2i |
|- ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) ) = ( ( ( ( 1st ` C ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` A ) ) ) |
73 |
59 72
|
breq12i |
|- ( ( ( ( ( 2nd ` C ) .N ( 2nd ` B ) ) .N ( ( 1st ` C ) .N ( 2nd ` A ) ) ) +N ( ( ( 2nd ` C ) .N ( 2nd ` C ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ) ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) |
74 |
47 73
|
bitrdi |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) |
75 |
|
ordpipq |
|- ( <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . <-> ( ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) .N ( ( 2nd ` C ) .N ( 2nd ` B ) ) ) |
76 |
74 75
|
bitr4di |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) <. ( ( ( 1st ` C ) .N ( 2nd ` A ) ) +N ( ( 1st ` A ) .N ( 2nd ` C ) ) ) , ( ( 2nd ` C ) .N ( 2nd ` A ) ) >. . ) ) |
77 |
17 26 76
|
3bitr4rd |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( C +Q A ) |
78 |
6 77
|
bitrd |
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A ( C +Q A ) |
79 |
2 3 4 78
|
ndmovord |
|- ( C e. Q. -> ( A ( C +Q A ) |