Theorem mulgnn0dir

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

	Ref	Expression
Hypotheses	mulgnndir.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgnndir.t	⊢ · = ( .g ‘ 𝐺 )
	mulgnndir.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	mulgnn0dir	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulgnndir.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgnndir.t	⊢ · = ( .g ‘ 𝐺 )
3		mulgnndir.p	⊢ + = ( +g ‘ 𝐺 )
4		mndsgrp	⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Smgrp )
5	4	adantr	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐺 ∈ Smgrp )
6	5	ad2antrr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ) → 𝐺 ∈ Smgrp )
7		simplr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℕ )
8		simpr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
9		simpr3	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
10	9	ad2antrr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ 𝐵 )
11	1 2 3	mulgnndir	⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
12	6 7 8 10 11	syl13anc	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
13		simpll	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → 𝐺 ∈ Mnd )
14		simpr1	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℕ0 )
15	14	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → 𝑀 ∈ ℕ0 )
16		simplr3	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → 𝑋 ∈ 𝐵 )
17	1 2 13 15 16	mulgnn0cld	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 𝑀 · 𝑋 ) ∈ 𝐵 )
18		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
19	1 3 18	mndrid	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑀 · 𝑋 ) + ( 0g ‘ 𝐺 ) ) = ( 𝑀 · 𝑋 ) )
20	13 17 19	syl2anc	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( ( 𝑀 · 𝑋 ) + ( 0g ‘ 𝐺 ) ) = ( 𝑀 · 𝑋 ) )
21		simpr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → 𝑁 = 0 )
22	21	oveq1d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
23	1 18 2	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
24	16 23	syl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
25	22 24	eqtrd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
26	25	oveq2d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) = ( ( 𝑀 · 𝑋 ) + ( 0g ‘ 𝐺 ) ) )
27	21	oveq2d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 𝑀 + 𝑁 ) = ( 𝑀 + 0 ) )
28	15	nn0cnd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → 𝑀 ∈ ℂ )
29	28	addridd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 𝑀 + 0 ) = 𝑀 )
30	27 29	eqtrd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( 𝑀 + 𝑁 ) = 𝑀 )
31	30	oveq1d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( 𝑀 · 𝑋 ) )
32	20 26 31	3eqtr4rd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑁 = 0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
33	32	adantlr	⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑁 = 0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
34		simpr2	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℕ0 )
35		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
36	34 35	sylib	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
37	36	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
38	12 33 37	mpjaodan	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
39		simpll	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝐺 ∈ Mnd )
40		simplr2	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑁 ∈ ℕ0 )
41		simplr3	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑋 ∈ 𝐵 )
42	1 2 39 40 41	mulgnn0cld	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
43	1 3 18	mndlid	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
44	39 42 43	syl2anc	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( ( 0g ‘ 𝐺 ) + ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
45		simpr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑀 = 0 )
46	45	oveq1d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑋 ) = ( 0 · 𝑋 ) )
47	41 23	syl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
48	46 47	eqtrd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
49	48	oveq1d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) = ( ( 0g ‘ 𝐺 ) + ( 𝑁 · 𝑋 ) ) )
50	45	oveq1d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 + 𝑁 ) = ( 0 + 𝑁 ) )
51	40	nn0cnd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑁 ∈ ℂ )
52	51	addlidd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 0 + 𝑁 ) = 𝑁 )
53	50 52	eqtrd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 + 𝑁 ) = 𝑁 )
54	53	oveq1d	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( 𝑁 · 𝑋 ) )
55	44 49 54	3eqtr4rd	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )
56		elnn0	⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
57	14 56	sylib	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
58	38 55 57	mpjaodan	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )