Step |
Hyp |
Ref |
Expression |
1 |
|
elpqn |
|- ( x e. Q. -> x e. ( N. X. N. ) ) |
2 |
1
|
adantr |
|- ( ( x e. Q. /\ y e. Q. ) -> x e. ( N. X. N. ) ) |
3 |
|
xp1st |
|- ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. ) |
4 |
2 3
|
syl |
|- ( ( x e. Q. /\ y e. Q. ) -> ( 1st ` x ) e. N. ) |
5 |
|
elpqn |
|- ( y e. Q. -> y e. ( N. X. N. ) ) |
6 |
5
|
adantl |
|- ( ( x e. Q. /\ y e. Q. ) -> y e. ( N. X. N. ) ) |
7 |
|
xp2nd |
|- ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. ) |
8 |
6 7
|
syl |
|- ( ( x e. Q. /\ y e. Q. ) -> ( 2nd ` y ) e. N. ) |
9 |
|
mulclpi |
|- ( ( ( 1st ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. ) |
10 |
4 8 9
|
syl2anc |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. ) |
11 |
|
xp1st |
|- ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. ) |
12 |
6 11
|
syl |
|- ( ( x e. Q. /\ y e. Q. ) -> ( 1st ` y ) e. N. ) |
13 |
|
xp2nd |
|- ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. ) |
14 |
2 13
|
syl |
|- ( ( x e. Q. /\ y e. Q. ) -> ( 2nd ` x ) e. N. ) |
15 |
|
mulclpi |
|- ( ( ( 1st ` y ) e. N. /\ ( 2nd ` x ) e. N. ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. ) |
16 |
12 14 15
|
syl2anc |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. ) |
17 |
|
ltsopi |
|- |
18 |
|
sotric |
|- ( ( ( ( ( 1st ` x ) .N ( 2nd ` y ) ) -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) ) |
19 |
17 18
|
mpan |
|- ( ( ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. /\ ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) ) |
20 |
10 16 19
|
syl2anc |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) ) |
21 |
|
ordpinq |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x ( ( 1st ` x ) .N ( 2nd ` y ) ) |
22 |
|
fveq2 |
|- ( x = y -> ( 1st ` x ) = ( 1st ` y ) ) |
23 |
|
fveq2 |
|- ( x = y -> ( 2nd ` x ) = ( 2nd ` y ) ) |
24 |
23
|
eqcomd |
|- ( x = y -> ( 2nd ` y ) = ( 2nd ` x ) ) |
25 |
22 24
|
oveq12d |
|- ( x = y -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) |
26 |
|
enqbreq2 |
|- ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) ) |
27 |
1 5 26
|
syl2an |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) ) |
28 |
|
enqeq |
|- ( ( x e. Q. /\ y e. Q. /\ x ~Q y ) -> x = y ) |
29 |
28
|
3expia |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x ~Q y -> x = y ) ) |
30 |
27 29
|
sylbird |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) -> x = y ) ) |
31 |
25 30
|
impbid2 |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x = y <-> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) ) ) |
32 |
|
ordpinq |
|- ( ( y e. Q. /\ x e. Q. ) -> ( y ( ( 1st ` y ) .N ( 2nd ` x ) ) |
33 |
32
|
ancoms |
|- ( ( x e. Q. /\ y e. Q. ) -> ( y ( ( 1st ` y ) .N ( 2nd ` x ) ) |
34 |
31 33
|
orbi12d |
|- ( ( x e. Q. /\ y e. Q. ) -> ( ( x = y \/ y ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) ) |
35 |
34
|
notbid |
|- ( ( x e. Q. /\ y e. Q. ) -> ( -. ( x = y \/ y -. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( ( 1st ` y ) .N ( 2nd ` x ) ) \/ ( ( 1st ` y ) .N ( 2nd ` x ) ) |
36 |
20 21 35
|
3bitr4d |
|- ( ( x e. Q. /\ y e. Q. ) -> ( x -. ( x = y \/ y |
37 |
21
|
3adant3 |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x ( ( 1st ` x ) .N ( 2nd ` y ) ) |
38 |
|
elpqn |
|- ( z e. Q. -> z e. ( N. X. N. ) ) |
39 |
38
|
3ad2ant3 |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> z e. ( N. X. N. ) ) |
40 |
|
xp2nd |
|- ( z e. ( N. X. N. ) -> ( 2nd ` z ) e. N. ) |
41 |
|
ltmpi |
|- ( ( 2nd ` z ) e. N. -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) |
42 |
39 40 41
|
3syl |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) |
43 |
37 42
|
bitrd |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) |
44 |
|
ordpinq |
|- ( ( y e. Q. /\ z e. Q. ) -> ( y ( ( 1st ` y ) .N ( 2nd ` z ) ) |
45 |
44
|
3adant1 |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( y ( ( 1st ` y ) .N ( 2nd ` z ) ) |
46 |
1
|
3ad2ant1 |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> x e. ( N. X. N. ) ) |
47 |
|
ltmpi |
|- ( ( 2nd ` x ) e. N. -> ( ( ( 1st ` y ) .N ( 2nd ` z ) ) ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) ) |
48 |
46 13 47
|
3syl |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( ( 1st ` y ) .N ( 2nd ` z ) ) ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) ) |
49 |
45 48
|
bitrd |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( y ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) ) |
50 |
43 49
|
anbi12d |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( x ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) |
51 |
|
fvex |
|- ( 2nd ` x ) e. _V |
52 |
|
fvex |
|- ( 1st ` y ) e. _V |
53 |
|
fvex |
|- ( 2nd ` z ) e. _V |
54 |
|
mulcompi |
|- ( r .N s ) = ( s .N r ) |
55 |
|
mulasspi |
|- ( ( r .N s ) .N t ) = ( r .N ( s .N t ) ) |
56 |
51 52 53 54 55
|
caov13 |
|- ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) ) = ( ( 2nd ` z ) .N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) |
57 |
|
fvex |
|- ( 1st ` z ) e. _V |
58 |
|
fvex |
|- ( 2nd ` y ) e. _V |
59 |
51 57 58 54 55
|
caov13 |
|- ( ( 2nd ` x ) .N ( ( 1st ` z ) .N ( 2nd ` y ) ) ) = ( ( 2nd ` y ) .N ( ( 1st ` z ) .N ( 2nd ` x ) ) ) |
60 |
56 59
|
breq12i |
|- ( ( ( 2nd ` x ) .N ( ( 1st ` y ) .N ( 2nd ` z ) ) ) ( ( 2nd ` z ) .N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) |
61 |
|
fvex |
|- ( 1st ` x ) e. _V |
62 |
53 61 58 54 55
|
caov13 |
|- ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) = ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
63 |
|
ltrelpi |
|- |
64 |
17 63
|
sotri |
|- ( ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) |
65 |
62 64
|
eqbrtrrid |
|- ( ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
66 |
60 65
|
sylan2b |
|- ( ( ( ( 2nd ` z ) .N ( ( 1st ` x ) .N ( 2nd ` y ) ) ) ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
67 |
50 66
|
syl6bi |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( x ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
68 |
|
ordpinq |
|- ( ( x e. Q. /\ z e. Q. ) -> ( x ( ( 1st ` x ) .N ( 2nd ` z ) ) |
69 |
68
|
3adant2 |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x ( ( 1st ` x ) .N ( 2nd ` z ) ) |
70 |
5
|
3ad2ant2 |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> y e. ( N. X. N. ) ) |
71 |
|
ltmpi |
|- ( ( 2nd ` y ) e. N. -> ( ( ( 1st ` x ) .N ( 2nd ` z ) ) ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
72 |
70 7 71
|
3syl |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( ( 1st ` x ) .N ( 2nd ` z ) ) ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
73 |
69 72
|
bitrd |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x ( ( 2nd ` y ) .N ( ( 1st ` x ) .N ( 2nd ` z ) ) ) |
74 |
67 73
|
sylibrd |
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( ( x x |
75 |
36 74
|
isso2i |
|- |