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 ⊢ S = PSubSp ⁡ K
pclid.c ⊢ U = PCl ⁡ K
Assertion pclbtwnN ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → X = U ⁡ Y

Proof

Step Hyp Ref Expression
1 pclid.s ⊢ S = PSubSp ⁡ K
2 pclid.c ⊢ U = PCl ⁡ K
3 simprr ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → X ⊆ U ⁡ Y
4 simpll ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → K ∈ V
5 simprl ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → Y ⊆ X
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 6 1 psubssat ⊢ K ∈ V ∧ X ∈ S → X ⊆ Atoms ⁡ K
8 7 adantr ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → X ⊆ Atoms ⁡ K
9 6 2 pclssN ⊢ K ∈ V ∧ Y ⊆ X ∧ X ⊆ Atoms ⁡ K → U ⁡ Y ⊆ U ⁡ X
10 4 5 8 9 syl3anc ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → U ⁡ Y ⊆ U ⁡ X
11 1 2 pclidN ⊢ K ∈ V ∧ X ∈ S → U ⁡ X = X
12 11 adantr ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → U ⁡ X = X
13 10 12 sseqtrd ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → U ⁡ Y ⊆ X
14 3 13 eqssd ⊢ K ∈ V ∧ X ∈ S ∧ Y ⊆ X ∧ X ⊆ U ⁡ Y → X = U ⁡ Y