Metamath Proof Explorer


Theorem psubclsubN

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

Ref Expression
Hypotheses psubclsub.s S = PSubSp K
psubclsub.c C = PSubCl K
Assertion psubclsubN K HL X C X S

Proof

Step Hyp Ref Expression
1 psubclsub.s S = PSubSp K
2 psubclsub.c C = PSubCl K
3 eqid 𝑃 K = 𝑃 K
4 3 2 psubcli2N K HL X C 𝑃 K 𝑃 K X = X
5 eqid Atoms K = Atoms K
6 5 3 2 psubcliN K HL X C X Atoms K 𝑃 K 𝑃 K X = X
7 6 simpld K HL X C X Atoms K
8 5 1 3 polsubN K HL X Atoms K 𝑃 K X S
9 7 8 syldan K HL X C 𝑃 K X S
10 5 1 psubssat K HL 𝑃 K X S 𝑃 K X Atoms K
11 9 10 syldan K HL X C 𝑃 K X Atoms K
12 5 1 3 polsubN K HL 𝑃 K X Atoms K 𝑃 K 𝑃 K X S
13 11 12 syldan K HL X C 𝑃 K 𝑃 K X S
14 4 13 eqeltrrd K HL X C X S