Theorem css0

Description: The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	css0.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
	css0.z	⊢ 0 = ( 0g ‘ 𝑊 )
Assertion	css0	⊢ ( 𝑊 ∈ PreHil → { 0 } ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		css0.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
2		css0.z	⊢ 0 = ( 0g ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
5	3 4 2	ocv1	⊢ ( 𝑊 ∈ PreHil → ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) = { 0 } )
6		ssid	⊢ ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝑊 )
7	3 1 4	ocvcss	⊢ ( ( 𝑊 ∈ PreHil ∧ ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝑊 ) ) → ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) ∈ 𝐶 )
8	6 7	mpan2	⊢ ( 𝑊 ∈ PreHil → ( ( ocv ‘ 𝑊 ) ‘ ( Base ‘ 𝑊 ) ) ∈ 𝐶 )
9	5 8	eqeltrrd	⊢ ( 𝑊 ∈ PreHil → { 0 } ∈ 𝐶 )