Step |
Hyp |
Ref |
Expression |
1 |
|
sspval.g |
|- G = ( +v ` U ) |
2 |
|
sspval.s |
|- S = ( .sOLD ` U ) |
3 |
|
sspval.n |
|- N = ( normCV ` U ) |
4 |
|
sspval.h |
|- H = ( SubSp ` U ) |
5 |
|
fveq2 |
|- ( u = U -> ( +v ` u ) = ( +v ` U ) ) |
6 |
5 1
|
eqtr4di |
|- ( u = U -> ( +v ` u ) = G ) |
7 |
6
|
sseq2d |
|- ( u = U -> ( ( +v ` w ) C_ ( +v ` u ) <-> ( +v ` w ) C_ G ) ) |
8 |
|
fveq2 |
|- ( u = U -> ( .sOLD ` u ) = ( .sOLD ` U ) ) |
9 |
8 2
|
eqtr4di |
|- ( u = U -> ( .sOLD ` u ) = S ) |
10 |
9
|
sseq2d |
|- ( u = U -> ( ( .sOLD ` w ) C_ ( .sOLD ` u ) <-> ( .sOLD ` w ) C_ S ) ) |
11 |
|
fveq2 |
|- ( u = U -> ( normCV ` u ) = ( normCV ` U ) ) |
12 |
11 3
|
eqtr4di |
|- ( u = U -> ( normCV ` u ) = N ) |
13 |
12
|
sseq2d |
|- ( u = U -> ( ( normCV ` w ) C_ ( normCV ` u ) <-> ( normCV ` w ) C_ N ) ) |
14 |
7 10 13
|
3anbi123d |
|- ( u = U -> ( ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) <-> ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) ) ) |
15 |
14
|
rabbidv |
|- ( u = U -> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } ) |
16 |
|
df-ssp |
|- SubSp = ( u e. NrmCVec |-> { w e. NrmCVec | ( ( +v ` w ) C_ ( +v ` u ) /\ ( .sOLD ` w ) C_ ( .sOLD ` u ) /\ ( normCV ` w ) C_ ( normCV ` u ) ) } ) |
17 |
1
|
fvexi |
|- G e. _V |
18 |
17
|
pwex |
|- ~P G e. _V |
19 |
2
|
fvexi |
|- S e. _V |
20 |
19
|
pwex |
|- ~P S e. _V |
21 |
18 20
|
xpex |
|- ( ~P G X. ~P S ) e. _V |
22 |
3
|
fvexi |
|- N e. _V |
23 |
22
|
pwex |
|- ~P N e. _V |
24 |
21 23
|
xpex |
|- ( ( ~P G X. ~P S ) X. ~P N ) e. _V |
25 |
|
rabss |
|- ( { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } C_ ( ( ~P G X. ~P S ) X. ~P N ) <-> A. w e. NrmCVec ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) -> w e. ( ( ~P G X. ~P S ) X. ~P N ) ) ) |
26 |
|
fvex |
|- ( +v ` w ) e. _V |
27 |
26
|
elpw |
|- ( ( +v ` w ) e. ~P G <-> ( +v ` w ) C_ G ) |
28 |
|
fvex |
|- ( .sOLD ` w ) e. _V |
29 |
28
|
elpw |
|- ( ( .sOLD ` w ) e. ~P S <-> ( .sOLD ` w ) C_ S ) |
30 |
|
opelxpi |
|- ( ( ( +v ` w ) e. ~P G /\ ( .sOLD ` w ) e. ~P S ) -> <. ( +v ` w ) , ( .sOLD ` w ) >. e. ( ~P G X. ~P S ) ) |
31 |
27 29 30
|
syl2anbr |
|- ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S ) -> <. ( +v ` w ) , ( .sOLD ` w ) >. e. ( ~P G X. ~P S ) ) |
32 |
|
fvex |
|- ( normCV ` w ) e. _V |
33 |
32
|
elpw |
|- ( ( normCV ` w ) e. ~P N <-> ( normCV ` w ) C_ N ) |
34 |
33
|
biimpri |
|- ( ( normCV ` w ) C_ N -> ( normCV ` w ) e. ~P N ) |
35 |
|
opelxpi |
|- ( ( <. ( +v ` w ) , ( .sOLD ` w ) >. e. ( ~P G X. ~P S ) /\ ( normCV ` w ) e. ~P N ) -> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) ) |
36 |
31 34 35
|
syl2an |
|- ( ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S ) /\ ( normCV ` w ) C_ N ) -> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) ) |
37 |
36
|
3impa |
|- ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) -> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) ) |
38 |
|
eqid |
|- ( +v ` w ) = ( +v ` w ) |
39 |
|
eqid |
|- ( .sOLD ` w ) = ( .sOLD ` w ) |
40 |
|
eqid |
|- ( normCV ` w ) = ( normCV ` w ) |
41 |
38 39 40
|
nvop |
|- ( w e. NrmCVec -> w = <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. ) |
42 |
41
|
eleq1d |
|- ( w e. NrmCVec -> ( w e. ( ( ~P G X. ~P S ) X. ~P N ) <-> <. <. ( +v ` w ) , ( .sOLD ` w ) >. , ( normCV ` w ) >. e. ( ( ~P G X. ~P S ) X. ~P N ) ) ) |
43 |
37 42
|
syl5ibr |
|- ( w e. NrmCVec -> ( ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) -> w e. ( ( ~P G X. ~P S ) X. ~P N ) ) ) |
44 |
25 43
|
mprgbir |
|- { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } C_ ( ( ~P G X. ~P S ) X. ~P N ) |
45 |
24 44
|
ssexi |
|- { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } e. _V |
46 |
15 16 45
|
fvmpt |
|- ( U e. NrmCVec -> ( SubSp ` U ) = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } ) |
47 |
4 46
|
syl5eq |
|- ( U e. NrmCVec -> H = { w e. NrmCVec | ( ( +v ` w ) C_ G /\ ( .sOLD ` w ) C_ S /\ ( normCV ` w ) C_ N ) } ) |