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

Metamath Proof Explorer

Theorem dihglbcpreN

Description: Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane W . (Contributed by NM, 20-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglbc.b 
|- B = ( Base ` K )
dihglbc.g 
|- G = ( glb ` K )
dihglbc.h 
|- H = ( LHyp ` K )
dihglbc.i 
|- I = ( ( DIsoH ` K ) ` W )
dihglbc.l 
|- .<_ = ( le ` K )
dihglbcpre.j 
|- .\/ = ( join ` K )
dihglbcpre.m 
|- ./\ = ( meet ` K )
dihglbcpre.a 
|- A = ( Atoms ` K )
dihglbcpre.p 
|- P = ( ( oc ` K ) ` W )
dihglbcpre.t 
|- T = ( ( LTrn ` K ) ` W )
dihglbcpre.r 
|- R = ( ( trL ` K ) ` W )
dihglbcpre.e 
|- E = ( ( TEndo ` K ) ` W )
dihglbcpre.f 
|- F = ( iota_ g e. T ( g ` P ) = q )
Assertion dihglbcpreN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )

Proof

Step Hyp Ref Expression
1 dihglbc.b 
 |-  B = ( Base ` K )
2 dihglbc.g 
 |-  G = ( glb ` K )
3 dihglbc.h 
 |-  H = ( LHyp ` K )
4 dihglbc.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 dihglbc.l 
 |-  .<_ = ( le ` K )
6 dihglbcpre.j 
 |-  .\/ = ( join ` K )
7 dihglbcpre.m 
 |-  ./\ = ( meet ` K )
8 dihglbcpre.a 
 |-  A = ( Atoms ` K )
9 dihglbcpre.p 
 |-  P = ( ( oc ` K ) ` W )
10 dihglbcpre.t 
 |-  T = ( ( LTrn ` K ) ` W )
11 dihglbcpre.r 
 |-  R = ( ( trL ` K ) ` W )
12 dihglbcpre.e 
 |-  E = ( ( TEndo ` K ) ` W )
13 dihglbcpre.f 
 |-  F = ( iota_ g e. T ( g ` P ) = q )
14 3 4 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` ( G ` S ) ) )
15 14 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> Rel ( I ` ( G ` S ) ) )
16 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> S =/= (/) )
17 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
18 16 17 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. x x e. S )
19 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> x e. S )
20 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> ( K e. HL /\ W e. H ) )
21 3 4 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` x ) )
22 20 21 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> Rel ( I ` x ) )
23 19 22 jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ x e. S ) -> ( x e. S /\ Rel ( I ` x ) ) )
24 23 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( x e. S -> ( x e. S /\ Rel ( I ` x ) ) ) )
25 24 eximdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( E. x x e. S -> E. x ( x e. S /\ Rel ( I ` x ) ) ) )
26 18 25 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. x ( x e. S /\ Rel ( I ` x ) ) )
27 df-rex 
 |-  ( E. x e. S Rel ( I ` x ) <-> E. x ( x e. S /\ Rel ( I ` x ) ) )
28 26 27 sylibr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. x e. S Rel ( I ` x ) )
29 reliin 
 |-  ( E. x e. S Rel ( I ` x ) -> Rel |^|_ x e. S ( I ` x ) )
30 28 29 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> Rel |^|_ x e. S ( I ` x ) )
31 id 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) )
32 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( K e. HL /\ W e. H ) )
33 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> K e. HL )
34 hlclat 
 |-  ( K e. HL -> K e. CLat )
35 33 34 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> K e. CLat )
36 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> S C_ B )
37 1 2 clatglbcl 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
38 35 36 37 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( G ` S ) e. B )
39 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> -. ( G ` S ) .<_ W )
40 1 5 6 7 8 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. B /\ -. ( G ` S ) .<_ W ) ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) )
41 32 38 39 40 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> E. q e. A ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) )
42 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( K e. HL /\ W e. H ) )
43 38 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( G ` S ) e. B )
44 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> -. ( G ` S ) .<_ W )
45 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) )
46 vex 
 |-  f e. _V
47 vex 
 |-  s e. _V
48 1 5 6 7 8 3 9 10 11 12 4 13 46 47 dihopelvalc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( G ` S ) e. B /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) ) )
49 42 43 44 45 48 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) ) )
50 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> S =/= (/) )
51 r19.28zv 
 |-  ( S =/= (/) -> ( A. x e. S ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) <-> ( ( f e. T /\ s e. E ) /\ A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) )
52 50 51 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( A. x e. S ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) <-> ( ( f e. T /\ s e. E ) /\ A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) )
53 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( K e. HL /\ W e. H ) )
54 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> S C_ B )
55 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> x e. S )
56 54 55 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> x e. B )
57 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> -. ( G ` S ) .<_ W )
58 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. HL )
59 58 34 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. CLat )
60 1 5 2 clatglble 
 |-  ( ( K e. CLat /\ S C_ B /\ x e. S ) -> ( G ` S ) .<_ x )
61 59 54 55 60 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( G ` S ) .<_ x )
62 58 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. Lat )
63 38 3ad2ant1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( G ` S ) e. B )
64 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> W e. H )
65 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
66 64 65 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> W e. B )
67 1 5 lattr 
 |-  ( ( K e. Lat /\ ( ( G ` S ) e. B /\ x e. B /\ W e. B ) ) -> ( ( ( G ` S ) .<_ x /\ x .<_ W ) -> ( G ` S ) .<_ W ) )
68 62 63 56 66 67 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( ( ( G ` S ) .<_ x /\ x .<_ W ) -> ( G ` S ) .<_ W ) )
69 61 68 mpand 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( x .<_ W -> ( G ` S ) .<_ W ) )
70 57 69 mtod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> -. x .<_ W )
71 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q e. A /\ -. q .<_ W ) )
72 simp2ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q e. A )
73 1 8 atbase 
 |-  ( q e. A -> q e. B )
74 72 73 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q e. B )
75 1 7 latmcl 
 |-  ( ( K e. Lat /\ ( G ` S ) e. B /\ W e. B ) -> ( ( G ` S ) ./\ W ) e. B )
76 62 63 66 75 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( ( G ` S ) ./\ W ) e. B )
77 1 5 6 latlej1 
 |-  ( ( K e. Lat /\ q e. B /\ ( ( G ` S ) ./\ W ) e. B ) -> q .<_ ( q .\/ ( ( G ` S ) ./\ W ) ) )
78 62 74 76 77 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q .<_ ( q .\/ ( ( G ` S ) ./\ W ) ) )
79 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) )
80 78 79 breqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q .<_ ( G ` S ) )
81 1 5 62 74 63 56 80 61 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> q .<_ x )
82 1 5 6 7 8 atmod3i1 
 |-  ( ( K e. HL /\ ( q e. A /\ x e. B /\ W e. B ) /\ q .<_ x ) -> ( q .\/ ( x ./\ W ) ) = ( x ./\ ( q .\/ W ) ) )
83 58 72 56 66 81 82 syl131anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ ( x ./\ W ) ) = ( x ./\ ( q .\/ W ) ) )
84 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
85 5 6 84 8 3 lhpjat2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( q .\/ W ) = ( 1. ` K ) )
86 53 71 85 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ W ) = ( 1. ` K ) )
87 86 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( x ./\ ( q .\/ W ) ) = ( x ./\ ( 1. ` K ) ) )
88 hlol 
 |-  ( K e. HL -> K e. OL )
