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

Metamath Proof Explorer

Theorem css0

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

Ref Expression
Hypotheses css0.c ⊢ C = ClSubSp ⁡ W
css0.z ⊢ 0 ˙ = 0 W
Assertion css0 ⊢ W ∈ PreHil → 0 ˙ ∈ C

Proof

Step Hyp Ref Expression
1 css0.c ⊢ C = ClSubSp ⁡ W
2 css0.z ⊢ 0 ˙ = 0 W
3 eqid ⊢ Base W = Base W
4 eqid ⊢ ocv ⁡ W = ocv ⁡ W
5 3 4 2 ocv1 ⊢ W ∈ PreHil → ocv ⁡ W ⁡ Base W = 0 ˙
6 ssid ⊢ Base W ⊆ Base W
7 3 1 4 ocvcss ⊢ W ∈ PreHil ∧ Base W ⊆ Base W → ocv ⁡ W ⁡ Base W ∈ C
8 6 7 mpan2 ⊢ W ∈ PreHil → ocv ⁡ W ⁡ Base W ∈ C
9 5 8 eqeltrrd ⊢ W ∈ PreHil → 0 ˙ ∈ C