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

Metamath Proof Explorer

Theorem cssi

Description: Property of a closed subspace (of a pre-Hilbert space). (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cssval.o ⊢ ⊥ ˙ = ocv ⁡ W
cssval.c ⊢ C = ClSubSp ⁡ W
Assertion cssi ⊢ S ∈ C → S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S

Proof

Step Hyp Ref Expression
1 cssval.o ⊢ ⊥ ˙ = ocv ⁡ W
2 cssval.c ⊢ C = ClSubSp ⁡ W
3 elfvdm ⊢ S ∈ ClSubSp ⁡ W → W ∈ dom ⁡ ClSubSp
4 3 2 eleq2s ⊢ S ∈ C → W ∈ dom ⁡ ClSubSp
5 1 2 iscss ⊢ W ∈ dom ⁡ ClSubSp → S ∈ C ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
6 4 5 syl ⊢ S ∈ C → S ∈ C ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
7 6 ibi ⊢ S ∈ C → S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S