Metamath Proof Explorer

Theorem pmapat

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

Ref Expression
Hypotheses pmapat.a ⊢ A = Atoms ⁡ K
pmapat.m ⊢ M = pmap ⁡ K
Assertion pmapat ⊢ K ∈ HL ∧ P ∈ A → M ⁡ P = P

Proof

Step Hyp Ref Expression
1 pmapat.a ⊢ A = Atoms ⁡ K
2 pmapat.m ⊢ M = pmap ⁡ K
3 eqid ⊢ Base K = Base K
4 3 1 atbase ⊢ P ∈ A → P ∈ Base K
5 eqid ⊢ ≤ K = ≤ K
6 3 5 1 2 pmapval ⊢ K ∈ HL ∧ P ∈ Base K → M ⁡ P = q ∈ A | q ≤ K P
7 4 6 sylan2 ⊢ K ∈ HL ∧ P ∈ A → M ⁡ P = q ∈ A | q ≤ K P
8 hlatl ⊢ K ∈ HL → K ∈ AtLat
9 8 ad2antrr ⊢ K ∈ HL ∧ P ∈ A ∧ q ∈ A → K ∈ AtLat
10 simpr ⊢ K ∈ HL ∧ P ∈ A ∧ q ∈ A → q ∈ A
11 simplr ⊢ K ∈ HL ∧ P ∈ A ∧ q ∈ A → P ∈ A
12 5 1 atcmp ⊢ K ∈ AtLat ∧ q ∈ A ∧ P ∈ A → q ≤ K P ↔ q = P
13 9 10 11 12 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ q ∈ A → q ≤ K P ↔ q = P
14 13 rabbidva ⊢ K ∈ HL ∧ P ∈ A → q ∈ A | q ≤ K P = q ∈ A | q = P
15 rabsn ⊢ P ∈ A → q ∈ A | q = P = P
16 15 adantl ⊢ K ∈ HL ∧ P ∈ A → q ∈ A | q = P = P
17 7 14 16 3eqtrd ⊢ K ∈ HL ∧ P ∈ A → M ⁡ P = P