Metamath Proof Explorer

Theorem nmmulg

Description: The norm of a group product, provided the ZZ -module is normed. (Contributed by Thierry Arnoux, 8-Nov-2017)

Ref Expression
Hypotheses nmmulg.x ⊢ 𝐵 = ( Base ‘ 𝑅 )
nmmulg.n ⊢ 𝑁 = ( norm ‘ 𝑅 )
nmmulg.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
nmmulg.t ⊢ · = ( .g ‘ 𝑅 )
Assertion nmmulg ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑀 · 𝑋 ) ) = ( ( abs ‘ 𝑀 ) · ( 𝑁 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 nmmulg.x ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 nmmulg.n ⊢ 𝑁 = ( norm ‘ 𝑅 )
3 nmmulg.z ⊢ 𝑍 = ( ℤMod ‘ 𝑅 )
4 nmmulg.t ⊢ · = ( .g ‘ 𝑅 )
5 simp2 ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑀 ∈ ℤ )
6 zringbas ⊢ ℤ = ( Base ‘ ℤring )
7 nlmlmod ⊢ ( 𝑍 ∈ NrmMod → 𝑍 ∈ LMod )
8 3 zlmlmod ⊢ ( 𝑅 ∈ Abel ↔ 𝑍 ∈ LMod )
9 7 8 sylibr ⊢ ( 𝑍 ∈ NrmMod → 𝑅 ∈ Abel )
10 9 3ad2ant1 ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Abel )
11 3 zlmsca ⊢ ( 𝑅 ∈ Abel → ℤring = ( Scalar ‘ 𝑍 ) )
12 10 11 syl ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ℤring = ( Scalar ‘ 𝑍 ) )
13 12 fveq2d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( Base ‘ ℤring ) = ( Base ‘ ( Scalar ‘ 𝑍 ) ) )
14 6 13 syl5eq ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ℤ = ( Base ‘ ( Scalar ‘ 𝑍 ) ) )
15 5 14 eleqtrd ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑍 ) ) )
16 3 1 zlmbas ⊢ 𝐵 = ( Base ‘ 𝑍 )
17 eqid ⊢ ( norm ‘ 𝑍 ) = ( norm ‘ 𝑍 )
18 3 4 zlmvsca ⊢ · = ( ·𝑠 ‘ 𝑍 )
19 eqid ⊢ ( Scalar ‘ 𝑍 ) = ( Scalar ‘ 𝑍 )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑍 ) ) = ( Base ‘ ( Scalar ‘ 𝑍 ) )
21 eqid ⊢ ( norm ‘ ( Scalar ‘ 𝑍 ) ) = ( norm ‘ ( Scalar ‘ 𝑍 ) )
22 16 17 18 19 20 21 nmvs ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ( Base ‘ ( Scalar ‘ 𝑍 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( ( norm ‘ 𝑍 ) ‘ ( 𝑀 · 𝑋 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑍 ) ) ‘ 𝑀 ) · ( ( norm ‘ 𝑍 ) ‘ 𝑋 ) ) )
23 15 22 syld3an2 ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( norm ‘ 𝑍 ) ‘ ( 𝑀 · 𝑋 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑍 ) ) ‘ 𝑀 ) · ( ( norm ‘ 𝑍 ) ‘ 𝑋 ) ) )
24 3 2 zlmnm ⊢ ( 𝑅 ∈ Abel → 𝑁 = ( norm ‘ 𝑍 ) )
25 10 24 syl ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 = ( norm ‘ 𝑍 ) )
26 25 fveq1d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑀 · 𝑋 ) ) = ( ( norm ‘ 𝑍 ) ‘ ( 𝑀 · 𝑋 ) ) )
27 zzsnm ⊢ ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) = ( ( norm ‘ ℤring ) ‘ 𝑀 ) )
28 27 3ad2ant2 ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( abs ‘ 𝑀 ) = ( ( norm ‘ ℤring ) ‘ 𝑀 ) )
29 12 fveq2d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( norm ‘ ℤring ) = ( norm ‘ ( Scalar ‘ 𝑍 ) ) )
30 29 fveq1d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( norm ‘ ℤring ) ‘ 𝑀 ) = ( ( norm ‘ ( Scalar ‘ 𝑍 ) ) ‘ 𝑀 ) )
31 28 30 eqtrd ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( abs ‘ 𝑀 ) = ( ( norm ‘ ( Scalar ‘ 𝑍 ) ) ‘ 𝑀 ) )
32 25 fveq1d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) = ( ( norm ‘ 𝑍 ) ‘ 𝑋 ) )
33 31 32 oveq12d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( abs ‘ 𝑀 ) · ( 𝑁 ‘ 𝑋 ) ) = ( ( ( norm ‘ ( Scalar ‘ 𝑍 ) ) ‘ 𝑀 ) · ( ( norm ‘ 𝑍 ) ‘ 𝑋 ) ) )
34 23 26 33 3eqtr4d ⊢ ( ( 𝑍 ∈ NrmMod ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑀 · 𝑋 ) ) = ( ( abs ‘ 𝑀 ) · ( 𝑁 ‘ 𝑋 ) ) )