Metamath Proof Explorer

Theorem mulgmodid

Description: Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 30-Aug-2021)

Ref Expression
Hypotheses mulgmodid.b 
|- B = ( Base ` G )
mulgmodid.o 
|- .0. = ( 0g ` G )
mulgmodid.t 
|- .x. = ( .g ` G )
Assertion mulgmodid 
|- ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N mod M ) .x. X ) = ( N .x. X ) )

Proof

Step Hyp Ref Expression
1 mulgmodid.b 
 |-  B = ( Base ` G )
2 mulgmodid.o 
 |-  .0. = ( 0g ` G )
3 mulgmodid.t 
 |-  .x. = ( .g ` G )
4 zre 
 |-  ( N e. ZZ -> N e. RR )
5 nnrp 
 |-  ( M e. NN -> M e. RR+ )
6 modval 
 |-  ( ( N e. RR /\ M e. RR+ ) -> ( N mod M ) = ( N - ( M x. ( |_ ` ( N / M ) ) ) ) )
7 4 5 6 syl2an 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( N mod M ) = ( N - ( M x. ( |_ ` ( N / M ) ) ) ) )
8 7 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( N mod M ) = ( N - ( M x. ( |_ ` ( N / M ) ) ) ) )
9 8 oveq1d 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N mod M ) .x. X ) = ( ( N - ( M x. ( |_ ` ( N / M ) ) ) ) .x. X ) )
10 zcn 
 |-  ( N e. ZZ -> N e. CC )
11 10 adantr 
 |-  ( ( N e. ZZ /\ M e. NN ) -> N e. CC )
12 nnz 
 |-  ( M e. NN -> M e. ZZ )
13 12 adantl 
 |-  ( ( N e. ZZ /\ M e. NN ) -> M e. ZZ )
14 nnre 
 |-  ( M e. NN -> M e. RR )
15 nnne0 
 |-  ( M e. NN -> M =/= 0 )
16 redivcl 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( N / M ) e. RR )
17 4 14 15 16 syl3an 
 |-  ( ( N e. ZZ /\ M e. NN /\ M e. NN ) -> ( N / M ) e. RR )
18 17 3anidm23 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( N / M ) e. RR )
19 18 flcld 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( |_ ` ( N / M ) ) e. ZZ )
20 13 19 zmulcld 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( M x. ( |_ ` ( N / M ) ) ) e. ZZ )
21 20 zcnd 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( M x. ( |_ ` ( N / M ) ) ) e. CC )
22 11 21 negsubd 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( N + -u ( M x. ( |_ ` ( N / M ) ) ) ) = ( N - ( M x. ( |_ ` ( N / M ) ) ) ) )
23 22 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( N + -u ( M x. ( |_ ` ( N / M ) ) ) ) = ( N - ( M x. ( |_ ` ( N / M ) ) ) ) )
24 23 oveq1d 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N + -u ( M x. ( |_ ` ( N / M ) ) ) ) .x. X ) = ( ( N - ( M x. ( |_ ` ( N / M ) ) ) ) .x. X ) )
25 simp1 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> G e. Grp )
26 simpl 
 |-  ( ( N e. ZZ /\ M e. NN ) -> N e. ZZ )
27 26 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> N e. ZZ )
28 13 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> M e. ZZ )
29 19 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( |_ ` ( N / M ) ) e. ZZ )
30 28 29 zmulcld 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( M x. ( |_ ` ( N / M ) ) ) e. ZZ )
31 30 znegcld 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> -u ( M x. ( |_ ` ( N / M ) ) ) e. ZZ )
32 simpl 
 |-  ( ( X e. B /\ ( M .x. X ) = .0. ) -> X e. B )
33 32 3ad2ant3 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> X e. B )
34 eqid 
 |-  ( +g ` G ) = ( +g ` G )
