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 ∧ 𝑃 ⊆ 𝐴 ) → ( ( 𝑈 ‘ 𝑃 ) = ∅ ↔ 𝑃 = ∅ ) )