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