Metamath Proof Explorer

Theorem clmadd

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

Ref Expression
Hypothesis clm0.f 
|- F = ( Scalar ` W )
Assertion clmadd 
|- ( W e. CMod -> + = ( +g ` 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 cnfldadd 
 |-  + = ( +g ` CCfld )
5 3 4 ressplusg 
 |-  ( ( Base ` F ) e. _V -> + = ( +g ` ( CCfld |`s ( Base ` F ) ) ) )
6 2 5 ax-mp 
 |-  + = ( +g ` ( 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 -> ( +g ` F ) = ( +g ` ( CCfld |`s ( Base ` F ) ) ) )
10 6 9 eqtr4id 
 |-  ( W e. CMod -> + = ( +g ` F ) )