This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 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 ‘ 𝐹 ) )