This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ) → ( 𝑀 ‘ ( 𝐺 ‘ 𝑆 ) ) = ∩ 𝑥 ∈ 𝑆 ( 𝑀 ‘ 𝑥 ) )