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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pcl0b.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion pcl0bN ( ( 𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴 ) → ( ( 𝑈 ‘ 𝑃 ) = ∅ ↔ 𝑃 = ∅ ) )

Proof

Step Hyp Ref Expression
1 pcl0b.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pcl0b.c ⊢ 𝑈 = ( PCl ‘ 𝐾 )
3 1 2 pclssidN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴 ) → 𝑃 ⊆ ( 𝑈 ‘ 𝑃 ) )
4 eqimss ⊢ ( ( 𝑈 ‘ 𝑃 ) = ∅ → ( 𝑈 ‘ 𝑃 ) ⊆ ∅ )
5 3 4 sylan9ss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴 ) ∧ ( 𝑈 ‘ 𝑃 ) = ∅ ) → 𝑃 ⊆ ∅ )
6 ss0 ⊢ ( 𝑃 ⊆ ∅ → 𝑃 = ∅ )
7 5 6 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴 ) ∧ ( 𝑈 ‘ 𝑃 ) = ∅ ) → 𝑃 = ∅ )
8 fveq2 ⊢ ( 𝑃 = ∅ → ( 𝑈 ‘ 𝑃 ) = ( 𝑈 ‘ ∅ ) )
9 2 pcl0N ⊢ ( 𝐾 ∈ HL → ( 𝑈 ‘ ∅ ) = ∅ )
10 8 9 sylan9eqr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 = ∅ ) → ( 𝑈 ‘ 𝑃 ) = ∅ )
11 10 adantlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴 ) ∧ 𝑃 = ∅ ) → ( 𝑈 ‘ 𝑃 ) = ∅ )
12 7 11 impbida ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴 ) → ( ( 𝑈 ‘ 𝑃 ) = ∅ ↔ 𝑃 = ∅ ) )