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

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ ( 𝑈 ‘ 𝑌 ) ) ) → 𝑋 = ( 𝑈 ‘ 𝑌 ) )