Description: Lemma for ipval3 . (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dipfval.1 | |- X = ( BaseSet ` U ) |
|
| dipfval.2 | |- G = ( +v ` U ) |
||
| dipfval.4 | |- S = ( .sOLD ` U ) |
||
| dipfval.6 | |- N = ( normCV ` U ) |
||
| dipfval.7 | |- P = ( .iOLD ` U ) |
||
| Assertion | ipval2lem4 | |- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( ( N ` ( A G ( C S B ) ) ) ^ 2 ) e. CC ) |
| 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 | 1 2 3 4 5 | ipval2lem2 | |- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( ( N ` ( A G ( C S B ) ) ) ^ 2 ) e. RR ) |
| 7 | 6 | recnd | |- ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ C e. CC ) -> ( ( N ` ( A G ( C S B ) ) ) ^ 2 ) e. CC ) |