Metamath Proof Explorer

Theorem dihglb2

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

Ref Expression
Hypotheses dihglb.b 
|- B = ( Base ` K )
dihglb.g 
|- G = ( glb ` K )
dihglb.h 
|- H = ( LHyp ` K )
dihglb.i 
|- I = ( ( DIsoH ` K ) ` W )
dihglb2.u 
|- U = ( ( DVecH ` K ) ` W )
dihglb2.v 
|- V = ( Base ` U )
Assertion dihglb2 
|- ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( I ` ( G ` { x e. B | S C_ ( I ` x ) } ) ) = |^| { y e. ran I | S C_ y } )

Proof

Step Hyp Ref Expression
1 dihglb.b 
 |-  B = ( Base ` K )
2 dihglb.g 
 |-  G = ( glb ` K )
3 dihglb.h 
 |-  H = ( LHyp ` K )
4 dihglb.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 dihglb2.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 dihglb2.v 
 |-  V = ( Base ` U )
7 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( K e. HL /\ W e. H ) )
8 ssrab2 
 |-  { x e. B | S C_ ( I ` x ) } C_ B
9 8 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> { x e. B | S C_ ( I ` x ) } C_ B )
10 hlop 
 |-  ( K e. HL -> K e. OP )
11 10 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> K e. OP )
12 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
13 1 12 op1cl 
 |-  ( K e. OP -> ( 1. ` K ) e. B )
14 11 13 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( 1. ` K ) e. B )
15 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> S C_ V )
16 12 3 4 5 6 dih1 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` ( 1. ` K ) ) = V )
17 16 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( I ` ( 1. ` K ) ) = V )
18 15 17 sseqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> S C_ ( I ` ( 1. ` K ) ) )
19 fveq2 
 |-  ( x = ( 1. ` K ) -> ( I ` x ) = ( I ` ( 1. ` K ) ) )
20 19 sseq2d 
 |-  ( x = ( 1. ` K ) -> ( S C_ ( I ` x ) <-> S C_ ( I ` ( 1. ` K ) ) ) )
21 20 elrab 
 |-  ( ( 1. ` K ) e. { x e. B | S C_ ( I ` x ) } <-> ( ( 1. ` K ) e. B /\ S C_ ( I ` ( 1. ` K ) ) ) )
22 14 18 21 sylanbrc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( 1. ` K ) e. { x e. B | S C_ ( I ` x ) } )
23 22 ne0d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> { x e. B | S C_ ( I ` x ) } =/= (/) )
24 1 2 3 4 dihglb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( { x e. B | S C_ ( I ` x ) } C_ B /\ { x e. B | S C_ ( I ` x ) } =/= (/) ) ) -> ( I ` ( G ` { x e. B | S C_ ( I ` x ) } ) ) = |^|_ z e. { x e. B | S C_ ( I ` x ) } ( I ` z ) )
25 7 9 23 24 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( I ` ( G ` { x e. B | S C_ ( I ` x ) } ) ) = |^|_ z e. { x e. B | S C_ ( I ` x ) } ( I ` z ) )
26 fvex 
 |-  ( I ` z ) e. _V
27 26 dfiin2 
 |-  |^|_ z e. { x e. B | S C_ ( I ` x ) } ( I ` z ) = |^| { y | E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) }
28 1 3 4 dihfn 
 |-  ( ( K e. HL /\ W e. H ) -> I Fn B )
29 28 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) /\ S C_ y ) -> I Fn B )
30 fvelrnb 
 |-  ( I Fn B -> ( y e. ran I <-> E. z e. B ( I ` z ) = y ) )
31 29 30 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) /\ S C_ y ) -> ( y e. ran I <-> E. z e. B ( I ` z ) = y ) )
32 eqcom 
 |-  ( ( I ` z ) = y <-> y = ( I ` z ) )
33 32 rexbii 
 |-  ( E. z e. B ( I ` z ) = y <-> E. z e. B y = ( I ` z ) )
34 df-rex 
 |-  ( E. z e. B y = ( I ` z ) <-> E. z ( z e. B /\ y = ( I ` z ) ) )
35 33 34 bitri 
 |-  ( E. z e. B ( I ` z ) = y <-> E. z ( z e. B /\ y = ( I ` z ) ) )
36 31 35 bitrdi 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) /\ S C_ y ) -> ( y e. ran I <-> E. z ( z e. B /\ y = ( I ` z ) ) ) )
37 36 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( S C_ y -> ( y e. ran I <-> E. z ( z e. B /\ y = ( I ` z ) ) ) ) )
38 37 pm5.32rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( ( y e. ran I /\ S C_ y ) <-> ( E. z ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) ) )
39 df-rex 
 |-  ( E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) <-> E. z ( z e. { x e. B | S C_ ( I ` x ) } /\ y = ( I ` z ) ) )
40 fveq2 
 |-  ( x = z -> ( I ` x ) = ( I ` z ) )
41 40 sseq2d 
 |-  ( x = z -> ( S C_ ( I ` x ) <-> S C_ ( I ` z ) ) )
42 41 elrab 
 |-  ( z e. { x e. B | S C_ ( I ` x ) } <-> ( z e. B /\ S C_ ( I ` z ) ) )
43 42 anbi1i 
 |-  ( ( z e. { x e. B | S C_ ( I ` x ) } /\ y = ( I ` z ) ) <-> ( ( z e. B /\ S C_ ( I ` z ) ) /\ y = ( I ` z ) ) )
44 sseq2 
 |-  ( y = ( I ` z ) -> ( S C_ y <-> S C_ ( I ` z ) ) )
45 44 anbi2d 
 |-  ( y = ( I ` z ) -> ( ( z e. B /\ S C_ y ) <-> ( z e. B /\ S C_ ( I ` z ) ) ) )
46 45 pm5.32ri 
 |-  ( ( ( z e. B /\ S C_ y ) /\ y = ( I ` z ) ) <-> ( ( z e. B /\ S C_ ( I ` z ) ) /\ y = ( I ` z ) ) )
47 an32 
 |-  ( ( ( z e. B /\ S C_ y ) /\ y = ( I ` z ) ) <-> ( ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) )
48 43 46 47 3bitr2i 
 |-  ( ( z e. { x e. B | S C_ ( I ` x ) } /\ y = ( I ` z ) ) <-> ( ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) )
49 48 exbii 
 |-  ( E. z ( z e. { x e. B | S C_ ( I ` x ) } /\ y = ( I ` z ) ) <-> E. z ( ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) )
50 19.41v 
 |-  ( E. z ( ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) <-> ( E. z ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) )
51 39 49 50 3bitrri 
 |-  ( ( E. z ( z e. B /\ y = ( I ` z ) ) /\ S C_ y ) <-> E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) )
52 38 51 bitr2di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) <-> ( y e. ran I /\ S C_ y ) ) )
53 52 abbidv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> { y | E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) } = { y | ( y e. ran I /\ S C_ y ) } )
54 df-rab 
 |-  { y e. ran I | S C_ y } = { y | ( y e. ran I /\ S C_ y ) }
55 53 54 eqtr4di 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> { y | E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) } = { y e. ran I | S C_ y } )
56 55 inteqd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> |^| { y | E. z e. { x e. B | S C_ ( I ` x ) } y = ( I ` z ) } = |^| { y e. ran I | S C_ y } )
57 27 56 syl5eq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> |^|_ z e. { x e. B | S C_ ( I ` x ) } ( I ` z ) = |^| { y e. ran I | S C_ y } )
58 25 57 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S C_ V ) -> ( I ` ( G ` { x e. B | S C_ ( I ` x ) } ) ) = |^| { y e. ran I | S C_ y } )