Metamath Proof Explorer

Theorem dihglblem6

Description: Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014)

Ref Expression
Hypotheses dihglblem6.b 
|- B = ( Base ` K )
dihglblem6.l 
|- .<_ = ( le ` K )
dihglblem6.m 
|- ./\ = ( meet ` K )
dihglblem6.a 
|- A = ( Atoms ` K )
dihglblem6.g 
|- G = ( glb ` K )
dihglblem6.h 
|- H = ( LHyp ` K )
dihglblem6.i 
|- I = ( ( DIsoH ` K ) ` W )
dihglblem6.u 
|- U = ( ( DVecH ` K ) ` W )
dihglblem6.s 
|- P = ( LSubSp ` U )
dihglblem6.d 
|- D = ( LSAtoms ` U )
Assertion dihglblem6 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )

Proof

Step Hyp Ref Expression
1 dihglblem6.b 
 |-  B = ( Base ` K )
2 dihglblem6.l 
 |-  .<_ = ( le ` K )
3 dihglblem6.m 
 |-  ./\ = ( meet ` K )
4 dihglblem6.a 
 |-  A = ( Atoms ` K )
5 dihglblem6.g 
 |-  G = ( glb ` K )
6 dihglblem6.h 
 |-  H = ( LHyp ` K )
7 dihglblem6.i 
 |-  I = ( ( DIsoH ` K ) ` W )
8 dihglblem6.u 
 |-  U = ( ( DVecH ` K ) ` W )
9 dihglblem6.s 
 |-  P = ( LSubSp ` U )
10 dihglblem6.d 
 |-  D = ( LSAtoms ` U )
11 eqid 
 |-  ( meet ` K ) = ( meet ` K )
12 eqid 
 |-  { u e. B | E. v e. S u = ( v ( meet ` K ) W ) } = { u e. B | E. v e. S u = ( v ( meet ` K ) W ) }
13 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
14 1 2 11 5 6 12 13 7 dihglblem4 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) )
15 fal 
 |-  -. F.
16 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> ( K e. HL /\ W e. H ) )
17 6 8 16 dvhlmod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> U e. LMod )
18 simplll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> K e. HL )
19 hlclat 
 |-  ( K e. HL -> K e. CLat )
20 18 19 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> K e. CLat )
21 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> S C_ B )
22 1 5 clatglbcl 
 |-  ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
23 20 21 22 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> ( G ` S ) e. B )
24 1 6 7 8 9 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G ` S ) e. B ) -> ( I ` ( G ` S ) ) e. P )
25 16 23 24 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> ( I ` ( G ` S ) ) e. P )
26 1 5 6 8 7 9 dihglblem5 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> |^|_ x e. S ( I ` x ) e. P )
27 26 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> |^|_ x e. S ( I ` x ) e. P )
28 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) )
29 9 10 17 25 27 28 lpssat 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) ) -> E. p e. D ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) )
30 29 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) -> E. p e. D ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) )
31 simp1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( K e. HL /\ W e. H ) )
32 6 8 7 10 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. D ) -> p e. ran I )
33 32 adantlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> p e. ran I )
34 33 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> p e. ran I )
35 6 7 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ran I ) -> ( I ` ( `' I ` p ) ) = p )
36 31 34 35 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( I ` ( `' I ` p ) ) = p )
37 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> p C_ |^|_ x e. S ( I ` x ) )
38 ssiin 
 |-  ( p C_ |^|_ x e. S ( I ` x ) <-> A. x e. S p C_ ( I ` x ) )
39 37 38 sylib 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> A. x e. S p C_ ( I ` x ) )
40 simplll 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> ( K e. HL /\ W e. H ) )
41 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> ( K e. HL /\ W e. H ) )
42 1 6 7 8 9 dihf11 
 |-  ( ( K e. HL /\ W e. H ) -> I : B -1-1-> P )
43 f1f1orn 
 |-  ( I : B -1-1-> P -> I : B -1-1-onto-> ran I )
44 41 42 43 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> I : B -1-1-onto-> ran I )
45 f1ocnvdm 
 |-  ( ( I : B -1-1-onto-> ran I /\ p e. ran I ) -> ( `' I ` p ) e. B )
46 44 33 45 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> ( `' I ` p ) e. B )
47 46 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> ( `' I ` p ) e. B )
48 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> S C_ B )
49 48 sselda 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> x e. B )
50 1 2 6 7 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` p ) e. B /\ x e. B ) -> ( ( I ` ( `' I ` p ) ) C_ ( I ` x ) <-> ( `' I ` p ) .<_ x ) )
51 40 47 49 50 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> ( ( I ` ( `' I ` p ) ) C_ ( I ` x ) <-> ( `' I ` p ) .<_ x ) )
52 41 33 35 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> ( I ` ( `' I ` p ) ) = p )
53 52 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> ( I ` ( `' I ` p ) ) = p )
54 53 sseq1d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> ( ( I ` ( `' I ` p ) ) C_ ( I ` x ) <-> p C_ ( I ` x ) ) )
55 51 54 bitr3d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) /\ x e. S ) -> ( ( `' I ` p ) .<_ x <-> p C_ ( I ` x ) ) )
56 55 ralbidva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D ) -> ( A. x e. S ( `' I ` p ) .<_ x <-> A. x e. S p C_ ( I ` x ) ) )
57 56 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( A. x e. S ( `' I ` p ) .<_ x <-> A. x e. S p C_ ( I ` x ) ) )
58 39 57 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> A. x e. S ( `' I ` p ) .<_ x )
59 simp1ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> K e. HL )
60 59 19 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> K e. CLat )
61 46 3adant3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( `' I ` p ) e. B )
62 simp1rl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> S C_ B )
63 1 2 5 clatleglb 
 |-  ( ( K e. CLat /\ ( `' I ` p ) e. B /\ S C_ B ) -> ( ( `' I ` p ) .<_ ( G ` S ) <-> A. x e. S ( `' I ` p ) .<_ x ) )
64 60 61 62 63 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( ( `' I ` p ) .<_ ( G ` S ) <-> A. x e. S ( `' I ` p ) .<_ x ) )
65 58 64 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( `' I ` p ) .<_ ( G ` S ) )
66 60 62 22 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( G ` S ) e. B )
67 1 2 6 7 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` p ) e. B /\ ( G ` S ) e. B ) -> ( ( I ` ( `' I ` p ) ) C_ ( I ` ( G ` S ) ) <-> ( `' I ` p ) .<_ ( G ` S ) ) )
68 31 61 66 67 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( ( I ` ( `' I ` p ) ) C_ ( I ` ( G ` S ) ) <-> ( `' I ` p ) .<_ ( G ` S ) ) )
69 65 68 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> ( I ` ( `' I ` p ) ) C_ ( I ` ( G ` S ) ) )
70 36 69 eqsstrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> p C_ ( I ` ( G ` S ) ) )
71 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> -. p C_ ( I ` ( G ` S ) ) )
72 70 71 pm2.21fal 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ p e. D /\ ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) ) -> F. )
73 72 rexlimdv3a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( E. p e. D ( p C_ |^|_ x e. S ( I ` x ) /\ -. p C_ ( I ` ( G ` S ) ) ) -> F. ) )
74 30 73 syld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) -> F. ) )
75 15 74 mtoi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> -. ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) )
76 dfpss3 
 |-  ( ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) <-> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ -. |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) )
77 76 notbii 
 |-  ( -. ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) <-> -. ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ -. |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) )
78 iman 
 |-  ( ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) -> |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) <-> -. ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ -. |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) )
79 anclb 
 |-  ( ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) -> |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) <-> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) -> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) ) )
80 77 78 79 3bitr2i 
 |-  ( -. ( I ` ( G ` S ) ) C. |^|_ x e. S ( I ` x ) <-> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) -> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) ) )
81 75 80 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) -> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) ) )
82 14 81 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) )
83 eqss 
 |-  ( ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) <-> ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) /\ |^|_ x e. S ( I ` x ) C_ ( I ` ( G ` S ) ) ) )
84 82 83 sylibr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) = |^|_ x e. S ( I ` x ) )