Metamath Proof Explorer

Theorem dihord

Description: The isomorphism H is order-preserving. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord.b 
|- B = ( Base ` K )
dihord.l 
|- .<_ = ( le ` K )
dihord.h 
|- H = ( LHyp ` K )
dihord.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihord 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )

Proof

Step Hyp Ref Expression
1 dihord.b 
 |-  B = ( Base ` K )
2 dihord.l 
 |-  .<_ = ( le ` K )
3 dihord.h 
 |-  H = ( LHyp ` K )
4 dihord.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ Y .<_ W ) ) -> ( K e. HL /\ W e. H ) )
6 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ Y .<_ W ) ) -> X e. B )
7 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ Y .<_ W ) ) -> X .<_ W )
8 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ Y .<_ W ) ) -> Y e. B )
9 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ Y .<_ W ) ) -> Y .<_ W )
10 1 2 3 4 dihord3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
11 5 6 7 8 9 10 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
12 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ -. Y .<_ W ) ) -> ( K e. HL /\ W e. H ) )
13 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ -. Y .<_ W ) ) -> X e. B )
14 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ -. Y .<_ W ) ) -> X .<_ W )
15 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ -. Y .<_ W ) ) -> Y e. B )
16 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ -. Y .<_ W ) ) -> -. Y .<_ W )
17 1 2 3 4 dihord5a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y )
18 1 2 3 4 dihord5b 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( I ` X ) C_ ( I ` Y ) )
19 17 18 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
20 12 13 14 15 16 19 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( X .<_ W /\ -. Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
21 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ Y .<_ W ) ) -> ( K e. HL /\ W e. H ) )
22 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ Y .<_ W ) ) -> X e. B )
23 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ Y .<_ W ) ) -> -. X .<_ W )
24 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ Y .<_ W ) ) -> Y e. B )
25 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ Y .<_ W ) ) -> Y .<_ W )
26 1 2 3 4 dihord6a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( I ` X ) C_ ( I ` Y ) ) -> X .<_ Y )
27 1 2 3 4 dihord6b 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ X .<_ Y ) -> ( I ` X ) C_ ( I ` Y ) )
28 26 27 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
29 21 22 23 24 25 28 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
30 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ -. Y .<_ W ) ) -> ( K e. HL /\ W e. H ) )
31 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ -. Y .<_ W ) ) -> X e. B )
32 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ -. Y .<_ W ) ) -> -. X .<_ W )
33 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ -. Y .<_ W ) ) -> Y e. B )
34 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ -. Y .<_ W ) ) -> -. Y .<_ W )
35 1 2 3 4 dihord4 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
36 30 31 32 33 34 35 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) /\ ( -. X .<_ W /\ -. Y .<_ W ) ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )
37 11 20 29 36 4casesdan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ Y e. B ) -> ( ( I ` X ) C_ ( I ` Y ) <-> X .<_ Y ) )