zrhnm

Description: The norm of the image by ZRHom of an integer in a normed ring. (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 )
	zrhnm.1	\|- L = ( ZRHom ` R )
Assertion	zrhnm	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( L ` M ) ) = ( abs ` M ) )

Proof

Step	Hyp	Ref	Expression
1		nmmulg.x	\|- B = ( Base ` R )
2		nmmulg.n	\|- N = ( norm ` R )
3		nmmulg.z	\|- Z = ( ZMod ` R )
4		zrhnm.1	\|- L = ( ZRHom ` R )
5		simpl3	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> R e. NzRing )
6		nzrring	\|- ( R e. NzRing -> R e. Ring )
7	5 6	syl	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> R e. Ring )
8		simpr	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> M e. ZZ )
9		eqid	\|- ( .g ` R ) = ( .g ` R )
10		eqid	\|- ( 1r ` R ) = ( 1r ` R )
11	4 9 10	zrhmulg	\|- ( ( R e. Ring /\ M e. ZZ ) -> ( L ` M ) = ( M ( .g ` R ) ( 1r ` R ) ) )
12	11	fveq2d	\|- ( ( R e. Ring /\ M e. ZZ ) -> ( N ` ( L ` M ) ) = ( N ` ( M ( .g ` R ) ( 1r ` R ) ) ) )
13	7 8 12	syl2anc	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( L ` M ) ) = ( N ` ( M ( .g ` R ) ( 1r ` R ) ) ) )
14		simpl1	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> Z e. NrmMod )
15	1 10	ringidcl	\|- ( R e. Ring -> ( 1r ` R ) e. B )
16	7 15	syl	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( 1r ` R ) e. B )
17	1 2 3 9	nmmulg	\|- ( ( Z e. NrmMod /\ M e. ZZ /\ ( 1r ` R ) e. B ) -> ( N ` ( M ( .g ` R ) ( 1r ` R ) ) ) = ( ( abs ` M ) x. ( N ` ( 1r ` R ) ) ) )
18	14 8 16 17	syl3anc	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( M ( .g ` R ) ( 1r ` R ) ) ) = ( ( abs ` M ) x. ( N ` ( 1r ` R ) ) ) )
19	3 2	zlmnm	\|- ( R e. NzRing -> N = ( norm ` Z ) )
20	5 19	syl	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> N = ( norm ` Z ) )
21	20	fveq1d	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( 1r ` R ) ) = ( ( norm ` Z ) ` ( 1r ` R ) ) )
22		simpl2	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> Z e. NrmRing )
23		nrgring	\|- ( Z e. NrmRing -> Z e. Ring )
24	22 23	syl	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> Z e. Ring )
25		eqid	\|- ( 0g ` R ) = ( 0g ` R )
26	10 25	nzrnz	\|- ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
27	5 26	syl	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( 1r ` R ) =/= ( 0g ` R ) )
28	3 10	zlm1	\|- ( 1r ` R ) = ( 1r ` Z )
29	3 25	zlm0	\|- ( 0g ` R ) = ( 0g ` Z )
30	28 29	isnzr	\|- ( Z e. NzRing <-> ( Z e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
31	24 27 30	sylanbrc	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> Z e. NzRing )
32		eqid	\|- ( norm ` Z ) = ( norm ` Z )
33	32 28	nm1	\|- ( ( Z e. NrmRing /\ Z e. NzRing ) -> ( ( norm ` Z ) ` ( 1r ` R ) ) = 1 )
34	22 31 33	syl2anc	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( ( norm ` Z ) ` ( 1r ` R ) ) = 1 )
35	21 34	eqtrd	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( 1r ` R ) ) = 1 )
36	35	oveq2d	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( ( abs ` M ) x. ( N ` ( 1r ` R ) ) ) = ( ( abs ` M ) x. 1 ) )
37	13 18 36	3eqtrd	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( L ` M ) ) = ( ( abs ` M ) x. 1 ) )
38	8	zcnd	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> M e. CC )
39		abscl	\|- ( M e. CC -> ( abs ` M ) e. RR )
40	39	recnd	\|- ( M e. CC -> ( abs ` M ) e. CC )
41		mulid1	\|- ( ( abs ` M ) e. CC -> ( ( abs ` M ) x. 1 ) = ( abs ` M ) )
42	38 40 41	3syl	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( ( abs ` M ) x. 1 ) = ( abs ` M ) )
43	37 42	eqtrd	\|- ( ( ( Z e. NrmMod /\ Z e. NrmRing /\ R e. NzRing ) /\ M e. ZZ ) -> ( N ` ( L ` M ) ) = ( abs ` M ) )

Metamath Proof Explorer

Theorem zrhnm

Proof