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 ⊢ B = Base R
nmmulg.n ⊢ N = norm ⁡ R
nmmulg.z ⊢ Z = ℤMod ⁡ R
nmmulg.t ⊢ · ˙ = ⋅ R
Assertion nmmulg ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → N ⁡ M · ˙ X = M ⁢ N ⁡ X

Proof

Step Hyp Ref Expression
1 nmmulg.x ⊢ B = Base R
2 nmmulg.n ⊢ N = norm ⁡ R
3 nmmulg.z ⊢ Z = ℤMod ⁡ R
4 nmmulg.t ⊢ · ˙ = ⋅ R
5 simp2 ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → M ∈ ℤ
6 zringbas ⊢ ℤ = Base ℤ ring
7 nlmlmod ⊢ Z ∈ NrmMod → Z ∈ LMod
8 3 zlmlmod ⊢ R ∈ Abel ↔ Z ∈ LMod
9 7 8 sylibr ⊢ Z ∈ NrmMod → R ∈ Abel
10 9 3ad2ant1 ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → R ∈ Abel
11 3 zlmsca ⊢ R ∈ Abel → ℤ ring = Scalar ⁡ Z
12 10 11 syl ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → ℤ ring = Scalar ⁡ Z
13 12 fveq2d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → Base ℤ ring = Base Scalar ⁡ Z
14 6 13 eqtrid ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → ℤ = Base Scalar ⁡ Z
15 5 14 eleqtrd ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → M ∈ Base Scalar ⁡ Z
16 3 1 zlmbas ⊢ B = Base Z
17 eqid ⊢ norm ⁡ Z = norm ⁡ Z
18 3 4 zlmvsca ⊢ · ˙ = ⋅ Z
19 eqid ⊢ Scalar ⁡ Z = Scalar ⁡ Z
20 eqid ⊢ Base Scalar ⁡ Z = Base Scalar ⁡ Z
21 eqid ⊢ norm ⁡ Scalar ⁡ Z = norm ⁡ Scalar ⁡ Z
22 16 17 18 19 20 21 nmvs ⊢ Z ∈ NrmMod ∧ M ∈ Base Scalar ⁡ Z ∧ X ∈ B → norm ⁡ Z ⁡ M · ˙ X = norm ⁡ Scalar ⁡ Z ⁡ M ⁢ norm ⁡ Z ⁡ X
23 15 22 syld3an2 ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → norm ⁡ Z ⁡ M · ˙ X = norm ⁡ Scalar ⁡ Z ⁡ M ⁢ norm ⁡ Z ⁡ X
24 3 2 zlmnm ⊢ R ∈ Abel → N = norm ⁡ Z
25 10 24 syl ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → N = norm ⁡ Z
26 25 fveq1d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → N ⁡ M · ˙ X = norm ⁡ Z ⁡ M · ˙ X
27 zzsnm ⊢ M ∈ ℤ → M = norm ⁡ ℤ ring ⁡ M
28 27 3ad2ant2 ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → M = norm ⁡ ℤ ring ⁡ M
29 12 fveq2d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → norm ⁡ ℤ ring = norm ⁡ Scalar ⁡ Z
30 29 fveq1d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → norm ⁡ ℤ ring ⁡ M = norm ⁡ Scalar ⁡ Z ⁡ M
31 28 30 eqtrd ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → M = norm ⁡ Scalar ⁡ Z ⁡ M
32 25 fveq1d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → N ⁡ X = norm ⁡ Z ⁡ X
33 31 32 oveq12d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → M ⁢ N ⁡ X = norm ⁡ Scalar ⁡ Z ⁡ M ⁢ norm ⁡ Z ⁡ X
34 23 26 33 3eqtr4d ⊢ Z ∈ NrmMod ∧ M ∈ ℤ ∧ X ∈ B → N ⁡ M · ˙ X = M ⁢ N ⁡ X