This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. )