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