Metamath Proof Explorer

Theorem dihglblem5

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

Ref Expression
Hypotheses dihglblem5.b 
|- B = ( Base ` K )
dihglblem5.g 
|- G = ( glb ` K )
dihglblem5.h 
|- H = ( LHyp ` K )
dihglblem5.u 
|- U = ( ( DVecH ` K ) ` W )
dihglblem5.i 
|- I = ( ( DIsoH ` K ) ` W )
dihglblem5.s 
|- S = ( LSubSp ` U )
Assertion dihglblem5 
|- ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> |^|_ x e. T ( I ` x ) e. S )

Proof

Step Hyp Ref Expression
1 dihglblem5.b 
 |-  B = ( Base ` K )
2 dihglblem5.g 
 |-  G = ( glb ` K )
3 dihglblem5.h 
 |-  H = ( LHyp ` K )
4 dihglblem5.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihglblem5.i 
 |-  I = ( ( DIsoH ` K ) ` W )
6 dihglblem5.s 
 |-  S = ( LSubSp ` U )
7 fvex 
 |-  ( I ` x ) e. _V
8 7 dfiin2 
 |-  |^|_ x e. T ( I ` x ) = |^| { y | E. x e. T y = ( I ` x ) }
9 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> ( K e. HL /\ W e. H ) )
10 3 4 9 dvhlmod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> U e. LMod )
11 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) /\ x e. T ) -> ( K e. HL /\ W e. H ) )
12 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) /\ x e. T ) -> T C_ B )
13 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) /\ x e. T ) -> x e. T )
14 12 13 sseldd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) /\ x e. T ) -> x e. B )
15 1 3 5 4 6 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. B ) -> ( I ` x ) e. S )
16 11 14 15 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) /\ x e. T ) -> ( I ` x ) e. S )
17 16 ralrimiva 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> A. x e. T ( I ` x ) e. S )
18 uniiunlem 
 |-  ( A. x e. T ( I ` x ) e. S -> ( A. x e. T ( I ` x ) e. S <-> { y | E. x e. T y = ( I ` x ) } C_ S ) )
19 17 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> ( A. x e. T ( I ` x ) e. S <-> { y | E. x e. T y = ( I ` x ) } C_ S ) )
20 17 19 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> { y | E. x e. T y = ( I ` x ) } C_ S )
21 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> T =/= (/) )
22 n0 
 |-  ( T =/= (/) <-> E. x x e. T )
23 21 22 sylib 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> E. x x e. T )
24 nfre1 
 |-  F/ x E. x e. T y = ( I ` x )
25 24 nfab 
 |-  F/_ x { y | E. x e. T y = ( I ` x ) }
26 nfcv 
 |-  F/_ x (/)
27 25 26 nfne 
 |-  F/ x { y | E. x e. T y = ( I ` x ) } =/= (/)
28 7 elabrex 
 |-  ( x e. T -> ( I ` x ) e. { y | E. x e. T y = ( I ` x ) } )
29 28 ne0d 
 |-  ( x e. T -> { y | E. x e. T y = ( I ` x ) } =/= (/) )
30 27 29 exlimi 
 |-  ( E. x x e. T -> { y | E. x e. T y = ( I ` x ) } =/= (/) )
31 23 30 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> { y | E. x e. T y = ( I ` x ) } =/= (/) )
32 6 lssintcl 
 |-  ( ( U e. LMod /\ { y | E. x e. T y = ( I ` x ) } C_ S /\ { y | E. x e. T y = ( I ` x ) } =/= (/) ) -> |^| { y | E. x e. T y = ( I ` x ) } e. S )
33 10 20 31 32 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> |^| { y | E. x e. T y = ( I ` x ) } e. S )
34 8 33 eqeltrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( T C_ B /\ T =/= (/) ) ) -> |^|_ x e. T ( I ` x ) e. S )