This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝑆 )