This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihglblem5apreN

Description: A conjunction property of isomorphism H. TODO: reduce antecedent size; general review for shorter proof. (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 dihglblem5apreN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` ( X ./\ W ) ) = ( ( I ` X ) i^i ( I ` W ) ) )

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 hllat 
 |-  ( K e. HL -> K e. Lat )
15 14 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> K e. Lat )
16 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> X e. B )
17 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
18 17 ad2antlr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> W e. B )
19 1 5 2 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ X )
20 15 16 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( X ./\ W ) .<_ X )
21 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( K e. HL /\ W e. H ) )
22 1 2 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) e. B )
23 15 16 18 22 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( X ./\ W ) e. B )
24 1 5 3 4 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X ./\ W ) e. B /\ X e. B ) -> ( ( I ` ( X ./\ W ) ) C_ ( I ` X ) <-> ( X ./\ W ) .<_ X ) )
25 21 23 16 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( ( I ` ( X ./\ W ) ) C_ ( I ` X ) <-> ( X ./\ W ) .<_ X ) )
26 20 25 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` ( X ./\ W ) ) C_ ( I ` X ) )
27 1 5 2 latmle2 
 |-  ( ( K e. Lat /\ X e. B /\ W e. B ) -> ( X ./\ W ) .<_ W )
28 15 16 18 27 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( X ./\ W ) .<_ W )
29 1 5 3 4 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X ./\ W ) e. B /\ W e. B ) -> ( ( I ` ( X ./\ W ) ) C_ ( I ` W ) <-> ( X ./\ W ) .<_ W ) )
30 21 23 18 29 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( ( I ` ( X ./\ W ) ) C_ ( I ` W ) <-> ( X ./\ W ) .<_ W ) )
31 28 30 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` ( X ./\ W ) ) C_ ( I ` W ) )
32 26 31 ssind 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` ( X ./\ W ) ) C_ ( ( I ` X ) i^i ( I ` W ) ) )
33 3 4 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` X ) )
34 relin1 
 |-  ( Rel ( I ` X ) -> Rel ( ( I ` X ) i^i ( I ` W ) ) )
35 33 34 syl 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( ( I ` X ) i^i ( I ` W ) ) )
36 35 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> Rel ( ( I ` X ) i^i ( I ` W ) ) )
37 elin 
 |-  ( <. f , s >. e. ( ( I ` X ) i^i ( I ` W ) ) <-> ( <. f , s >. e. ( I ` X ) /\ <. f , s >. e. ( I ` W ) ) )
38 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 ) )
39 vex 
 |-  f e. _V
40 vex 
 |-  s e. _V
41 1 5 6 2 7 3 8 9 10 11 4 12 39 40 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 ) ) )
42 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
43 17 adantl 
 |-  ( ( K e. HL /\ W e. H ) -> W e. B )
44 1 5 latref 
 |-  ( ( K e. Lat /\ W e. B ) -> W .<_ W )
45 14 17 44 syl2an 
 |-  ( ( K e. HL /\ W e. H ) -> W .<_ W )
46 1 5 3 9 10 13 4 dihopelvalbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( W e. B /\ W .<_ W ) ) -> ( <. f , s >. e. ( I ` W ) <-> ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) )
47 42 43 45 46 syl12anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( <. f , s >. e. ( I ` W ) <-> ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) )
48 47 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) -> ( <. f , s >. e. ( I ` W ) <-> ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) )
49 41 48 anbi12d 
 |-  ( ( ( 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 , s >. e. ( I ` W ) ) <-> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) )
50 simprll 
 |-  ( ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) -> f e. T )
51 50 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> f e. T )
52 simprrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> s = .0. )
53 52 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( s ` G ) = ( .0. ` G ) )
54 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( K e. HL /\ W e. H ) )
55 5 7 3 8 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
56 54 55 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( P e. A /\ -. P .<_ W ) )
57 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( q e. A /\ -. q .<_ W ) )
58 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 )
59 54 56 57 58 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> G e. T )
60 13 1 tendo02 
 |-  ( G e. T -> ( .0. ` G ) = ( _I |` B ) )
