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

Metamath Proof Explorer

Theorem pcl0bN

Description: The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pcl0b.a ⊢ A = Atoms ⁡ K
pcl0b.c ⊢ U = PCl ⁡ K
Assertion pcl0bN ⊢ K ∈ HL ∧ P ⊆ A → U ⁡ P = ∅ ↔ P = ∅

Proof

Step Hyp Ref Expression
1 pcl0b.a ⊢ A = Atoms ⁡ K
2 pcl0b.c ⊢ U = PCl ⁡ K
3 1 2 pclssidN ⊢ K ∈ HL ∧ P ⊆ A → P ⊆ U ⁡ P
4 eqimss ⊢ U ⁡ P = ∅ → U ⁡ P ⊆ ∅
5 3 4 sylan9ss ⊢ K ∈ HL ∧ P ⊆ A ∧ U ⁡ P = ∅ → P ⊆ ∅
6 ss0 ⊢ P ⊆ ∅ → P = ∅
7 5 6 syl ⊢ K ∈ HL ∧ P ⊆ A ∧ U ⁡ P = ∅ → P = ∅
8 fveq2 ⊢ P = ∅ → U ⁡ P = U ⁡ ∅
9 2 pcl0N ⊢ K ∈ HL → U ⁡ ∅ = ∅
10 8 9 sylan9eqr ⊢ K ∈ HL ∧ P = ∅ → U ⁡ P = ∅
11 10 adantlr ⊢ K ∈ HL ∧ P ⊆ A ∧ P = ∅ → U ⁡ P = ∅
12 7 11 impbida ⊢ K ∈ HL ∧ P ⊆ A → U ⁡ P = ∅ ↔ P = ∅