This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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