Theorem pmapglb

Description: The projective map of the GLB of a set of lattice elements S . Variant of Theorem 15.5.2 of MaedaMaeda p. 62. (Contributed by NM, 5-Dec-2011)

	Ref	Expression
Hypotheses	pmapglb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapglb.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	pmapglb.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	pmapglb	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		pmapglb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapglb.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
3		pmapglb.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
4		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑦 = 𝑥 ) )
5		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
6	5	anbi1ci	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝑆 ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑆 ∧ 𝑦 = 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝑆 ) )
8		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆 ) )
9	8	equsexvw	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 ∈ 𝑆 ) ↔ 𝑦 ∈ 𝑆 )
10	4 7 9	3bitri	⊢ ( ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 ↔ 𝑦 ∈ 𝑆 )
11	10	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 } = { 𝑦 ∣ 𝑦 ∈ 𝑆 }
12		abid2	⊢ { 𝑦 ∣ 𝑦 ∈ 𝑆 } = 𝑆
13	11 12	eqtr2i	⊢ 𝑆 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 }
14	13	fveq2i	⊢ ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 } )
15	14	fveq2i	⊢ ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 } ) )
16		dfss3	⊢ ( 𝑆 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝑆 𝑥 ∈ 𝐵 )
17	1 2 3	pmapglbx	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ∈ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 } ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
18	16 17	syl3an2b	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = 𝑥 } ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )
19	15 18	syl5eq	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )