Metamath Proof Explorer

Theorem pmapglb2N

Description: The projective map of the GLB of a set of lattice elements S . Variant of Theorem 15.5.2 of MaedaMaeda p. 62. Allows S = (/) . (Contributed by NM, 21-Jan-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pmapglb2.b 
 |-  B = ( Base ` K )
2 pmapglb2.g 
 |-  G = ( glb ` K )
3 pmapglb2.a 
 |-  A = ( Atoms ` K )
4 pmapglb2.m 
 |-  M = ( pmap ` K )
5 hlop 
 |-  ( K e. HL -> K e. OP )
6 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
7 2 6 glb0N 
 |-  ( K e. OP -> ( G ` (/) ) = ( 1. ` K ) )
8 7 fveq2d 
 |-  ( K e. OP -> ( M ` ( G ` (/) ) ) = ( M ` ( 1. ` K ) ) )
9 6 3 4 pmap1N 
 |-  ( K e. OP -> ( M ` ( 1. ` K ) ) = A )
10 8 9 eqtrd 
 |-  ( K e. OP -> ( M ` ( G ` (/) ) ) = A )
11 5 10 syl 
 |-  ( K e. HL -> ( M ` ( G ` (/) ) ) = A )
12 2fveq3 
 |-  ( S = (/) -> ( M ` ( G ` S ) ) = ( M ` ( G ` (/) ) ) )
13 riin0 
 |-  ( S = (/) -> ( A i^i |^|_ x e. S ( M ` x ) ) = A )
14 12 13 eqeq12d 
 |-  ( S = (/) -> ( ( M ` ( G ` S ) ) = ( A i^i |^|_ x e. S ( M ` x ) ) <-> ( M ` ( G ` (/) ) ) = A ) )
15 11 14 syl5ibrcom 
 |-  ( K e. HL -> ( S = (/) -> ( M ` ( G ` S ) ) = ( A i^i |^|_ x e. S ( M ` x ) ) ) )
16 15 adantr 
 |-  ( ( K e. HL /\ S C_ B ) -> ( S = (/) -> ( M ` ( G ` S ) ) = ( A i^i |^|_ x e. S ( M ` x ) ) ) )
17 1 2 4 pmapglb 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( M ` ( G ` S ) ) = |^|_ x e. S ( M ` x ) )
18 simpr 
 |-  ( ( ( K e. HL /\ S C_ B ) /\ x e. S ) -> x e. S )
19 simpll 
 |-  ( ( ( K e. HL /\ S C_ B ) /\ x e. S ) -> K e. HL )
20 ssel2 
 |-  ( ( S C_ B /\ x e. S ) -> x e. B )
21 20 adantll 
 |-  ( ( ( K e. HL /\ S C_ B ) /\ x e. S ) -> x e. B )
22 1 3 4 pmapssat 
 |-  ( ( K e. HL /\ x e. B ) -> ( M ` x ) C_ A )
23 19 21 22 syl2anc 
 |-  ( ( ( K e. HL /\ S C_ B ) /\ x e. S ) -> ( M ` x ) C_ A )
24 18 23 jca 
 |-  ( ( ( K e. HL /\ S C_ B ) /\ x e. S ) -> ( x e. S /\ ( M ` x ) C_ A ) )
25 24 ex 
 |-  ( ( K e. HL /\ S C_ B ) -> ( x e. S -> ( x e. S /\ ( M ` x ) C_ A ) ) )
26 25 eximdv 
 |-  ( ( K e. HL /\ S C_ B ) -> ( E. x x e. S -> E. x ( x e. S /\ ( M ` x ) C_ A ) ) )
27 n0 
 |-  ( S =/= (/) <-> E. x x e. S )
28 df-rex 
 |-  ( E. x e. S ( M ` x ) C_ A <-> E. x ( x e. S /\ ( M ` x ) C_ A ) )
29 26 27 28 3imtr4g 
 |-  ( ( K e. HL /\ S C_ B ) -> ( S =/= (/) -> E. x e. S ( M ` x ) C_ A ) )
30 29 3impia 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> E. x e. S ( M ` x ) C_ A )
31 iinss 
 |-  ( E. x e. S ( M ` x ) C_ A -> |^|_ x e. S ( M ` x ) C_ A )
32 30 31 syl 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> |^|_ x e. S ( M ` x ) C_ A )
33 sseqin2 
 |-  ( |^|_ x e. S ( M ` x ) C_ A <-> ( A i^i |^|_ x e. S ( M ` x ) ) = |^|_ x e. S ( M ` x ) )
34 32 33 sylib 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( A i^i |^|_ x e. S ( M ` x ) ) = |^|_ x e. S ( M ` x ) )
35 17 34 eqtr4d 
 |-  ( ( K e. HL /\ S C_ B /\ S =/= (/) ) -> ( M ` ( G ` S ) ) = ( A i^i |^|_ x e. S ( M ` x ) ) )
36 35 3expia 
 |-  ( ( K e. HL /\ S C_ B ) -> ( S =/= (/) -> ( M ` ( G ` S ) ) = ( A i^i |^|_ x e. S ( M ` x ) ) ) )
37 16 36 pm2.61dne 
 |-  ( ( K e. HL /\ S C_ B ) -> ( M ` ( G ` S ) ) = ( A i^i |^|_ x e. S ( M ` x ) ) )