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