Metamath Proof Explorer

Theorem pmapglb2xN

Description: The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N , where we read S as S ( i ) . Extension of Theorem 15.5.2 of MaedaMaeda p. 62 that allows I = (/) . (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 pmapglb2xN 
|- ( ( K e. HL /\ A. i e. I S e. B ) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) )

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 rexeq 
 |-  ( I = (/) -> ( E. i e. I y = S <-> E. i e. (/) y = S ) )
13 12 abbidv 
 |-  ( I = (/) -> { y | E. i e. I y = S } = { y | E. i e. (/) y = S } )
14 rex0 
 |-  -. E. i e. (/) y = S
15 14 abf 
 |-  { y | E. i e. (/) y = S } = (/)
16 13 15 eqtrdi 
 |-  ( I = (/) -> { y | E. i e. I y = S } = (/) )
17 16 fveq2d 
 |-  ( I = (/) -> ( G ` { y | E. i e. I y = S } ) = ( G ` (/) ) )
18 17 fveq2d 
 |-  ( I = (/) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( M ` ( G ` (/) ) ) )
19 riin0 
 |-  ( I = (/) -> ( A i^i |^|_ i e. I ( M ` S ) ) = A )
20 18 19 eqeq12d 
 |-  ( I = (/) -> ( ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) <-> ( M ` ( G ` (/) ) ) = A ) )
21 11 20 syl5ibrcom 
 |-  ( K e. HL -> ( I = (/) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) ) )
22 21 adantr 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( I = (/) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) ) )
23 1 2 4 pmapglbx 
 |-  ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = |^|_ i e. I ( M ` S ) )
24 nfv 
 |-  F/ i K e. HL
25 nfra1 
 |-  F/ i A. i e. I S e. B
26 24 25 nfan 
 |-  F/ i ( K e. HL /\ A. i e. I S e. B )
27 simpr 
 |-  ( ( ( K e. HL /\ A. i e. I S e. B ) /\ i e. I ) -> i e. I )
28 simpll 
 |-  ( ( ( K e. HL /\ A. i e. I S e. B ) /\ i e. I ) -> K e. HL )
29 rspa 
 |-  ( ( A. i e. I S e. B /\ i e. I ) -> S e. B )
30 29 adantll 
 |-  ( ( ( K e. HL /\ A. i e. I S e. B ) /\ i e. I ) -> S e. B )
31 1 3 4 pmapssat 
 |-  ( ( K e. HL /\ S e. B ) -> ( M ` S ) C_ A )
32 28 30 31 syl2anc 
 |-  ( ( ( K e. HL /\ A. i e. I S e. B ) /\ i e. I ) -> ( M ` S ) C_ A )
33 27 32 jca 
 |-  ( ( ( K e. HL /\ A. i e. I S e. B ) /\ i e. I ) -> ( i e. I /\ ( M ` S ) C_ A ) )
34 33 ex 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( i e. I -> ( i e. I /\ ( M ` S ) C_ A ) ) )
35 26 34 eximd 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( E. i i e. I -> E. i ( i e. I /\ ( M ` S ) C_ A ) ) )
36 n0 
 |-  ( I =/= (/) <-> E. i i e. I )
37 df-rex 
 |-  ( E. i e. I ( M ` S ) C_ A <-> E. i ( i e. I /\ ( M ` S ) C_ A ) )
38 35 36 37 3imtr4g 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( I =/= (/) -> E. i e. I ( M ` S ) C_ A ) )
39 38 3impia 
 |-  ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> E. i e. I ( M ` S ) C_ A )
40 iinss 
 |-  ( E. i e. I ( M ` S ) C_ A -> |^|_ i e. I ( M ` S ) C_ A )
41 39 40 syl 
 |-  ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> |^|_ i e. I ( M ` S ) C_ A )
42 sseqin2 
 |-  ( |^|_ i e. I ( M ` S ) C_ A <-> ( A i^i |^|_ i e. I ( M ` S ) ) = |^|_ i e. I ( M ` S ) )
43 41 42 sylib 
 |-  ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> ( A i^i |^|_ i e. I ( M ` S ) ) = |^|_ i e. I ( M ` S ) )
44 23 43 eqtr4d 
 |-  ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) )
45 44 3expia 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( I =/= (/) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) ) )
46 22 45 pm2.61dne 
 |-  ( ( K e. HL /\ A. i e. I S e. B ) -> ( M ` ( G ` { y | E. i e. I y = S } ) ) = ( A i^i |^|_ i e. I ( M ` S ) ) )