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