Metamath Proof Explorer

Theorem pmapsubclN

Description: A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmapsubcl.b ⊢ B = Base K
pmapsubcl.m ⊢ M = pmap ⁡ K
pmapsubcl.c ⊢ C = PSubCl ⁡ K
Assertion pmapsubclN ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ∈ C

Proof

Step Hyp Ref Expression
1 pmapsubcl.b ⊢ B = Base K
2 pmapsubcl.m ⊢ M = pmap ⁡ K
3 pmapsubcl.c ⊢ C = PSubCl ⁡ K
4 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
5 1 4 2 pmapssat ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ⊆ Atoms ⁡ K
6 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
7 1 2 6 2polpmapN ⊢ K ∈ HL ∧ X ∈ B → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ X = M ⁡ X
8 4 6 3 ispsubclN ⊢ K ∈ HL → M ⁡ X ∈ C ↔ M ⁡ X ⊆ Atoms ⁡ K ∧ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ X = M ⁡ X
9 8 adantr ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ∈ C ↔ M ⁡ X ⊆ Atoms ⁡ K ∧ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ M ⁡ X = M ⁡ X
10 5 7 9 mpbir2and ⊢ K ∈ HL ∧ X ∈ B → M ⁡ X ∈ C