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