Metamath Proof Explorer


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