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

Metamath Proof Explorer

Theorem pmapat

Description: The projective map of an atom. (Contributed by NM, 25-Jan-2012)

Ref Expression
Hypotheses pmapat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pmapat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion pmapat ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑃 ) = { 𝑃 } )

Proof

Step Hyp Ref Expression
1 pmapat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pmapat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
3 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 3 1 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
5 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6 3 5 1 2 pmapval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝑃 ) = { 𝑞 ∈ 𝐴 ∣ 𝑞 ( le ‘ 𝐾 ) 𝑃 } )
7 4 6 sylan2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑃 ) = { 𝑞 ∈ 𝐴 ∣ 𝑞 ( le ‘ 𝐾 ) 𝑃 } )
8 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
9 8 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
10 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
11 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
12 5 1 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑞 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑞 = 𝑃 ) )
13 9 10 11 12 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑞 = 𝑃 ) )
14 13 rabbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → { 𝑞 ∈ 𝐴 ∣ 𝑞 ( le ‘ 𝐾 ) 𝑃 } = { 𝑞 ∈ 𝐴 ∣ 𝑞 = 𝑃 } )
15 rabsn ⊢ ( 𝑃 ∈ 𝐴 → { 𝑞 ∈ 𝐴 ∣ 𝑞 = 𝑃 } = { 𝑃 } )
16 15 adantl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → { 𝑞 ∈ 𝐴 ∣ 𝑞 = 𝑃 } = { 𝑃 } )
17 7 14 16 3eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑃 ) = { 𝑃 } )