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

Metamath Proof Explorer

Theorem pmapglb

Description: The projective map of the GLB of a set of lattice elements S . Variant of Theorem 15.5.2 of MaedaMaeda p. 62. (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypotheses pmapglb.b 
|- B = ( Base ` K )
pmapglb.g 
|- G = ( glb ` K )
pmapglb.m 
|- M = ( pmap ` K )
Assertion pmapglb 
|- ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( M ` ( G ` S ) ) = |^|_ x e. S ( M ` x ) )

Proof

Step Hyp Ref Expression
1 pmapglb.b 
 |-  B = ( Base ` K )
2 pmapglb.g 
 |-  G = ( glb ` K )
3 pmapglb.m 
 |-  M = ( pmap ` K )
4 df-rex 
 |-  ( E. x e. S y = x <-> E. x ( x e. S /\ y = x ) )
5 equcom 
 |-  ( y = x <-> x = y )
6 5 anbi1ci 
 |-  ( ( x e. S /\ y = x ) <-> ( x = y /\ x e. S ) )
7 6 exbii 
 |-  ( E. x ( x e. S /\ y = x ) <-> E. x ( x = y /\ x e. S ) )
8 eleq1w 
 |-  ( x = y -> ( x e. S <-> y e. S ) )
9 8 equsexvw 
 |-  ( E. x ( x = y /\ x e. S ) <-> y e. S )
10 4 7 9 3bitri 
 |-  ( E. x e. S y = x <-> y e. S )
11 10 abbii 
 |-  { y | E. x e. S y = x } = { y | y e. S }
12 abid2 
 |-  { y | y e. S } = S
13 11 12 eqtr2i 
 |-  S = { y | E. x e. S y = x }
14 13 fveq2i 
 |-  ( G ` S ) = ( G ` { y | E. x e. S y = x } )
15 14 fveq2i 
 |-  ( M ` ( G ` S ) ) = ( M ` ( G ` { y | E. x e. S y = x } ) )
16 dfss3 
 |-  ( S C_ B <-> A. x e. S x e. B )
17 1 2 3 pmapglbx 
 |-  ( ( K e. HL /\ A. x e. S x e. B /\ S =/= (/) ) -> ( M ` ( G ` { y | E. x e. S y = x } ) ) = |^|_ x e. S ( M ` x ) )
18 16 17 syl3an2b 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( M ` ( G ` { y | E. x e. S y = x } ) ) = |^|_ x e. S ( M ` x ) )
19 15 18 eqtrid 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( M ` ( G ` S ) ) = |^|_ x e. S ( M ` x ) )