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 = ( ZMod ` R )
nmmulg.t 
|- .x. = ( .g ` R )
Assertion nmmulg 
|- ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( N ` ( M .x. X ) ) = ( ( abs ` M ) x. ( N ` X ) ) )

Proof

Step Hyp Ref Expression
1 nmmulg.x 
 |-  B = ( Base ` R )
2 nmmulg.n 
 |-  N = ( norm ` R )
3 nmmulg.z 
 |-  Z = ( ZMod ` R )
4 nmmulg.t 
 |-  .x. = ( .g ` R )
5 simp2 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> M e. ZZ )
6 zringbas 
 |-  ZZ = ( Base ` ZZring )
7 nlmlmod 
 |-  ( Z e. NrmMod -> Z e. LMod )
8 3 zlmlmod 
 |-  ( R e. Abel <-> Z e. LMod )
9 7 8 sylibr 
 |-  ( Z e. NrmMod -> R e. Abel )
10 9 3ad2ant1 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> R e. Abel )
11 3 zlmsca 
 |-  ( R e. Abel -> ZZring = ( Scalar ` Z ) )
12 10 11 syl 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ZZring = ( Scalar ` Z ) )
13 12 fveq2d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( Base ` ZZring ) = ( Base ` ( Scalar ` Z ) ) )
14 6 13 syl5eq 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ZZ = ( Base ` ( Scalar ` Z ) ) )
15 5 14 eleqtrd 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> M e. ( Base ` ( Scalar ` Z ) ) )
16 3 1 zlmbas 
 |-  B = ( Base ` Z )
17 eqid 
 |-  ( norm ` Z ) = ( norm ` Z )
18 3 4 zlmvsca 
 |-  .x. = ( .s ` 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 e. NrmMod /\ M e. ( Base ` ( Scalar ` Z ) ) /\ X e. B ) -> ( ( norm ` Z ) ` ( M .x. X ) ) = ( ( ( norm ` ( Scalar ` Z ) ) ` M ) x. ( ( norm ` Z ) ` X ) ) )
23 15 22 syld3an2 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( ( norm ` Z ) ` ( M .x. X ) ) = ( ( ( norm ` ( Scalar ` Z ) ) ` M ) x. ( ( norm ` Z ) ` X ) ) )
24 3 2 zlmnm 
 |-  ( R e. Abel -> N = ( norm ` Z ) )
25 10 24 syl 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> N = ( norm ` Z ) )
26 25 fveq1d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( N ` ( M .x. X ) ) = ( ( norm ` Z ) ` ( M .x. X ) ) )
27 zzsnm 
 |-  ( M e. ZZ -> ( abs ` M ) = ( ( norm ` ZZring ) ` M ) )
28 27 3ad2ant2 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( abs ` M ) = ( ( norm ` ZZring ) ` M ) )
29 12 fveq2d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( norm ` ZZring ) = ( norm ` ( Scalar ` Z ) ) )
30 29 fveq1d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( ( norm ` ZZring ) ` M ) = ( ( norm ` ( Scalar ` Z ) ) ` M ) )
31 28 30 eqtrd 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( abs ` M ) = ( ( norm ` ( Scalar ` Z ) ) ` M ) )
32 25 fveq1d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( N ` X ) = ( ( norm ` Z ) ` X ) )
33 31 32 oveq12d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( ( abs ` M ) x. ( N ` X ) ) = ( ( ( norm ` ( Scalar ` Z ) ) ` M ) x. ( ( norm ` Z ) ` X ) ) )
34 23 26 33 3eqtr4d 
 |-  ( ( Z e. NrmMod /\ M e. ZZ /\ X e. B ) -> ( N ` ( M .x. X ) ) = ( ( abs ` M ) x. ( N ` X ) ) )