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

Metamath Proof Explorer

Theorem iscss

Description: The predicate "is a closed subspace" (of a pre-Hilbert space). (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 cssval.o ⊢ ⊥ ˙ = ocv ⁡ W
2 cssval.c ⊢ C = ClSubSp ⁡ W
3 1 2 cssval ⊢ W ∈ X → C = s | s = ⊥ ˙ ⁡ ⊥ ˙ ⁡ s
4 3 eleq2d ⊢ W ∈ X → S ∈ C ↔ S ∈ s | s = ⊥ ˙ ⁡ ⊥ ˙ ⁡ s
5 id ⊢ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
6 fvex ⊢ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∈ V
7 5 6 eqeltrdi ⊢ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → S ∈ V
8 id ⊢ s = S → s = S
9 2fveq3 ⊢ s = S → ⊥ ˙ ⁡ ⊥ ˙ ⁡ s = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
10 8 9 eqeq12d ⊢ s = S → s = ⊥ ˙ ⁡ ⊥ ˙ ⁡ s ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
11 7 10 elab3 ⊢ S ∈ s | s = ⊥ ˙ ⁡ ⊥ ˙ ⁡ s ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
12 4 11 bitrdi ⊢ W ∈ X → S ∈ C ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S