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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	clmadd	⊢ ( 𝑊 ∈ ℂMod → + = ( +g ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		fvex	⊢ ( Base ‘ 𝐹 ) ∈ V
3		eqid	⊢ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) = ( ℂfld ↾s ( Base ‘ 𝐹 ) )
4		cnfldadd	⊢ + = ( +g ‘ ℂfld )
5	3 4	ressplusg	⊢ ( ( Base ‘ 𝐹 ) ∈ V → + = ( +g ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
6	2 5	ax-mp	⊢ + = ( +g ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
7		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8	1 7	clmsca	⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
9	8	fveq2d	⊢ ( 𝑊 ∈ ℂMod → ( +g ‘ 𝐹 ) = ( +g ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
10	6 9	eqtr4id	⊢ ( 𝑊 ∈ ℂMod → + = ( +g ‘ 𝐹 ) )