89 58 88 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> K e. OL )
90 1 7 84 olm11 
 |-  ( ( K e. OL /\ x e. B ) -> ( x ./\ ( 1. ` K ) ) = x )
91 89 56 90 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( x ./\ ( 1. ` K ) ) = x )
92 83 87 91 3eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( q .\/ ( x ./\ W ) ) = x )
93 1 5 6 7 8 3 9 10 11 12 4 13 46 47 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 ` F ) ) ) .<_ x ) ) )
94 53 56 70 71 92 93 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ x e. S ) -> ( <. f , s >. e. ( I ` x ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) )
95 94 3expa 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) /\ x e. S ) -> ( <. f , s >. e. ( I ` x ) <-> ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) )
96 95 ralbidva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( A. x e. S <. f , s >. e. ( I ` x ) <-> A. x e. S ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) )
97 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> K e. HL )
98 97 34 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> K e. CLat )
99 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( K e. HL /\ W e. H ) )
100 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> f e. T )
101 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> s e. E )
102 5 8 3 9 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
103 99 102 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( P e. A /\ -. P .<_ W ) )
104 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( q e. A /\ -. q .<_ W ) )
105 5 8 3 10 13 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( q e. A /\ -. q .<_ W ) ) -> F e. T )
106 99 103 104 105 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> F e. T )
107 3 10 12 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( s ` F ) e. T )
108 99 101 106 107 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( s ` F ) e. T )
109 3 10 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s ` F ) e. T ) -> `' ( s ` F ) e. T )
110 99 108 109 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> `' ( s ` F ) e. T )
111 3 10 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ `' ( s ` F ) e. T ) -> ( f o. `' ( s ` F ) ) e. T )
112 99 100 110 111 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( f o. `' ( s ` F ) ) e. T )
113 1 3 10 11 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f o. `' ( s ` F ) ) e. T ) -> ( R ` ( f o. `' ( s ` F ) ) ) e. B )
114 99 112 113 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( R ` ( f o. `' ( s ` F ) ) ) e. B )
115 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> S C_ B )
116 1 5 2 clatleglb 
 |-  ( ( K e. CLat /\ ( R ` ( f o. `' ( s ` F ) ) ) e. B /\ S C_ B ) -> ( ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) <-> A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) )
117 98 114 115 116 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) /\ ( f e. T /\ s e. E ) ) -> ( ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) <-> A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) )
118 117 3expa 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) /\ ( f e. T /\ s e. E ) ) -> ( ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) <-> A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) )
119 118 pm5.32da 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) <-> ( ( f e. T /\ s e. E ) /\ A. x e. S ( R ` ( f o. `' ( s ` F ) ) ) .<_ x ) ) )
120 52 96 119 3bitr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) <-> A. x e. S <. f , s >. e. ( I ` x ) ) )
121 opex 
 |-  <. f , s >. e. _V
122 eliin 
 |-  ( <. f , s >. e. _V -> ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S <. f , s >. e. ( I ` x ) ) )
123 121 122 ax-mp 
 |-  ( <. f , s >. e. |^|_ x e. S ( I ` x ) <-> A. x e. S <. f , s >. e. ( I ` x ) )
124 120 123 bitr4di 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( ( ( f e. T /\ s e. E ) /\ ( R ` ( f o. `' ( s ` F ) ) ) .<_ ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) )
125 49 124 bitrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) /\ ( ( q e. A /\ -. q .<_ W ) /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) )
126 125 exp44 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( q e. A -> ( -. q .<_ W -> ( ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) ) ) )
127 126 imp4a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( q e. A -> ( ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) ) )
128 127 rexlimdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( E. q e. A ( -. q .<_ W /\ ( q .\/ ( ( G ` S ) ./\ W ) ) = ( G ` S ) ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) ) )
129 41 128 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( <. f , s >. e. ( I ` ( G ` S ) ) <-> <. f , s >. e. |^|_ x e. S ( I ` x ) ) )
130 129 eqrelrdv2 
 |-  ( ( ( Rel ( I ` ( G ` S ) ) /\ Rel |^|_ x e. S ( I ` x ) ) /\ ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )
131 15 30 31 130 syl21anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) /\ -. ( G ` S ) .<_ W ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )