# Metamath Proof Explorer

## Theorem mulgdi

Description: Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgdi.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
mulgdi.m
mulgdi.p
Assertion mulgdi

### Proof

Step Hyp Ref Expression
1 mulgdi.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 mulgdi.m
3 mulgdi.p
4 ablcmn ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{CMnd}$
5 4 ad2antrr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {G}\in \mathrm{CMnd}$
6 simpr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {M}\in {ℕ}_{0}$
7 simplr2 ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {X}\in {B}$
8 simplr3 ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {M}\in {ℕ}_{0}\right)\to {Y}\in {B}$
9 1 2 3 mulgnn0di
10 5 6 7 8 9 syl13anc
11 4 ad2antrr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge -{M}\in {ℕ}_{0}\right)\to {G}\in \mathrm{CMnd}$
12 simpr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge -{M}\in {ℕ}_{0}\right)\to -{M}\in {ℕ}_{0}$
13 simpr2 ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
14 13 adantr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge -{M}\in {ℕ}_{0}\right)\to {X}\in {B}$
15 simpr3 ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
16 15 adantr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge -{M}\in {ℕ}_{0}\right)\to {Y}\in {B}$
17 1 2 3 mulgnn0di
18 11 12 14 16 17 syl13anc
19 ablgrp ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{Grp}$
20 19 adantr ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {G}\in \mathrm{Grp}$
21 simpr1 ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {M}\in ℤ$
22 1 3 grpcl
23 20 13 15 22 syl3anc
24 eqid ${⊢}{inv}_{g}\left({G}\right)={inv}_{g}\left({G}\right)$
25 1 2 24 mulgneg
26 20 21 23 25 syl3anc
28 1 2 24 mulgneg
29 20 21 13 28 syl3anc
30 1 2 24 mulgneg
31 20 21 15 30 syl3anc
32 29 31 oveq12d
34 18 27 33 3eqtr3d
35 simpl ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to {G}\in \mathrm{Abel}$
36 1 2 mulgcl
37 20 21 13 36 syl3anc
38 1 2 mulgcl
39 20 21 15 38 syl3anc
41 35 37 39 40 syl3anc
43 34 42 eqtr4d
44 43 fveq2d
45 1 2 mulgcl
46 20 21 23 45 syl3anc
56 elznn0 ${⊢}{M}\in ℤ↔\left({M}\in ℝ\wedge \left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)\right)$
57 56 simprbi ${⊢}{M}\in ℤ\to \left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)$
58 21 57 syl ${⊢}\left({G}\in \mathrm{Abel}\wedge \left({M}\in ℤ\wedge {X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({M}\in {ℕ}_{0}\vee -{M}\in {ℕ}_{0}\right)$