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 HL S B S M G S = x 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 x S y = x x x S y = x
5 equcom y = x x = y
6 5 anbi1ci x S y = x x = y x S
7 6 exbii x x S y = x x x = y x S
8 eleq1w x = y x S y S
9 8 equsexvw x x = y x S y S
10 4 7 9 3bitri x S y = x y S
11 10 abbii y | x S y = x = y | y S
12 abid2 y | y S = S
13 11 12 eqtr2i S = y | x S y = x
14 13 fveq2i G S = G y | x S y = x
15 14 fveq2i M G S = M G y | x S y = x
16 dfss3 S B x S x B
17 1 2 3 pmapglbx K HL x S x B S M G y | x S y = x = x S M x
18 16 17 syl3an2b K HL S B S M G y | x S y = x = x S M x
19 15 18 syl5eq K HL S B S M G S = x S M x