Step |
Hyp |
Ref |
Expression |
1 |
|
dipfval.1 |
|- X = ( BaseSet ` U ) |
2 |
|
dipfval.2 |
|- G = ( +v ` U ) |
3 |
|
dipfval.4 |
|- S = ( .sOLD ` U ) |
4 |
|
dipfval.6 |
|- N = ( normCV ` U ) |
5 |
|
dipfval.7 |
|- P = ( .iOLD ` U ) |
6 |
|
simpl1 |
|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> U e. NrmCVec ) |
7 |
|
simpl2 |
|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> A e. X ) |
8 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ C e. CC /\ B e. X ) -> ( C S B ) e. X ) |
9 |
8
|
3com23 |
|- ( ( U e. NrmCVec /\ B e. X /\ C e. CC ) -> ( C S B ) e. X ) |
10 |
9
|
3expa |
|- ( ( ( U e. NrmCVec /\ B e. X ) /\ C e. CC ) -> ( C S B ) e. X ) |
11 |
10
|
3adantl2 |
|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( C S B ) e. X ) |
12 |
1 2
|
nvgcl |
|- ( ( U e. NrmCVec /\ A e. X /\ ( C S B ) e. X ) -> ( A G ( C S B ) ) e. X ) |
13 |
6 7 11 12
|
syl3anc |
|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( A G ( C S B ) ) e. X ) |
14 |
1 4
|
nvcl |
|- ( ( U e. NrmCVec /\ ( A G ( C S B ) ) e. X ) -> ( N ` ( A G ( C S B ) ) ) e. RR ) |
15 |
6 13 14
|
syl2anc |
|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( N ` ( A G ( C S B ) ) ) e. RR ) |
16 |
15
|
resqcld |
|- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( ( N ` ( A G ( C S B ) ) ) ^ 2 ) e. RR ) |