Metamath Proof Explorer

Theorem cphcjcl

Description: The scalar field of a subcomplex pre-Hilbert space is closed under conjugation. (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses cphsca.f 
|- F = ( Scalar ` W )
cphsca.k 
|- K = ( Base ` F )
Assertion cphcjcl 
|- ( ( W e. CPreHil /\ A e. K ) -> ( * ` A ) e. K )

Proof

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 )