Step |
Hyp |
Ref |
Expression |
1 |
|
opex |
|- <. A , B >. e. _V |
2 |
|
opex |
|- <. C , D >. e. _V |
3 |
|
eleq1 |
|- ( x = <. A , B >. -> ( x e. ( N. X. N. ) <-> <. A , B >. e. ( N. X. N. ) ) ) |
4 |
3
|
anbi1d |
|- ( x = <. A , B >. -> ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) <-> ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) ) |
5 |
4
|
anbi1d |
|- ( x = <. A , B >. -> ( ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) |
6 |
|
fveq2 |
|- ( x = <. A , B >. -> ( 1st ` x ) = ( 1st ` <. A , B >. ) ) |
7 |
|
opelxp |
|- ( <. A , B >. e. ( N. X. N. ) <-> ( A e. N. /\ B e. N. ) ) |
8 |
|
op1stg |
|- ( ( A e. N. /\ B e. N. ) -> ( 1st ` <. A , B >. ) = A ) |
9 |
7 8
|
sylbi |
|- ( <. A , B >. e. ( N. X. N. ) -> ( 1st ` <. A , B >. ) = A ) |
10 |
9
|
adantr |
|- ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( 1st ` <. A , B >. ) = A ) |
11 |
6 10
|
sylan9eq |
|- ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( 1st ` x ) = A ) |
12 |
11
|
oveq1d |
|- ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) = ( A .N ( 2nd ` y ) ) ) |
13 |
|
fveq2 |
|- ( x = <. A , B >. -> ( 2nd ` x ) = ( 2nd ` <. A , B >. ) ) |
14 |
|
op2ndg |
|- ( ( A e. N. /\ B e. N. ) -> ( 2nd ` <. A , B >. ) = B ) |
15 |
7 14
|
sylbi |
|- ( <. A , B >. e. ( N. X. N. ) -> ( 2nd ` <. A , B >. ) = B ) |
16 |
15
|
adantr |
|- ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( 2nd ` <. A , B >. ) = B ) |
17 |
13 16
|
sylan9eq |
|- ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( 2nd ` x ) = B ) |
18 |
17
|
oveq2d |
|- ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) = ( ( 1st ` y ) .N B ) ) |
19 |
12 18
|
breq12d |
|- ( ( x = <. A , B >. /\ ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) ( A .N ( 2nd ` y ) ) |
20 |
19
|
pm5.32da |
|- ( x = <. A , B >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) |
21 |
5 20
|
bitrd |
|- ( x = <. A , B >. -> ( ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) |
22 |
|
eleq1 |
|- ( y = <. C , D >. -> ( y e. ( N. X. N. ) <-> <. C , D >. e. ( N. X. N. ) ) ) |
23 |
22
|
anbi2d |
|- ( y = <. C , D >. -> ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) <-> ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) ) |
24 |
23
|
anbi1d |
|- ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) |
25 |
|
fveq2 |
|- ( y = <. C , D >. -> ( 2nd ` y ) = ( 2nd ` <. C , D >. ) ) |
26 |
|
opelxp |
|- ( <. C , D >. e. ( N. X. N. ) <-> ( C e. N. /\ D e. N. ) ) |
27 |
|
op2ndg |
|- ( ( C e. N. /\ D e. N. ) -> ( 2nd ` <. C , D >. ) = D ) |
28 |
26 27
|
sylbi |
|- ( <. C , D >. e. ( N. X. N. ) -> ( 2nd ` <. C , D >. ) = D ) |
29 |
28
|
adantl |
|- ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) -> ( 2nd ` <. C , D >. ) = D ) |
30 |
25 29
|
sylan9eq |
|- ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( 2nd ` y ) = D ) |
31 |
30
|
oveq2d |
|- ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( A .N ( 2nd ` y ) ) = ( A .N D ) ) |
32 |
|
fveq2 |
|- ( y = <. C , D >. -> ( 1st ` y ) = ( 1st ` <. C , D >. ) ) |
33 |
|
op1stg |
|- ( ( C e. N. /\ D e. N. ) -> ( 1st ` <. C , D >. ) = C ) |
34 |
26 33
|
sylbi |
|- ( <. C , D >. e. ( N. X. N. ) -> ( 1st ` <. C , D >. ) = C ) |
35 |
34
|
adantl |
|- ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) -> ( 1st ` <. C , D >. ) = C ) |
36 |
32 35
|
sylan9eq |
|- ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( 1st ` y ) = C ) |
37 |
36
|
oveq1d |
|- ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( ( 1st ` y ) .N B ) = ( C .N B ) ) |
38 |
31 37
|
breq12d |
|- ( ( y = <. C , D >. /\ ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) -> ( ( A .N ( 2nd ` y ) ) ( A .N D ) |
39 |
38
|
pm5.32da |
|- ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) |
40 |
24 39
|
bitrd |
|- ( y = <. C , D >. -> ( ( ( <. A , B >. e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( A .N ( 2nd ` y ) ) ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) |
41 |
|
df-ltpq |
|- . | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) |
42 |
1 2 21 40 41
|
brab |
|- ( <. A , B >. . <-> ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) |
43 |
|
simpr |
|- ( ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) ( A .N D ) |
44 |
|
ltrelpi |
|- |
45 |
44
|
brel |
|- ( ( A .N D ) ( ( A .N D ) e. N. /\ ( C .N B ) e. N. ) ) |
46 |
|
dmmulpi |
|- dom .N = ( N. X. N. ) |
47 |
|
0npi |
|- -. (/) e. N. |
48 |
46 47
|
ndmovrcl |
|- ( ( A .N D ) e. N. -> ( A e. N. /\ D e. N. ) ) |
49 |
46 47
|
ndmovrcl |
|- ( ( C .N B ) e. N. -> ( C e. N. /\ B e. N. ) ) |
50 |
48 49
|
anim12i |
|- ( ( ( A .N D ) e. N. /\ ( C .N B ) e. N. ) -> ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) ) |
51 |
|
opelxpi |
|- ( ( A e. N. /\ B e. N. ) -> <. A , B >. e. ( N. X. N. ) ) |
52 |
51
|
ad2ant2rl |
|- ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> <. A , B >. e. ( N. X. N. ) ) |
53 |
|
simprl |
|- ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> C e. N. ) |
54 |
|
simplr |
|- ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> D e. N. ) |
55 |
53 54
|
opelxpd |
|- ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> <. C , D >. e. ( N. X. N. ) ) |
56 |
52 55
|
jca |
|- ( ( ( A e. N. /\ D e. N. ) /\ ( C e. N. /\ B e. N. ) ) -> ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) |
57 |
45 50 56
|
3syl |
|- ( ( A .N D ) ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) ) |
58 |
57
|
ancri |
|- ( ( A .N D ) ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) |
59 |
43 58
|
impbii |
|- ( ( ( <. A , B >. e. ( N. X. N. ) /\ <. C , D >. e. ( N. X. N. ) ) /\ ( A .N D ) ( A .N D ) |
60 |
42 59
|
bitri |
|- ( <. A , B >. . <-> ( A .N D ) |