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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	clmmul	⊢ ( 𝑊 ∈ ℂMod → · = ( .r ‘ 𝐹 ) )

Proof

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