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

Metamath Proof Explorer

Theorem clmabs

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

Ref Expression
Hypotheses clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion clmabs ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 1 2 clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
4 3 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( norm ‘ 𝐹 ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) ) )
5 4 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( norm ‘ 𝐹 ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) ) )
6 5 fveq1d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = ( ( norm ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) )
7 1 2 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
8 subrgsubg ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
9 7 8 syl ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
10 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
11 cnfldnm ⊢ abs = ( norm ‘ ℂfld )
12 eqid ⊢ ( norm ‘ ( ℂfld ↾s 𝐾 ) ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) )
13 10 11 12 subgnm2 ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ) → ( ( norm ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) = ( abs ‘ 𝐴 ) )
14 9 13 sylan ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( norm ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) = ( abs ‘ 𝐴 ) )
15 6 14 eqtr2d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )