| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cphsca.f |
|- F = ( Scalar ` W ) |
| 2 |
|
cphsca.k |
|- K = ( Base ` F ) |
| 3 |
|
sqrtf |
|- sqrt : CC --> CC |
| 4 |
|
ffn |
|- ( sqrt : CC --> CC -> sqrt Fn CC ) |
| 5 |
3 4
|
ax-mp |
|- sqrt Fn CC |
| 6 |
|
inss2 |
|- ( K i^i ( 0 [,) +oo ) ) C_ ( 0 [,) +oo ) |
| 7 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
| 8 |
|
ax-resscn |
|- RR C_ CC |
| 9 |
7 8
|
sstri |
|- ( 0 [,) +oo ) C_ CC |
| 10 |
6 9
|
sstri |
|- ( K i^i ( 0 [,) +oo ) ) C_ CC |
| 11 |
|
simp1 |
|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> A e. K ) |
| 12 |
|
elrege0 |
|- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) ) |
| 13 |
12
|
biimpri |
|- ( ( A e. RR /\ 0 <_ A ) -> A e. ( 0 [,) +oo ) ) |
| 14 |
13
|
3adant1 |
|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> A e. ( 0 [,) +oo ) ) |
| 15 |
11 14
|
elind |
|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> A e. ( K i^i ( 0 [,) +oo ) ) ) |
| 16 |
|
fnfvima |
|- ( ( sqrt Fn CC /\ ( K i^i ( 0 [,) +oo ) ) C_ CC /\ A e. ( K i^i ( 0 [,) +oo ) ) ) -> ( sqrt ` A ) e. ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) ) |
| 17 |
5 10 15 16
|
mp3an12i |
|- ( ( A e. K /\ A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) ) |
| 18 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 19 |
|
eqid |
|- ( .i ` W ) = ( .i ` W ) |
| 20 |
|
eqid |
|- ( norm ` W ) = ( norm ` W ) |
| 21 |
18 19 20 1 2
|
iscph |
|- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ F = ( CCfld |`s K ) ) /\ ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K /\ ( norm ` W ) = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) ) ) |
| 22 |
21
|
simp2bi |
|- ( W e. CPreHil -> ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) C_ K ) |
| 23 |
22
|
sselda |
|- ( ( W e. CPreHil /\ ( sqrt ` A ) e. ( sqrt " ( K i^i ( 0 [,) +oo ) ) ) ) -> ( sqrt ` A ) e. K ) |
| 24 |
17 23
|
sylan2 |
|- ( ( W e. CPreHil /\ ( A e. K /\ A e. RR /\ 0 <_ A ) ) -> ( sqrt ` A ) e. K ) |