61 59 60 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( .0. ` G ) = ( _I |` B ) )
62 53 61 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( s ` G ) = ( _I |` B ) )
63 62 cnveqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> `' ( s ` G ) = `' ( _I |` B ) )
64 cnvresid 
 |-  `' ( _I |` B ) = ( _I |` B )
65 63 64 eqtrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> `' ( s ` G ) = ( _I |` B ) )
66 65 coeq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( f o. `' ( s ` G ) ) = ( f o. ( _I |` B ) ) )
67 1 3 9 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> f : B -1-1-onto-> B )
68 54 51 67 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> f : B -1-1-onto-> B )
69 f1of 
 |-  ( f : B -1-1-onto-> B -> f : B --> B )
70 fcoi1 
 |-  ( f : B --> B -> ( f o. ( _I |` B ) ) = f )
71 68 69 70 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( f o. ( _I |` B ) ) = f )
72 66 71 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( f o. `' ( s ` G ) ) = f )
73 72 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( R ` ( f o. `' ( s ` G ) ) ) = ( R ` f ) )
74 simprlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( R ` ( f o. `' ( s ` G ) ) ) .<_ X )
75 73 74 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( R ` f ) .<_ X )
76 5 3 9 10 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( R ` f ) .<_ W )
77 54 51 76 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( R ` f ) .<_ W )
78 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> K e. HL )
79 78 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> K e. Lat )
80 1 3 9 10 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T ) -> ( R ` f ) e. B )
81 54 51 80 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( R ` f ) e. B )
82 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> X e. B )
83 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> W e. H )
84 83 17 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> W e. B )
85 1 5 2 latlem12 
 |-  ( ( K e. Lat /\ ( ( R ` f ) e. B /\ X e. B /\ W e. B ) ) -> ( ( ( R ` f ) .<_ X /\ ( R ` f ) .<_ W ) <-> ( R ` f ) .<_ ( X ./\ W ) ) )
86 79 81 82 84 85 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( ( ( R ` f ) .<_ X /\ ( R ` f ) .<_ W ) <-> ( R ` f ) .<_ ( X ./\ W ) ) )
87 75 77 86 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( R ` f ) .<_ ( X ./\ W ) )
88 51 87 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) )
89 79 82 84 22 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( X ./\ W ) e. B )
90 79 82 84 27 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( X ./\ W ) .<_ W )
91 1 5 3 9 10 13 4 dihopelvalbN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( X ./\ W ) e. B /\ ( X ./\ W ) .<_ W ) ) -> ( <. f , s >. e. ( I ` ( X ./\ W ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = .0. ) ) )
92 54 89 90 91 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> ( <. f , s >. e. ( I ` ( X ./\ W ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ ( X ./\ W ) ) /\ s = .0. ) ) )
93 88 52 92 mpbir2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) /\ ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) )
94 93 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( X ./\ W ) ) = X ) ) -> ( ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` G ) ) ) .<_ X ) /\ ( ( f e. T /\ ( R ` f ) .<_ W ) /\ s = .0. ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) )
95 49 94 sylbid 
 |-  ( ( ( 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 , s >. e. ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) )
96 95 3expia 
 |-  ( ( ( 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 , s >. e. ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) ) )
97 96 exp4c 
 |-  ( ( ( 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 , s >. e. ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) ) ) ) )
98 97 imp4a 
 |-  ( ( ( 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 , s >. e. ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) ) ) )
99 98 rexlimdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( E. q e. A ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> ( ( <. f , s >. e. ( I ` X ) /\ <. f , s >. e. ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) ) )
100 38 99 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( ( <. f , s >. e. ( I ` X ) /\ <. f , s >. e. ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) )
101 37 100 biimtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( <. f , s >. e. ( ( I ` X ) i^i ( I ` W ) ) -> <. f , s >. e. ( I ` ( X ./\ W ) ) ) )
102 36 101 relssdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( ( I ` X ) i^i ( I ` W ) ) C_ ( I ` ( X ./\ W ) ) )
103 32 102 eqssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( I ` ( X ./\ W ) ) = ( ( I ` X ) i^i ( I ` W ) ) )