Metamath Proof Explorer

Theorem mulgdi

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

Ref Expression
Hypotheses mulgdi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgdi.m ⊢ · = ( .g ‘ 𝐺 )
mulgdi.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgdi ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 mulgdi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgdi.m ⊢ · = ( .g ‘ 𝐺 )
3 mulgdi.p ⊢ + = ( +g ‘ 𝐺 )
4 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
5 4 ad2antrr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ0 ) → 𝐺 ∈ CMnd )
6 simpr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
7 simplr2 ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
8 simplr3 ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ0 ) → 𝑌 ∈ 𝐵 )
9 1 2 3 mulgnn0di ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
10 5 6 7 8 9 syl13anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
11 4 ad2antrr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → 𝐺 ∈ CMnd )
12 simpr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → - 𝑀 ∈ ℕ0 )
13 simpr2 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
14 13 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
15 simpr3 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
16 15 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → 𝑌 ∈ 𝐵 )
17 1 2 3 mulgnn0di ⊢ ( ( 𝐺 ∈ CMnd ∧ ( - 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( - 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( - 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑌 ) ) )
18 11 12 14 16 17 syl13anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( - 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( - 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑌 ) ) )
19 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
20 19 adantr ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
21 simpr1 ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑀 ∈ ℤ )
22 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
23 20 13 15 22 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
24 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
25 1 2 24 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( - 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) )
26 20 21 23 25 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( - 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) )
27 26 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( - 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) )
28 1 2 24 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑀 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) )
29 20 21 13 28 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( - 𝑀 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) )
30 1 2 24 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑌 ∈ 𝐵 ) → ( - 𝑀 · 𝑌 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) )
31 20 21 15 30 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( - 𝑀 · 𝑌 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) )
32 29 31 oveq12d ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( - 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑌 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
33 32 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( - 𝑀 · 𝑋 ) + ( - 𝑀 · 𝑌 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
34 18 27 33 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
35 simpl ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐺 ∈ Abel )
36 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
37 20 21 13 36 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
38 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 · 𝑌 ) ∈ 𝐵 )
39 20 21 15 38 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · 𝑌 ) ∈ 𝐵 )
40 1 3 24 ablinvadd ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑀 · 𝑌 ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
41 35 37 39 40 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
42 41 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑋 ) ) + ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · 𝑌 ) ) ) )
43 34 42 eqtr4d ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) = ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) )
44 43 fveq2d ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) ) = ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) ) )
45 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
46 20 21 23 45 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
47 46 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) ∈ 𝐵 )
48 1 24 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) ) = ( 𝑀 · ( 𝑋 + 𝑌 ) ) )
49 20 47 48 syl2an2r ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( 𝑀 · ( 𝑋 + 𝑌 ) ) ) ) = ( 𝑀 · ( 𝑋 + 𝑌 ) ) )
50 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑀 · 𝑌 ) ∈ 𝐵 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ∈ 𝐵 )
51 20 37 39 50 syl3anc ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ∈ 𝐵 )
52 51 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ∈ 𝐵 )
53 1 24 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
54 20 52 53 syl2an2r ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( ( invg ‘ 𝐺 ) ‘ ( ( invg ‘ 𝐺 ) ‘ ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
55 44 49 54 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ - 𝑀 ∈ ℕ0 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
56 elznn0 ⊢ ( 𝑀 ∈ ℤ ↔ ( 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) ) )
57 56 simprbi ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) )
58 21 57 syl ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 ∈ ℕ0 ∨ - 𝑀 ∈ ℕ0 ) )
59 10 55 58 mpjaodan ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )