| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cphsca.f |
|- F = ( Scalar ` W ) |
| 2 |
|
cphsca.k |
|- K = ( Base ` F ) |
| 3 |
1 2
|
cphsca |
|- ( W e. CPreHil -> F = ( CCfld |`s K ) ) |
| 4 |
3
|
fveq2d |
|- ( W e. CPreHil -> ( *r ` F ) = ( *r ` ( CCfld |`s K ) ) ) |
| 5 |
2
|
fvexi |
|- K e. _V |
| 6 |
|
eqid |
|- ( CCfld |`s K ) = ( CCfld |`s K ) |
| 7 |
|
cnfldcj |
|- * = ( *r ` CCfld ) |
| 8 |
6 7
|
ressstarv |
|- ( K e. _V -> * = ( *r ` ( CCfld |`s K ) ) ) |
| 9 |
5 8
|
ax-mp |
|- * = ( *r ` ( CCfld |`s K ) ) |
| 10 |
4 9
|
eqtr4di |
|- ( W e. CPreHil -> ( *r ` F ) = * ) |
| 11 |
10
|
adantr |
|- ( ( W e. CPreHil /\ A e. K ) -> ( *r ` F ) = * ) |
| 12 |
11
|
fveq1d |
|- ( ( W e. CPreHil /\ A e. K ) -> ( ( *r ` F ) ` A ) = ( * ` A ) ) |
| 13 |
|
cphphl |
|- ( W e. CPreHil -> W e. PreHil ) |
| 14 |
1
|
phlsrng |
|- ( W e. PreHil -> F e. *Ring ) |
| 15 |
13 14
|
syl |
|- ( W e. CPreHil -> F e. *Ring ) |
| 16 |
|
eqid |
|- ( *r ` F ) = ( *r ` F ) |
| 17 |
16 2
|
srngcl |
|- ( ( F e. *Ring /\ A e. K ) -> ( ( *r ` F ) ` A ) e. K ) |
| 18 |
15 17
|
sylan |
|- ( ( W e. CPreHil /\ A e. K ) -> ( ( *r ` F ) ` A ) e. K ) |
| 19 |
12 18
|
eqeltrrd |
|- ( ( W e. CPreHil /\ A e. K ) -> ( * ` A ) e. K ) |