Metamath Proof Explorer

Theorem mulgnn0di

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

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

Proof

Step Hyp Ref Expression
1 mulgdi.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgdi.m ⊢ · = ( .g ‘ 𝐺 )
3 mulgdi.p ⊢ + = ( +g ‘ 𝐺 )
4 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
5 4 ad2antrr ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → 𝐺 ∈ Mnd )
6 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
7 6 3expb ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
8 5 7 sylan ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
9 1 3 cmncom ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
10 9 3expb ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
11 10 ad4ant14 ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
12 1 3 mndass ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
13 5 12 sylan ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
14 simpr ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
15 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
16 14 15 eleqtrdi ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
17 simplr2 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → 𝑋 ∈ 𝐵 )
18 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ℕ )
19 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑘 ) = 𝑋 )
20 17 18 19 syl2an ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑘 ) = 𝑋 )
21 17 adantr ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑋 ∈ 𝐵 )
22 20 21 eqeltrd ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑘 ) ∈ 𝐵 )
23 simplr3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → 𝑌 ∈ 𝐵 )
24 fvconst2g ⊢ ( ( 𝑌 ∈ 𝐵 ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { 𝑌 } ) ‘ 𝑘 ) = 𝑌 )
25 23 18 24 syl2an ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ℕ × { 𝑌 } ) ‘ 𝑘 ) = 𝑌 )
26 23 adantr ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → 𝑌 ∈ 𝐵 )
27 25 26 eqeltrd ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ℕ × { 𝑌 } ) ‘ 𝑘 ) ∈ 𝐵 )
28 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
29 5 17 23 28 syl3anc ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
30 fvconst2g ⊢ ( ( ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ 𝑘 ∈ ℕ ) → ( ( ℕ × { ( 𝑋 + 𝑌 ) } ) ‘ 𝑘 ) = ( 𝑋 + 𝑌 ) )
31 29 18 30 syl2an ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ℕ × { ( 𝑋 + 𝑌 ) } ) ‘ 𝑘 ) = ( 𝑋 + 𝑌 ) )
32 20 25 oveq12d ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ( ℕ × { 𝑋 } ) ‘ 𝑘 ) + ( ( ℕ × { 𝑌 } ) ‘ 𝑘 ) ) = ( 𝑋 + 𝑌 ) )
33 31 32 eqtr4d ⊢ ( ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( ℕ × { ( 𝑋 + 𝑌 ) } ) ‘ 𝑘 ) = ( ( ( ℕ × { 𝑋 } ) ‘ 𝑘 ) + ( ( ℕ × { 𝑌 } ) ‘ 𝑘 ) ) )
34 8 11 13 16 22 27 33 seqcaopr ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { ( 𝑋 + 𝑌 ) } ) ) ‘ 𝑀 ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) + ( seq 1 ( + , ( ℕ × { 𝑌 } ) ) ‘ 𝑀 ) ) )
35 eqid ⊢ seq 1 ( + , ( ℕ × { ( 𝑋 + 𝑌 ) } ) ) = seq 1 ( + , ( ℕ × { ( 𝑋 + 𝑌 ) } ) )
36 1 3 2 35 mulgnn ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( seq 1 ( + , ( ℕ × { ( 𝑋 + 𝑌 ) } ) ) ‘ 𝑀 ) )
37 14 29 36 syl2anc ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( seq 1 ( + , ( ℕ × { ( 𝑋 + 𝑌 ) } ) ) ‘ 𝑀 ) )
38 eqid ⊢ seq 1 ( + , ( ℕ × { 𝑋 } ) ) = seq 1 ( + , ( ℕ × { 𝑋 } ) )
39 1 3 2 38 mulgnn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) )
40 14 17 39 syl2anc ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) )
41 eqid ⊢ seq 1 ( + , ( ℕ × { 𝑌 } ) ) = seq 1 ( + , ( ℕ × { 𝑌 } ) )
42 1 3 2 41 mulgnn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑌 ∈ 𝐵 ) → ( 𝑀 · 𝑌 ) = ( seq 1 ( + , ( ℕ × { 𝑌 } ) ) ‘ 𝑀 ) )
43 14 23 42 syl2anc ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · 𝑌 ) = ( seq 1 ( + , ( ℕ × { 𝑌 } ) ) ‘ 𝑀 ) )
44 40 43 oveq12d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) + ( seq 1 ( + , ( ℕ × { 𝑌 } ) ) ‘ 𝑀 ) ) )
45 34 37 44 3eqtr4d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
46 4 ad2antrr ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝐺 ∈ Mnd )
47 simplr2 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑋 ∈ 𝐵 )
48 simplr3 ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑌 ∈ 𝐵 )
49 46 47 48 28 syl3anc ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
50 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
51 1 50 2 mulg0 ⊢ ( ( 𝑋 + 𝑌 ) ∈ 𝐵 → ( 0 · ( 𝑋 + 𝑌 ) ) = ( 0g ‘ 𝐺 ) )
52 49 51 syl ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 0 · ( 𝑋 + 𝑌 ) ) = ( 0g ‘ 𝐺 ) )
53 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
54 53 50 mndidcl ⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
55 53 3 50 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
56 4 54 55 syl2anc2 ⊢ ( 𝐺 ∈ CMnd → ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
57 56 ad2antrr ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
58 52 57 eqtr4d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 0 · ( 𝑋 + 𝑌 ) ) = ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) )
59 simpr ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → 𝑀 = 0 )
60 59 oveq1d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( 0 · ( 𝑋 + 𝑌 ) ) )
61 59 oveq1d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑋 ) = ( 0 · 𝑋 ) )
62 1 50 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
63 47 62 syl ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
64 61 63 eqtrd ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
65 59 oveq1d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑌 ) = ( 0 · 𝑌 ) )
66 1 50 2 mulg0 ⊢ ( 𝑌 ∈ 𝐵 → ( 0 · 𝑌 ) = ( 0g ‘ 𝐺 ) )
67 48 66 syl ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 0 · 𝑌 ) = ( 0g ‘ 𝐺 ) )
68 65 67 eqtrd ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · 𝑌 ) = ( 0g ‘ 𝐺 ) )
69 64 68 oveq12d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) = ( ( 0g ‘ 𝐺 ) + ( 0g ‘ 𝐺 ) ) )
70 58 60 69 3eqtr4d ⊢ ( ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) ∧ 𝑀 = 0 ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )
71 simpr1 ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑀 ∈ ℕ0 )
72 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
73 71 72 sylib ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
74 45 70 73 mpjaodan ⊢ ( ( 𝐺 ∈ CMnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑀 · ( 𝑋 + 𝑌 ) ) = ( ( 𝑀 · 𝑋 ) + ( 𝑀 · 𝑌 ) ) )