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	syl5eq	|- ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( M ` ( G ` S ) ) = |^|_ x e. S ( M ` x ) )