Metamath Proof Explorer

Theorem clmmul

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

Ref Expression
Hypothesis clm0.f 
|- F = ( Scalar ` W )
Assertion clmmul 
|- ( W e. CMod -> x. = ( .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 cnfldmul 
 |-  x. = ( .r ` CCfld )
5 3 4 ressmulr 
 |-  ( ( Base ` F ) e. _V -> x. = ( .r ` ( CCfld |`s ( Base ` F ) ) ) )
6 2 5 ax-mp 
 |-  x. = ( .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 -> x. = ( .r ` F ) )