Metamath Proof Explorer

Theorem clmcj

Description: The conjugation of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypothesis clm0.f 
|- F = ( Scalar ` W )
Assertion clmcj 
|- ( W e. CMod -> * = ( *r ` F ) )

Proof

Step Hyp Ref Expression
1 clm0.f 
 |-  F = ( Scalar ` W )
2 fvex 
 |-  ( Base ` F ) e. _V
3 eqid 
 |-  ( CCfld |`s ( Base ` F ) ) = ( CCfld |`s ( Base ` F ) )
4 cnfldcj 
 |-  * = ( *r ` CCfld )
5 3 4 ressstarv 
 |-  ( ( Base ` F ) e. _V -> * = ( *r ` ( CCfld |`s ( Base ` F ) ) ) )
6 2 5 ax-mp 
 |-  * = ( *r ` ( CCfld |`s ( Base ` F ) ) )
7 eqid 
 |-  ( Base ` F ) = ( Base ` F )
8 1 7 clmsca 
 |-  ( W e. CMod -> F = ( CCfld |`s ( Base ` F ) ) )
9 8 fveq2d 
 |-  ( W e. CMod -> ( *r ` F ) = ( *r ` ( CCfld |`s ( Base ` F ) ) ) )
10 6 9 eqtr4id 
 |-  ( W e. CMod -> * = ( *r ` F ) )