Metamath Proof Explorer

Theorem pclss2polN

Description: The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclss2pol.a ⊢ A = Atoms ⁡ K
pclss2pol.o ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
pclss2pol.c ⊢ U = PCl ⁡ K
Assertion pclss2polN ⊢ K ∈ HL ∧ X ⊆ A → U ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 pclss2pol.a ⊢ A = Atoms ⁡ K
2 pclss2pol.o ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
3 pclss2pol.c ⊢ U = PCl ⁡ K
4 simpl ⊢ K ∈ HL ∧ X ⊆ A → K ∈ HL
5 1 2 2polssN ⊢ K ∈ HL ∧ X ⊆ A → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
6 1 2 polssatN ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X ⊆ A
7 1 2 polssatN ⊢ K ∈ HL ∧ ⊥ ˙ ⁡ X ⊆ A → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ A
8 6 7 syldan ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ A
9 1 3 pclssN ⊢ K ∈ HL ∧ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ A → U ⁡ X ⊆ U ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
10 4 5 8 9 syl3anc ⊢ K ∈ HL ∧ X ⊆ A → U ⁡ X ⊆ U ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
11 eqid ⊢ PSubSp ⁡ K = PSubSp ⁡ K
12 1 11 2 polsubN ⊢ K ∈ HL ∧ ⊥ ˙ ⁡ X ⊆ A → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ PSubSp ⁡ K
13 6 12 syldan ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ PSubSp ⁡ K
14 11 3 pclidN ⊢ K ∈ HL ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∈ PSubSp ⁡ K → U ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
15 13 14 syldan ⊢ K ∈ HL ∧ X ⊆ A → U ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
16 10 15 sseqtrd ⊢ K ∈ HL ∧ X ⊆ A → U ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X