Metamath Proof Explorer


Theorem dvdschrmulg

Description: In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016)

Ref Expression
Hypotheses dvdschrmulg.1
|- C = ( chr ` R )
dvdschrmulg.2
|- B = ( Base ` R )
dvdschrmulg.3
|- .x. = ( .g ` R )
dvdschrmulg.4
|- .0. = ( 0g ` R )
Assertion dvdschrmulg
|- ( ( R e. Ring /\ C || N /\ A e. B ) -> ( N .x. A ) = .0. )

Proof

Step Hyp Ref Expression
1 dvdschrmulg.1
 |-  C = ( chr ` R )
2 dvdschrmulg.2
 |-  B = ( Base ` R )
3 dvdschrmulg.3
 |-  .x. = ( .g ` R )
4 dvdschrmulg.4
 |-  .0. = ( 0g ` R )
5 simp1
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> R e. Ring )
6 dvdszrcl
 |-  ( C || N -> ( C e. ZZ /\ N e. ZZ ) )
7 6 simprd
 |-  ( C || N -> N e. ZZ )
8 7 3ad2ant2
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> N e. ZZ )
9 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
10 2 9 ringidcl
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
11 5 10 syl
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( 1r ` R ) e. B )
12 simp3
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> A e. B )
13 eqid
 |-  ( .r ` R ) = ( .r ` R )
14 2 3 13 mulgass2
 |-  ( ( R e. Ring /\ ( N e. ZZ /\ ( 1r ` R ) e. B /\ A e. B ) ) -> ( ( N .x. ( 1r ` R ) ) ( .r ` R ) A ) = ( N .x. ( ( 1r ` R ) ( .r ` R ) A ) ) )
15 5 8 11 12 14 syl13anc
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( ( N .x. ( 1r ` R ) ) ( .r ` R ) A ) = ( N .x. ( ( 1r ` R ) ( .r ` R ) A ) ) )
16 ringgrp
 |-  ( R e. Ring -> R e. Grp )
17 5 16 syl
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> R e. Grp )
18 eqid
 |-  ( od ` R ) = ( od ` R )
19 18 9 1 chrval
 |-  ( ( od ` R ) ` ( 1r ` R ) ) = C
20 simp2
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> C || N )
21 19 20 eqbrtrid
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( ( od ` R ) ` ( 1r ` R ) ) || N )
22 2 18 3 4 oddvdsi
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. B /\ ( ( od ` R ) ` ( 1r ` R ) ) || N ) -> ( N .x. ( 1r ` R ) ) = .0. )
23 17 11 21 22 syl3anc
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( N .x. ( 1r ` R ) ) = .0. )
24 23 oveq1d
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( ( N .x. ( 1r ` R ) ) ( .r ` R ) A ) = ( .0. ( .r ` R ) A ) )
25 2 13 4 ringlz
 |-  ( ( R e. Ring /\ A e. B ) -> ( .0. ( .r ` R ) A ) = .0. )
26 25 3adant2
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( .0. ( .r ` R ) A ) = .0. )
27 24 26 eqtrd
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( ( N .x. ( 1r ` R ) ) ( .r ` R ) A ) = .0. )
28 2 13 9 ringlidm
 |-  ( ( R e. Ring /\ A e. B ) -> ( ( 1r ` R ) ( .r ` R ) A ) = A )
29 28 3adant2
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( ( 1r ` R ) ( .r ` R ) A ) = A )
30 29 oveq2d
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( N .x. ( ( 1r ` R ) ( .r ` R ) A ) ) = ( N .x. A ) )
31 15 27 30 3eqtr3rd
 |-  ( ( R e. Ring /\ C || N /\ A e. B ) -> ( N .x. A ) = .0. )