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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapglb2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	pmapglb2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmapglb2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	pmapglb2xN	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmapglb2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapglb2.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
3		pmapglb2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		pmapglb2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
5		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
6		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
7	2 6	glb0N	⊢ ( 𝐾 ∈ OP → ( 𝐺 ‘ ∅ ) = ( 1. ‘ 𝐾 ) )
8	7	fveq2d	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = ( 𝑀 ‘ ( 1. ‘ 𝐾 ) ) )
9	6 3 4	pmap1N	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 1. ‘ 𝐾 ) ) = 𝐴 )
10	8 9	eqtrd	⊢ ( 𝐾 ∈ OP → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 )
11	5 10	syl	⊢ ( 𝐾 ∈ HL → ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 )
12		rexeq	⊢ ( 𝐼 = ∅ → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ↔ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆 ) )
13	12	abbidv	⊢ ( 𝐼 = ∅ → { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } = { 𝑦 ∣ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆 } )
14		rex0	⊢ ¬ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆
15	14	abf	⊢ { 𝑦 ∣ ∃ 𝑖 ∈ ∅ 𝑦 = 𝑆 } = ∅
16	13 15	eqtrdi	⊢ ( 𝐼 = ∅ → { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } = ∅ )
17	16	fveq2d	⊢ ( 𝐼 = ∅ → ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) = ( 𝐺 ‘ ∅ ) )
18	17	fveq2d	⊢ ( 𝐼 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) )
19		riin0	⊢ ( 𝐼 = ∅ → ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) = 𝐴 )
20	18 19	eqeq12d	⊢ ( 𝐼 = ∅ → ( ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ↔ ( 𝑀 ‘ ( 𝐺 ‘ ∅ ) ) = 𝐴 ) )
21	11 20	syl5ibrcom	⊢ ( 𝐾 ∈ HL → ( 𝐼 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ) )
22	21	adantr	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐼 = ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ) )
23	1 2 4	pmapglbx	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )
24		nfv	⊢ Ⅎ 𝑖 𝐾 ∈ HL
25		nfra1	⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵
26	24 25	nfan	⊢ Ⅎ 𝑖 ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 )
27		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
28		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → 𝐾 ∈ HL )
29		rspa	⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
30	29	adantll	⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
31	1 3 4	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
32	28 30 31	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
33	27 32	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) )
34	33	ex	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑖 ∈ 𝐼 → ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) ) )
35	26 34	eximd	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ∃ 𝑖 𝑖 ∈ 𝐼 → ∃ 𝑖 ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) ) )
36		n0	⊢ ( 𝐼 ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ 𝐼 )
37		df-rex	⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ↔ ∃ 𝑖 ( 𝑖 ∈ 𝐼 ∧ ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) )
38	35 36 37	3imtr4g	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐼 ≠ ∅ → ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ) )
39	38	3impia	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
40		iinss	⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 → ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
41	39 40	syl	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 )
42		sseqin2	⊢ ( ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )
43	41 42	sylib	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) = ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) )
44	23 43	eqtr4d	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) )
45	44	3expia	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐼 ≠ ∅ → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) ) )
46	22 45	pm2.61dne	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 } ) ) = ( 𝐴 ∩ ∩ 𝑖 ∈ 𝐼 ( 𝑀 ‘ 𝑆 ) ) )