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 ) ) ) ) |