Step |
Hyp |
Ref |
Expression |
1 |
|
df-ltpq |
|- . | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) |
2 |
|
opabssxp |
|- { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) |
3 |
1 2
|
eqsstri |
|- |
4 |
3
|
brel |
|- ( A ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) ) |
5 |
|
ltrelnq |
|- |
6 |
5
|
brel |
|- ( ( /Q ` A ) ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) ) |
7 |
|
elpqn |
|- ( ( /Q ` A ) e. Q. -> ( /Q ` A ) e. ( N. X. N. ) ) |
8 |
|
elpqn |
|- ( ( /Q ` B ) e. Q. -> ( /Q ` B ) e. ( N. X. N. ) ) |
9 |
|
nqerf |
|- /Q : ( N. X. N. ) --> Q. |
10 |
9
|
fdmi |
|- dom /Q = ( N. X. N. ) |
11 |
|
0nelxp |
|- -. (/) e. ( N. X. N. ) |
12 |
10 11
|
ndmfvrcl |
|- ( ( /Q ` A ) e. ( N. X. N. ) -> A e. ( N. X. N. ) ) |
13 |
10 11
|
ndmfvrcl |
|- ( ( /Q ` B ) e. ( N. X. N. ) -> B e. ( N. X. N. ) ) |
14 |
12 13
|
anim12i |
|- ( ( ( /Q ` A ) e. ( N. X. N. ) /\ ( /Q ` B ) e. ( N. X. N. ) ) -> ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) ) |
15 |
7 8 14
|
syl2an |
|- ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) ) |
16 |
6 15
|
syl |
|- ( ( /Q ` A ) ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) ) |
17 |
|
xp1st |
|- ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. ) |
18 |
|
xp2nd |
|- ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. ) |
19 |
|
mulclpi |
|- ( ( ( 1st ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. ) |
20 |
17 18 19
|
syl2an |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. ) |
21 |
|
ltmpi |
|- ( ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
22 |
20 21
|
syl |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
23 |
|
nqercl |
|- ( A e. ( N. X. N. ) -> ( /Q ` A ) e. Q. ) |
24 |
|
nqercl |
|- ( B e. ( N. X. N. ) -> ( /Q ` B ) e. Q. ) |
25 |
|
ordpinq |
|- ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( ( /Q ` A ) ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) |
26 |
23 24 25
|
syl2an |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) |
27 |
|
1st2nd2 |
|- ( A e. ( N. X. N. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. ) |
28 |
|
1st2nd2 |
|- ( B e. ( N. X. N. ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. ) |
29 |
27 28
|
breqan12d |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A <. ( 1st ` A ) , ( 2nd ` A ) >. . ) ) |
30 |
|
ordpipq |
|- ( <. ( 1st ` A ) , ( 2nd ` A ) >. . <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) |
31 |
29 30
|
bitrdi |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ( ( 1st ` A ) .N ( 2nd ` B ) ) |
32 |
|
xp1st |
|- ( ( /Q ` A ) e. ( N. X. N. ) -> ( 1st ` ( /Q ` A ) ) e. N. ) |
33 |
23 7 32
|
3syl |
|- ( A e. ( N. X. N. ) -> ( 1st ` ( /Q ` A ) ) e. N. ) |
34 |
|
xp2nd |
|- ( ( /Q ` B ) e. ( N. X. N. ) -> ( 2nd ` ( /Q ` B ) ) e. N. ) |
35 |
24 8 34
|
3syl |
|- ( B e. ( N. X. N. ) -> ( 2nd ` ( /Q ` B ) ) e. N. ) |
36 |
|
mulclpi |
|- ( ( ( 1st ` ( /Q ` A ) ) e. N. /\ ( 2nd ` ( /Q ` B ) ) e. N. ) -> ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) e. N. ) |
37 |
33 35 36
|
syl2an |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) e. N. ) |
38 |
|
ltmpi |
|- ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) e. N. -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) |
39 |
37 38
|
syl |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) ) ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) |
40 |
|
mulcompi |
|- ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
41 |
40
|
a1i |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) ) |
42 |
|
nqerrel |
|- ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) ) |
43 |
23 7
|
syl |
|- ( A e. ( N. X. N. ) -> ( /Q ` A ) e. ( N. X. N. ) ) |
44 |
|
enqbreq2 |
|- ( ( A e. ( N. X. N. ) /\ ( /Q ` A ) e. ( N. X. N. ) ) -> ( A ~Q ( /Q ` A ) <-> ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) = ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) ) ) |
45 |
43 44
|
mpdan |
|- ( A e. ( N. X. N. ) -> ( A ~Q ( /Q ` A ) <-> ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) = ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) ) ) |
46 |
42 45
|
mpbid |
|- ( A e. ( N. X. N. ) -> ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) = ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) ) |
47 |
46
|
eqcomd |
|- ( A e. ( N. X. N. ) -> ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) = ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) ) |
48 |
|
nqerrel |
|- ( B e. ( N. X. N. ) -> B ~Q ( /Q ` B ) ) |
49 |
24 8
|
syl |
|- ( B e. ( N. X. N. ) -> ( /Q ` B ) e. ( N. X. N. ) ) |
50 |
|
enqbreq2 |
|- ( ( B e. ( N. X. N. ) /\ ( /Q ` B ) e. ( N. X. N. ) ) -> ( B ~Q ( /Q ` B ) <-> ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) = ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) ) |
51 |
49 50
|
mpdan |
|- ( B e. ( N. X. N. ) -> ( B ~Q ( /Q ` B ) <-> ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) = ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) ) |
52 |
48 51
|
mpbid |
|- ( B e. ( N. X. N. ) -> ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) = ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) |
53 |
47 52
|
oveqan12d |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) ) |
54 |
|
mulcompi |
|- ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
55 |
|
fvex |
|- ( 1st ` B ) e. _V |
56 |
|
fvex |
|- ( 2nd ` A ) e. _V |
57 |
|
fvex |
|- ( 1st ` ( /Q ` A ) ) e. _V |
58 |
|
mulcompi |
|- ( x .N y ) = ( y .N x ) |
59 |
|
mulasspi |
|- ( ( x .N y ) .N z ) = ( x .N ( y .N z ) ) |
60 |
|
fvex |
|- ( 2nd ` ( /Q ` B ) ) e. _V |
61 |
55 56 57 58 59 60
|
caov411 |
|- ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) = ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
62 |
54 61
|
eqtri |
|- ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
63 |
|
mulcompi |
|- ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) ) = ( ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) |
64 |
|
fvex |
|- ( 1st ` ( /Q ` B ) ) e. _V |
65 |
|
fvex |
|- ( 2nd ` ( /Q ` A ) ) e. _V |
66 |
|
fvex |
|- ( 1st ` A ) e. _V |
67 |
|
fvex |
|- ( 2nd ` B ) e. _V |
68 |
64 65 66 58 59 67
|
caov411 |
|- ( ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) |
69 |
63 68
|
eqtri |
|- ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) |
70 |
53 62 69
|
3eqtr4g |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) ) ) |
71 |
41 70
|
breq12d |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
72 |
31 39 71
|
3bitrd |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) |
73 |
22 26 72
|
3bitr4rd |
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ( /Q ` A ) |
74 |
4 16 73
|
pm5.21nii |
|- ( A ( /Q ` A ) |