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 𝑆 = ( PSubSp ‘ 𝐾 )
psubclsub.c 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion psubclsubN ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → 𝑋𝑆 )

Proof

Step Hyp Ref Expression
1 psubclsub.s 𝑆 = ( PSubSp ‘ 𝐾 )
2 psubclsub.c 𝐶 = ( PSubCl ‘ 𝐾 )
3 eqid ( ⊥𝑃𝐾 ) = ( ⊥𝑃𝐾 )
4 3 2 psubcli2N ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → ( ( ⊥𝑃𝐾 ) ‘ ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ) = 𝑋 )
5 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 5 3 2 psubcliN ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃𝐾 ) ‘ ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) )
7 6 simpld ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
8 5 1 3 polsubN ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ∈ 𝑆 )
9 7 8 syldan ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ∈ 𝑆 )
10 5 1 psubssat ( ( 𝐾 ∈ HL ∧ ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ∈ 𝑆 ) → ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
11 9 10 syldan ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
12 5 1 3 polsubN ( ( 𝐾 ∈ HL ∧ ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃𝐾 ) ‘ ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ) ∈ 𝑆 )
13 11 12 syldan ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → ( ( ⊥𝑃𝐾 ) ‘ ( ( ⊥𝑃𝐾 ) ‘ 𝑋 ) ) ∈ 𝑆 )
14 4 13 eqeltrrd ( ( 𝐾 ∈ HL ∧ 𝑋𝐶 ) → 𝑋𝑆 )