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 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑃 ) = { 𝑃 } )