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 ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )