Metamath Proof Explorer

Theorem dihmeetlem1N

Description: Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem5a.b 
|- B = ( Base ` K )
dihglblem5a.m 
|- ./\ = ( meet ` K )
dihglblem5a.h 
|- H = ( LHyp ` K )
dihglblem5a.i 
|- I = ( ( DIsoH ` K ) ` W )
dihglblem5a.l 
|- .<_ = ( le ` K )
dihglblem5a.j 
|- .\/ = ( join ` K )
dihglblem5a.a 
|- A = ( Atoms ` K )
dihglblem5a.p 
|- P = ( ( oc ` K ) ` W )
dihglblem5a.t 
|- T = ( ( LTrn ` K ) ` W )
dihglblem5a.r 
|- R = ( ( trL ` K ) ` W )
dihglblem5a.e 
|- E = ( ( TEndo ` K ) ` W )
dihglblem5a.g 
|- G = ( iota_ h e. T ( h ` P ) = q )
dihglblem5a.o 
|- .0. = ( h e. T |-> ( _I |` B ) )
Assertion dihmeetlem1N 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = ( ( I ` X ) i^i ( I ` Y ) ) )

Proof

Step Hyp Ref Expression
1 dihglblem5a.b 
 |-  B = ( Base ` K )
2 dihglblem5a.m 
 |-  ./\ = ( meet ` K )
3 dihglblem5a.h 
 |-  H = ( LHyp ` K )
4 dihglblem5a.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 dihglblem5a.l 
 |-  .<_ = ( le ` K )
6 dihglblem5a.j 
 |-  .\/ = ( join ` K )
7 dihglblem5a.a 
 |-  A = ( Atoms ` K )
8 dihglblem5a.p 
 |-  P = ( ( oc ` K ) ` W )
9 dihglblem5a.t 
 |-  T = ( ( LTrn ` K ) ` W )
10 dihglblem5a.r 
 |-  R = ( ( trL ` K ) ` W )
11 dihglblem5a.e 
 |-  E = ( ( TEndo ` K ) ` W )
12 dihglblem5a.g 
 |-  G = ( iota_ h e. T ( h ` P ) = q )
13 dihglblem5a.o 
 |-  .0. = ( h e. T |-> ( _I |` B ) )
14 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> K e. HL )
15 14 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> K e. Lat )
16 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> X e. B )
17 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> Y e. B )
18 1 5 2 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
19 15 16 17 18 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) .<_ X )
20 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( K e. HL /\ W e. H ) )
21 1 2 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
22 15 16 17 21 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) e. B )
23 1 5 3 4 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( I ` ( X ./\ Y ) ) C_ ( I ` X ) <-> ( X ./\ Y ) .<_ X ) )
24 20 22 16 23 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` ( X ./\ Y ) ) C_ ( I ` X ) <-> ( X ./\ Y ) .<_ X ) )
25 19 24 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) C_ ( I ` X ) )
26 1 5 2 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y )
27 15 16 17 26 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( X ./\ Y ) .<_ Y )
28 1 5 3 4 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X ./\ Y ) e. B /\ Y e. B ) -> ( ( I ` ( X ./\ Y ) ) C_ ( I ` Y ) <-> ( X ./\ Y ) .<_ Y ) )
29 20 22 17 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` ( X ./\ Y ) ) C_ ( I ` Y ) <-> ( X ./\ Y ) .<_ Y ) )
30 27 29 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) C_ ( I ` Y ) )
31 25 30 ssind 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) C_ ( ( I ` X ) i^i ( I ` Y ) ) )
32 3 4 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` X ) )
33 relin1 
 |-  ( Rel ( I ` X ) -> Rel ( ( I ` X ) i^i ( I ` Y ) ) )
34 32 33 syl 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( ( I ` X ) i^i ( I ` Y ) ) )
35 34 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> Rel ( ( I ` X ) i^i ( I ` Y ) ) )
36 elin 
 |-  ( <. f , s >. e. ( ( I ` X ) i^i ( I ` Y ) ) <-> ( <. f , s >. e. ( I ` X ) /\ <. f , s >. e. ( I ` Y ) ) )
37 1 5 6 2 7 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) )
38 37 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) )
39 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( K e. HL /\ W e. H ) )
40 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( X e. B /\ -. X .<_ W ) )
41 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> q e. A )
42 simprrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> -. q .<_ W )
43 41 42 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( q e. A /\ -. q .<_ W ) )
44 simprrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( q .\/ ( X ./\ W ) ) = X )
45 vex 
 |-  f e. _V
46 vex 
 |-  s e. _V
47 1 5 6 2 7 3 8 9 10 11 4 12 45 46 dihopelvalc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) -> ( <. f , s >. e. ( I ` X ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) ) )
48 39 40 43 44 47 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( <. f , s >. e. ( I ` X ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) ) )
49 simpr 
 |-  ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) -> ( R ` ( f o. `' ( s ` G ) ) ) .<_ X )
50 48 49 syl6bi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( <. f , s >. e. ( I ` X ) -> ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) )
51 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( Y e. B /\ Y .<_ W ) )
52 1 5 3 9 10 13 4 dihopelvalbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( <. f , s >. e. ( I ` Y ) <-> ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) )
53 39 51 52 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( <. f , s >. e. ( I ` Y ) <-> ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) )
54 53 biimpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( <. f , s >. e. ( I ` Y ) -> ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) )
55 simprll 
 |-  ( ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) -> f e. T )
56 55 3ad2ant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> f e. T )
57 simp3rr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> s = .0. )
58 57 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( s ` G ) = ( .0. ` G ) )
59 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( K e. HL /\ W e. H ) )
60 5 7 3 8 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
61 59 60 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( P e. A /\ -. P .<_ W ) )
62 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> q e. A )
63 simp2rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> -. q .<_ W )
64 5 7 3 9 12 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( q e. A /\ -. q .<_ W ) ) -> G e. T )
65 59 61 62 63 64 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> G e. T )
66 13 1 tendo02 
 |-  ( G e. T -> ( .0. ` G ) = ( _I |` B ) )
67 65 66 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( .0. ` G ) = ( _I |` B ) )
68 58 67 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( s ` G ) = ( _I |` B ) )
69 68 cnveqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> `' ( s ` G ) = `' ( _I |` B ) )
70 cnvresid 
 |-  `' ( _I |` B ) = ( _I |` B )
71 69 70 eqtrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> `' ( s ` G ) = ( _I |` B ) )
72 71 coeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( f o. `' ( s ` G ) ) = ( f o. ( _I |` B ) ) )
73 1 3 9 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> f : B -1-1-onto-> B )
74 59 56 73 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> f : B -1-1-onto-> B )
75 f1of 
 |-  ( f : B -1-1-onto-> B -> f : B --> B )
76 fcoi1 
 |-  ( f : B --> B -> ( f o. ( _I |` B ) ) = f )
77 74 75 76 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( f o. ( _I |` B ) ) = f )
78 72 77 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( f o. `' ( s ` G ) ) = f )
79 78 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( R ` ( f o. `' ( s ` G ) ) ) = ( R ` f ) )
80 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( R ` ( f o. `' ( s ` G ) ) ) .<_ X )
81 79 80 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( R ` f ) .<_ X )
82 simprlr 
 |-  ( ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) -> ( R ` f ) .<_ Y )
83 82 3ad2ant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( R ` f ) .<_ Y )
84 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> K e. HL )
85 84 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> K e. Lat )
86 1 3 9 10 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( R ` f ) e. B )
87 59 56 86 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( R ` f ) e. B )
88 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> X e. B )
89 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> Y e. B )
90 1 5 2 latlem12 
 |-  ( ( K e. Lat /\ ( ( R ` f ) e. B /\ X e. B /\ Y e. B ) ) -> ( ( ( R ` f ) .<_ X /\ ( R ` f ) .<_ Y ) <-> ( R ` f ) .<_ ( X ./\ Y ) ) )
91 85 87 88 89 90 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( ( ( R ` f ) .<_ X /\ ( R ` f ) .<_ Y ) <-> ( R ` f ) .<_ ( X ./\ Y ) ) )
92 81 83 91 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( R ` f ) .<_ ( X ./\ Y ) )
93 56 92 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( f e. T /\ ( R ` f ) .<_ ( X ./\ Y ) ) )
94 85 88 89 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( X ./\ Y ) e. B )
95 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> W e. H )
96 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
97 95 96 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> W e. B )
98 85 88 89 26 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( X ./\ Y ) .<_ Y )
99 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> Y .<_ W )
100 1 5 85 94 89 97 98 99 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( X ./\ Y ) .<_ W )
101 1 5 3 9 10 13 4 dihopelvalbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ Y ) e. B /\ ( X ./\ Y ) .<_ W ) ) -> ( <. f , s >. e. ( I ` ( X ./\ Y ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ Y ) ) /\ s = .0. ) ) )
102 59 94 100 101 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> ( <. f , s >. e. ( I ` ( X ./\ Y ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ Y ) ) /\ s = .0. ) ) )
103 93 57 102 mpbir2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) ) -> <. f , s >. e. ( I ` ( X ./\ Y ) ) )
104 103 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( ( ( R ` ( f o. `' ( s ` G ) ) ) .<_ X /\ ( ( f e. T /\ ( R ` f ) .<_ Y ) /\ s = .0. ) ) -> <. f , s >. e. ( I ` ( X ./\ Y ) ) ) )
105 50 54 104 syl2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) /\ ( q e. A /\ ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) ) -> ( ( <. f , s >. e. ( I ` X ) /\ <. f , s >. e. ( I ` Y ) ) -> <. f , s >. e. ( I ` ( X ./\ Y ) ) ) )
106 38 105 rexlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( <. f , s >. e. ( I ` X ) /\ <. f , s >. e. ( I ` Y ) ) -> <. f , s >. e. ( I ` ( X ./\ Y ) ) ) )
107 36 106 syl5bi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( <. f , s >. e. ( ( I ` X ) i^i ( I ` Y ) ) -> <. f , s >. e. ( I ` ( X ./\ Y ) ) ) )
108 35 107 relssdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( ( I ` X ) i^i ( I ` Y ) ) C_ ( I ` ( X ./\ Y ) ) )
109 31 108 eqssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ Y .<_ W ) ) -> ( I ` ( X ./\ Y ) ) = ( ( I ` X ) i^i ( I ` Y ) ) )