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 CMod + = + F

Proof

Step Hyp Ref Expression
1 clm0.f F = Scalar W
2 eqid Base F = Base F
3 1 2 clmsca W CMod F = fld 𝑠 Base F
4 3 fveq2d W CMod + F = + fld 𝑠 Base F
5 fvex Base F V
6 eqid fld 𝑠 Base F = fld 𝑠 Base F
7 cnfldadd + = + fld
8 6 7 ressplusg Base F V + = + fld 𝑠 Base F
9 5 8 ax-mp + = + fld 𝑠 Base F
10 4 9 syl6reqr W CMod + = + F