Theorem pclidN

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

	Ref	Expression
Hypotheses	pclid.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
	pclid.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion	pclidN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		pclid.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2		pclid.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
3		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
4	3 1	psubssat	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
5	3 1 2	pclvalN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
6	4 5	syldan	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
7		intmin	⊢ ( 𝑋 ∈ 𝑆 → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } = 𝑋 )
8	7	adantl	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } = 𝑋 )
9	6 8	eqtrd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑋 ) = 𝑋 )