Theorem pclbtwnN

Description: A projective subspace sandwiched between a set of atoms and the set's projective subspace closure equals the closure. (Contributed by NM, 8-Sep-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pclid.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2		pclid.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
3		simprr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) )
4		simpll	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → 𝐾 ∈ 𝑉 )
5		simprl	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → 𝑌 ⊆ 𝑋 )
6		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7	6 1	psubssat	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
8	7	adantr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
9	6 2	pclssN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑈 ‘ 𝑌 ) ⊆ ( 𝑈 ‘ 𝑋 ) )
10	4 5 8 9	syl3anc	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → ( 𝑈 ‘ 𝑌 ) ⊆ ( 𝑈 ‘ 𝑋 ) )
11	1 2	pclidN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑋 ) = 𝑋 )
12	11	adantr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → ( 𝑈 ‘ 𝑋 ) = 𝑋 )
13	10 12	sseqtrd	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → ( 𝑈 ‘ 𝑌 ) ⊆ 𝑋 )
14	3 13	eqssd	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → 𝑋 = ( 𝑈 ‘ 𝑌 ) )