pmapglbx

Description: The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb , where we read S as S ( i ) . 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	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 ) )

Proof

Step	Hyp	Ref	Expression
1		pmapglb.b	\|- B = ( Base ` K )
2		pmapglb.g	\|- G = ( glb ` K )
3		pmapglb.m	\|- M = ( pmap ` K )
4		hlclat	\|- ( K e. HL -> K e. CLat )
5	4	ad2antrr	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> K e. CLat )
6		eqid	\|- ( Atoms ` K ) = ( Atoms ` K )
7	1 6	atbase	\|- ( p e. ( Atoms ` K ) -> p e. B )
8	7	adantl	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> p e. B )
9		r19.29	\|- ( ( A. i e. I S e. B /\ E. i e. I y = S ) -> E. i e. I ( S e. B /\ y = S ) )
10		eleq1a	\|- ( S e. B -> ( y = S -> y e. B ) )
11	10	imp	\|- ( ( S e. B /\ y = S ) -> y e. B )
12	11	rexlimivw	\|- ( E. i e. I ( S e. B /\ y = S ) -> y e. B )
13	9 12	syl	\|- ( ( A. i e. I S e. B /\ E. i e. I y = S ) -> y e. B )
14	13	ex	\|- ( A. i e. I S e. B -> ( E. i e. I y = S -> y e. B ) )
15	14	ad2antlr	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> ( E. i e. I y = S -> y e. B ) )
16	15	abssdv	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> { y \| E. i e. I y = S } C_ B )
17		eqid	\|- ( le ` K ) = ( le ` K )
18	1 17 2	clatleglb	\|- ( ( K e. CLat /\ p e. B /\ { y \| E. i e. I y = S } C_ B ) -> ( p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) <-> A. z e. { y \| E. i e. I y = S } p ( le ` K ) z ) )
19	5 8 16 18	syl3anc	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> ( p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) <-> A. z e. { y \| E. i e. I y = S } p ( le ` K ) z ) )
20		vex	\|- z e. _V
21		eqeq1	\|- ( y = z -> ( y = S <-> z = S ) )
22	21	rexbidv	\|- ( y = z -> ( E. i e. I y = S <-> E. i e. I z = S ) )
23	20 22	elab	\|- ( z e. { y \| E. i e. I y = S } <-> E. i e. I z = S )
24	23	imbi1i	\|- ( ( z e. { y \| E. i e. I y = S } -> p ( le ` K ) z ) <-> ( E. i e. I z = S -> p ( le ` K ) z ) )
25		r19.23v	\|- ( A. i e. I ( z = S -> p ( le ` K ) z ) <-> ( E. i e. I z = S -> p ( le ` K ) z ) )
26	24 25	bitr4i	\|- ( ( z e. { y \| E. i e. I y = S } -> p ( le ` K ) z ) <-> A. i e. I ( z = S -> p ( le ` K ) z ) )
27	26	albii	\|- ( A. z ( z e. { y \| E. i e. I y = S } -> p ( le ` K ) z ) <-> A. z A. i e. I ( z = S -> p ( le ` K ) z ) )
28		df-ral	\|- ( A. z e. { y \| E. i e. I y = S } p ( le ` K ) z <-> A. z ( z e. { y \| E. i e. I y = S } -> p ( le ` K ) z ) )
29		ralcom4	\|- ( A. i e. I A. z ( z = S -> p ( le ` K ) z ) <-> A. z A. i e. I ( z = S -> p ( le ` K ) z ) )
30	27 28 29	3bitr4i	\|- ( A. z e. { y \| E. i e. I y = S } p ( le ` K ) z <-> A. i e. I A. z ( z = S -> p ( le ` K ) z ) )
31		nfv	\|- F/ z p ( le ` K ) S
32		breq2	\|- ( z = S -> ( p ( le ` K ) z <-> p ( le ` K ) S ) )
33	31 32	ceqsalg	\|- ( S e. B -> ( A. z ( z = S -> p ( le ` K ) z ) <-> p ( le ` K ) S ) )
34	33	ralimi	\|- ( A. i e. I S e. B -> A. i e. I ( A. z ( z = S -> p ( le ` K ) z ) <-> p ( le ` K ) S ) )
35		ralbi	\|- ( A. i e. I ( A. z ( z = S -> p ( le ` K ) z ) <-> p ( le ` K ) S ) -> ( A. i e. I A. z ( z = S -> p ( le ` K ) z ) <-> A. i e. I p ( le ` K ) S ) )
36	34 35	syl	\|- ( A. i e. I S e. B -> ( A. i e. I A. z ( z = S -> p ( le ` K ) z ) <-> A. i e. I p ( le ` K ) S ) )
37	30 36	syl5bb	\|- ( A. i e. I S e. B -> ( A. z e. { y \| E. i e. I y = S } p ( le ` K ) z <-> A. i e. I p ( le ` K ) S ) )
38	37	ad2antlr	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> ( A. z e. { y \| E. i e. I y = S } p ( le ` K ) z <-> A. i e. I p ( le ` K ) S ) )
39	19 38	bitrd	\|- ( ( ( K e. HL /\ A. i e. I S e. B ) /\ p e. ( Atoms ` K ) ) -> ( p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) <-> A. i e. I p ( le ` K ) S ) )
40	39	rabbidva	\|- ( ( K e. HL /\ A. i e. I S e. B ) -> { p e. ( Atoms ` K ) \| p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) } = { p e. ( Atoms ` K ) \| A. i e. I p ( le ` K ) S } )
41	40	3adant3	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> { p e. ( Atoms ` K ) \| p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) } = { p e. ( Atoms ` K ) \| A. i e. I p ( le ` K ) S } )
42		simp1	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> K e. HL )
43	14	abssdv	\|- ( A. i e. I S e. B -> { y \| E. i e. I y = S } C_ B )
44	1 2	clatglbcl	\|- ( ( K e. CLat /\ { y \| E. i e. I y = S } C_ B ) -> ( G ` { y \| E. i e. I y = S } ) e. B )
45	4 43 44	syl2an	\|- ( ( K e. HL /\ A. i e. I S e. B ) -> ( G ` { y \| E. i e. I y = S } ) e. B )
46	45	3adant3	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> ( G ` { y \| E. i e. I y = S } ) e. B )
47	1 17 6 3	pmapval	\|- ( ( K e. HL /\ ( G ` { y \| E. i e. I y = S } ) e. B ) -> ( M ` ( G ` { y \| E. i e. I y = S } ) ) = { p e. ( Atoms ` K ) \| p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) } )
48	42 46 47	syl2anc	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> ( M ` ( G ` { y \| E. i e. I y = S } ) ) = { p e. ( Atoms ` K ) \| p ( le ` K ) ( G ` { y \| E. i e. I y = S } ) } )
49		iinrab	\|- ( I =/= (/) -> \|^\|_ i e. I { p e. ( Atoms ` K ) \| p ( le ` K ) S } = { p e. ( Atoms ` K ) \| A. i e. I p ( le ` K ) S } )
50	49	3ad2ant3	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> \|^\|_ i e. I { p e. ( Atoms ` K ) \| p ( le ` K ) S } = { p e. ( Atoms ` K ) \| A. i e. I p ( le ` K ) S } )
51	41 48 50	3eqtr4d	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> ( M ` ( G ` { y \| E. i e. I y = S } ) ) = \|^\|_ i e. I { p e. ( Atoms ` K ) \| p ( le ` K ) S } )
52		nfv	\|- F/ i K e. HL
53		nfra1	\|- F/ i A. i e. I S e. B
54		nfv	\|- F/ i I =/= (/)
55	52 53 54	nf3an	\|- F/ i ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) )
56		simpl1	\|- ( ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) /\ i e. I ) -> K e. HL )
57		rspa	\|- ( ( A. i e. I S e. B /\ i e. I ) -> S e. B )
58	57	3ad2antl2	\|- ( ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) /\ i e. I ) -> S e. B )
59	1 17 6 3	pmapval	\|- ( ( K e. HL /\ S e. B ) -> ( M ` S ) = { p e. ( Atoms ` K ) \| p ( le ` K ) S } )
60	56 58 59	syl2anc	\|- ( ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) /\ i e. I ) -> ( M ` S ) = { p e. ( Atoms ` K ) \| p ( le ` K ) S } )
61	55 60	iineq2d	\|- ( ( K e. HL /\ A. i e. I S e. B /\ I =/= (/) ) -> \|^\|_ i e. I ( M ` S ) = \|^\|_ i e. I { p e. ( Atoms ` K ) \| p ( le ` K ) S } )
62	51 61	eqtr4d	\|- ( ( 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 ) )

Metamath Proof Explorer

Theorem pmapglbx

Proof