35 1 3 34 mulgdir 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ -u ( M x. ( |_ ` ( N / M ) ) ) e. ZZ /\ X e. B ) ) -> ( ( N + -u ( M x. ( |_ ` ( N / M ) ) ) ) .x. X ) = ( ( N .x. X ) ( +g ` G ) ( -u ( M x. ( |_ ` ( N / M ) ) ) .x. X ) ) )
36 25 27 31 33 35 syl13anc 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N + -u ( M x. ( |_ ` ( N / M ) ) ) ) .x. X ) = ( ( N .x. X ) ( +g ` G ) ( -u ( M x. ( |_ ` ( N / M ) ) ) .x. X ) ) )
37 9 24 36 3eqtr2d 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N mod M ) .x. X ) = ( ( N .x. X ) ( +g ` G ) ( -u ( M x. ( |_ ` ( N / M ) ) ) .x. X ) ) )
38 nncn 
 |-  ( M e. NN -> M e. CC )
39 38 adantl 
 |-  ( ( N e. ZZ /\ M e. NN ) -> M e. CC )
40 19 zcnd 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( |_ ` ( N / M ) ) e. CC )
41 39 40 mulneg2d 
 |-  ( ( N e. ZZ /\ M e. NN ) -> ( M x. -u ( |_ ` ( N / M ) ) ) = -u ( M x. ( |_ ` ( N / M ) ) ) )
42 41 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( M x. -u ( |_ ` ( N / M ) ) ) = -u ( M x. ( |_ ` ( N / M ) ) ) )
43 42 oveq1d 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( M x. -u ( |_ ` ( N / M ) ) ) .x. X ) = ( -u ( M x. ( |_ ` ( N / M ) ) ) .x. X ) )
44 18 3ad2ant2 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( N / M ) e. RR )
45 44 flcld 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( |_ ` ( N / M ) ) e. ZZ )
46 45 znegcld 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> -u ( |_ ` ( N / M ) ) e. ZZ )
47 1 3 mulgassr 
 |-  ( ( G e. Grp /\ ( -u ( |_ ` ( N / M ) ) e. ZZ /\ M e. ZZ /\ X e. B ) ) -> ( ( M x. -u ( |_ ` ( N / M ) ) ) .x. X ) = ( -u ( |_ ` ( N / M ) ) .x. ( M .x. X ) ) )
48 25 46 28 33 47 syl13anc 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( M x. -u ( |_ ` ( N / M ) ) ) .x. X ) = ( -u ( |_ ` ( N / M ) ) .x. ( M .x. X ) ) )
49 oveq2 
 |-  ( ( M .x. X ) = .0. -> ( -u ( |_ ` ( N / M ) ) .x. ( M .x. X ) ) = ( -u ( |_ ` ( N / M ) ) .x. .0. ) )
50 49 adantl 
 |-  ( ( X e. B /\ ( M .x. X ) = .0. ) -> ( -u ( |_ ` ( N / M ) ) .x. ( M .x. X ) ) = ( -u ( |_ ` ( N / M ) ) .x. .0. ) )
51 50 3ad2ant3 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( -u ( |_ ` ( N / M ) ) .x. ( M .x. X ) ) = ( -u ( |_ ` ( N / M ) ) .x. .0. ) )
52 1 3 2 mulgz 
 |-  ( ( G e. Grp /\ -u ( |_ ` ( N / M ) ) e. ZZ ) -> ( -u ( |_ ` ( N / M ) ) .x. .0. ) = .0. )
53 25 46 52 syl2anc 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( -u ( |_ ` ( N / M ) ) .x. .0. ) = .0. )
54 48 51 53 3eqtrd 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( M x. -u ( |_ ` ( N / M ) ) ) .x. X ) = .0. )
55 43 54 eqtr3d 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( -u ( M x. ( |_ ` ( N / M ) ) ) .x. X ) = .0. )
56 55 oveq2d 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N .x. X ) ( +g ` G ) ( -u ( M x. ( |_ ` ( N / M ) ) ) .x. X ) ) = ( ( N .x. X ) ( +g ` G ) .0. ) )
57 id 
 |-  ( G e. Grp -> G e. Grp )
58 1 3 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
59 57 26 32 58 syl3an 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( N .x. X ) e. B )
60 1 34 2 grprid 
 |-  ( ( G e. Grp /\ ( N .x. X ) e. B ) -> ( ( N .x. X ) ( +g ` G ) .0. ) = ( N .x. X ) )
61 25 59 60 syl2anc 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N .x. X ) ( +g ` G ) .0. ) = ( N .x. X ) )
62 37 56 61 3eqtrd 
 |-  ( ( G e. Grp /\ ( N e. ZZ /\ M e. NN ) /\ ( X e. B /\ ( M .x. X ) = .0. ) ) -> ( ( N mod M ) .x. X ) = ( N .x. X ) )