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

Metamath Proof Explorer

Theorem clm1

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

Ref Expression
Hypothesis clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion clm1 ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
3 1 2 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) )
4 eqid ⊢ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) = ( ℂfld ↾s ( Base ‘ 𝐹 ) )
5 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
6 4 5 subrg1 ⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ ℂfld ) → 1 = ( 1r ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
7 3 6 syl ⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
8 1 2 clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s ( Base ‘ 𝐹 ) ) )
9 8 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( 1r ‘ 𝐹 ) = ( 1r ‘ ( ℂfld ↾s ( Base ‘ 𝐹 ) ) ) )
10 7 9 eqtr4d ⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ 𝐹 ) )