Metamath Proof Explorer

Theorem mulgdir

Description: Sum of group multiples, generalized to ZZ . (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgnndir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnndir.t ⊢ · = ( .g ‘ 𝐺 )
mulgnndir.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgdir ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnndir.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnndir.p ⊢ + = ( +g ‘ 𝐺 )
4 1 2 3 mulgdirlem ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
5 4 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
6 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝐺 ∈ Grp )
7 simpr2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℤ )
8 7 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑁 ∈ ℤ )
9 8 znegcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - 𝑁 ∈ ℤ )
10 simpr1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℤ )
11 10 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑀 ∈ ℤ )
12 11 znegcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - 𝑀 ∈ ℤ )
13 simplr3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
14 11 zcnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑀 ∈ ℂ )
15 14 negcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - 𝑀 ∈ ℂ )
16 8 zcnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → 𝑁 ∈ ℂ )
17 16 negcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - 𝑁 ∈ ℂ )
18 14 16 negdid ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - ( 𝑀 + 𝑁 ) = ( - 𝑀 + - 𝑁 ) )
19 15 17 18 comraddd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - ( 𝑀 + 𝑁 ) = ( - 𝑁 + - 𝑀 ) )
20 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → - ( 𝑀 + 𝑁 ) ∈ ℕ0 )
21 19 20 eqeltrrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( - 𝑁 + - 𝑀 ) ∈ ℕ0 )
22 1 2 3 mulgdirlem ⊢ ( ( 𝐺 ∈ Grp ∧ ( - 𝑁 ∈ ℤ ∧ - 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( - 𝑁 + - 𝑀 ) ∈ ℕ0 ) → ( ( - 𝑁 + - 𝑀 ) · 𝑋 ) = ( ( - 𝑁 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) )
23 6 9 12 13 21 22 syl131anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( - 𝑁 + - 𝑀 ) · 𝑋 ) = ( ( - 𝑁 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) )
24 19 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( - ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( - 𝑁 + - 𝑀 ) · 𝑋 ) )
25 10 7 zaddcld ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
26 25 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
27 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
28 1 2 27 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) )
29 6 26 13 28 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( - ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) )
30 24 29 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( - 𝑁 + - 𝑀 ) · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) )
31 1 2 27 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
32 6 8 13 31 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) )
33 1 2 27 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑀 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) )
34 6 11 13 33 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( - 𝑀 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) )
35 32 34 oveq12d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( - 𝑁 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) ) )
36 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
37 6 11 13 36 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
38 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
39 6 8 13 38 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
40 1 3 27 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) ) )
41 6 37 39 40 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑁 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) ) )
42 35 41 eqtr4d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( - 𝑁 · 𝑋 ) + ( - 𝑀 · 𝑋 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) )
43 23 30 42 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) )
44 43 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) ) = ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) ) )
45 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 )
46 6 26 13 45 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 )
47 1 27 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
48 6 46 47 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 + 𝑁 ) · 𝑋 ) ) ) = ( ( 𝑀 + 𝑁 ) · 𝑋 ) )
49 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ∈ 𝐵 )
50 6 37 39 49 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ∈ 𝐵 )
51 1 27 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
52 6 50 51 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
53 44 48 52 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) ∧ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
54 elznn0 ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℤ ↔ ( ( 𝑀 + 𝑁 ) ∈ ℝ ∧ ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) ) )
55 54 simprbi ⊢ ( ( 𝑀 + 𝑁 ) ∈ ℤ → ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) )
56 25 55 syl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) ∈ ℕ0 ∨ - ( 𝑀 + 𝑁 ) ∈ ℕ0 ) )
57 5 53 56 mpjaodan ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )