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 = ( .sOLD ` U )
isssp.r
|- R = ( .sOLD ` W )
isssp.n
|- N = ( normCV ` U )
isssp.m
|- M = ( normCV ` W )
isssp.h
|- H = ( SubSp ` U )
Assertion isssp
|- ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) ) )

Proof

Step Hyp Ref Expression
1 isssp.g
 |-  G = ( +v ` U )
2 isssp.f
 |-  F = ( +v ` W )
3 isssp.s
 |-  S = ( .sOLD ` U )
4 isssp.r
 |-  R = ( .sOLD ` W )
5 isssp.n
 |-  N = ( normCV ` U )
6 isssp.m
 |-  M = ( normCV ` W )
7 isssp.h
 |-  H = ( SubSp ` U )
8 1 3 5 7 sspval
 |-  ( U e. NrmCVec -> H = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } )
9 8 eleq2d
 |-  ( U e. NrmCVec -> ( W e. H <-> W e. { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ 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 ) C_ G <-> F C_ G ) )
13 fveq2
 |-  ( w = W -> ( .sOLD ` w ) = ( .sOLD ` W ) )
14 13 4 eqtr4di
 |-  ( w = W -> ( .sOLD ` w ) = R )
15 14 sseq1d
 |-  ( w = W -> ( ( .sOLD ` w ) C_ S <-> R C_ S ) )
16 fveq2
 |-  ( w = W -> ( normCV ` w ) = ( normCV ` W ) )
17 16 6 eqtr4di
 |-  ( w = W -> ( normCV ` w ) = M )
18 17 sseq1d
 |-  ( w = W -> ( ( normCV ` w ) C_ N <-> M C_ N ) )
19 12 15 18 3anbi123d
 |-  ( w = W -> ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) <-> ( F C_ G /\ R C_ S /\ M C_ N ) ) )
20 19 elrab
 |-  ( W e. { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) )
21 9 20 bitrdi
 |-  ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( F C_ G /\ R C_ S /\ M C_ N ) ) ) )