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 ) )