Metamath Proof Explorer


Theorem isssp

Description: The predicate "is a subspace." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isssp.g G = + v U
isssp.f F = + v W
isssp.s S = 𝑠OLD U
isssp.r R = 𝑠OLD W
isssp.n N = norm CV U
isssp.m M = norm CV W
isssp.h H = SubSp U
Assertion isssp U NrmCVec W H W NrmCVec F G R S M N

Proof

Step Hyp Ref Expression
1 isssp.g G = + v U
2 isssp.f F = + v W
3 isssp.s S = 𝑠OLD U
4 isssp.r R = 𝑠OLD W
5 isssp.n N = norm CV U
6 isssp.m M = norm CV W
7 isssp.h H = SubSp U
8 1 3 5 7 sspval U NrmCVec H = w NrmCVec | + v w G 𝑠OLD w S norm CV w N
9 8 eleq2d U NrmCVec W H W w NrmCVec | + v w G 𝑠OLD w S norm CV w N
10 fveq2 w = W + v w = + v W
11 10 2 eqtr4di w = W + v w = F
12 11 sseq1d w = W + v w G F G
13 fveq2 w = W 𝑠OLD w = 𝑠OLD W
14 13 4 eqtr4di w = W 𝑠OLD w = R
15 14 sseq1d w = W 𝑠OLD w S R S
16 fveq2 w = W norm CV w = norm CV W
17 16 6 eqtr4di w = W norm CV w = M
18 17 sseq1d w = W norm CV w N M N
19 12 15 18 3anbi123d w = W + v w G 𝑠OLD w S norm CV w N F G R S M N
20 19 elrab W w NrmCVec | + v w G 𝑠OLD w S norm CV w N W NrmCVec F G R S M N
21 9 20 bitrdi U NrmCVec W H W NrmCVec F G R S M N