Step | Hyp | Ref
| Expression |
1 | | cmnmnd 19402 |
. . . . . 6
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
2 | 1 | ad2antrr 723 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝐺 ∈ Mnd) |
3 | | mulgdi.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
4 | | mulgdi.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
5 | 3, 4 | mndcl 18393 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
6 | 5 | 3expb 1119 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
7 | 2, 6 | sylan 580 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
8 | 3, 4 | cmncom 19403 |
. . . . . 6
⊢ ((𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
9 | 8 | 3expb 1119 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
10 | 9 | ad4ant14 749 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
11 | 3, 4 | mndass 18394 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
12 | 2, 11 | sylan 580 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
13 | | simpr 485 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℕ) |
14 | | nnuz 12621 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
15 | 13, 14 | eleqtrdi 2849 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
(ℤ≥‘1)) |
16 | | simplr2 1215 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑋 ∈ 𝐵) |
17 | | elfznn 13285 |
. . . . . 6
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ) |
18 | | fvconst2g 7077 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑋})‘𝑘) = 𝑋) |
19 | 16, 17, 18 | syl2an 596 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑋})‘𝑘) = 𝑋) |
20 | 16 | adantr 481 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → 𝑋 ∈ 𝐵) |
21 | 19, 20 | eqeltrd 2839 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑋})‘𝑘) ∈ 𝐵) |
22 | | simplr3 1216 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑌 ∈ 𝐵) |
23 | | fvconst2g 7077 |
. . . . . 6
⊢ ((𝑌 ∈ 𝐵 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑌})‘𝑘) = 𝑌) |
24 | 22, 17, 23 | syl2an 596 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑌})‘𝑘) = 𝑌) |
25 | 22 | adantr 481 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → 𝑌 ∈ 𝐵) |
26 | 24, 25 | eqeltrd 2839 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑌})‘𝑘) ∈ 𝐵) |
27 | 3, 4 | mndcl 18393 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
28 | 2, 16, 22, 27 | syl3anc 1370 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑋 + 𝑌) ∈ 𝐵) |
29 | | fvconst2g 7077 |
. . . . . 6
⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{(𝑋 + 𝑌)})‘𝑘) = (𝑋 + 𝑌)) |
30 | 28, 17, 29 | syl2an 596 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {(𝑋 + 𝑌)})‘𝑘) = (𝑋 + 𝑌)) |
31 | 19, 24 | oveq12d 7293 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → (((ℕ × {𝑋})‘𝑘) + ((ℕ × {𝑌})‘𝑘)) = (𝑋 + 𝑌)) |
32 | 30, 31 | eqtr4d 2781 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {(𝑋 + 𝑌)})‘𝑘) = (((ℕ × {𝑋})‘𝑘) + ((ℕ × {𝑌})‘𝑘))) |
33 | 7, 10, 12, 15, 21, 26, 32 | seqcaopr 13760 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (seq1( + , (ℕ
× {(𝑋 + 𝑌)}))‘𝑀) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq1( + , (ℕ × {𝑌}))‘𝑀))) |
34 | | mulgdi.m |
. . . . 5
⊢ · =
(.g‘𝐺) |
35 | | eqid 2738 |
. . . . 5
⊢ seq1(
+ ,
(ℕ × {(𝑋 + 𝑌)})) = seq1( + , (ℕ × {(𝑋 + 𝑌)})) |
36 | 3, 4, 34, 35 | mulgnn 18708 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ (𝑋 + 𝑌) ∈ 𝐵) → (𝑀 · (𝑋 + 𝑌)) = (seq1( + , (ℕ × {(𝑋 + 𝑌)}))‘𝑀)) |
37 | 13, 28, 36 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · (𝑋 + 𝑌)) = (seq1( + , (ℕ × {(𝑋 + 𝑌)}))‘𝑀)) |
38 | | eqid 2738 |
. . . . . 6
⊢ seq1(
+ ,
(ℕ × {𝑋})) =
seq1( + ,
(ℕ × {𝑋})) |
39 | 3, 4, 34, 38 | mulgnn 18708 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
40 | 13, 16, 39 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
41 | | eqid 2738 |
. . . . . 6
⊢ seq1(
+ ,
(ℕ × {𝑌})) =
seq1( + ,
(ℕ × {𝑌})) |
42 | 3, 4, 34, 41 | mulgnn 18708 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑌 ∈ 𝐵) → (𝑀 · 𝑌) = (seq1( + , (ℕ × {𝑌}))‘𝑀)) |
43 | 13, 22, 42 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · 𝑌) = (seq1( + , (ℕ × {𝑌}))‘𝑀)) |
44 | 40, 43 | oveq12d 7293 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 · 𝑋) + (𝑀 · 𝑌)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq1( + , (ℕ × {𝑌}))‘𝑀))) |
45 | 33, 37, 44 | 3eqtr4d 2788 |
. 2
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) |
46 | 1 | ad2antrr 723 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝐺 ∈ Mnd) |
47 | | simplr2 1215 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝑋 ∈ 𝐵) |
48 | | simplr3 1216 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝑌 ∈ 𝐵) |
49 | 46, 47, 48, 27 | syl3anc 1370 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑋 + 𝑌) ∈ 𝐵) |
50 | | eqid 2738 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
51 | 3, 50, 34 | mulg0 18707 |
. . . . 5
⊢ ((𝑋 + 𝑌) ∈ 𝐵 → (0 · (𝑋 + 𝑌)) = (0g‘𝐺)) |
52 | 49, 51 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · (𝑋 + 𝑌)) = (0g‘𝐺)) |
53 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
54 | 53, 50 | mndidcl 18400 |
. . . . . 6
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ (Base‘𝐺)) |
55 | 53, 4, 50 | mndlid 18405 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧
(0g‘𝐺)
∈ (Base‘𝐺))
→ ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺)) |
56 | 1, 54, 55 | syl2anc2 585 |
. . . . 5
⊢ (𝐺 ∈ CMnd →
((0g‘𝐺)
+
(0g‘𝐺)) =
(0g‘𝐺)) |
57 | 56 | ad2antrr 723 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺)) |
58 | 52, 57 | eqtr4d 2781 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · (𝑋 + 𝑌)) = ((0g‘𝐺) + (0g‘𝐺))) |
59 | | simpr 485 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝑀 = 0) |
60 | 59 | oveq1d 7290 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · (𝑋 + 𝑌)) = (0 · (𝑋 + 𝑌))) |
61 | 59 | oveq1d 7290 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0 · 𝑋)) |
62 | 3, 50, 34 | mulg0 18707 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
63 | 47, 62 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
64 | 61, 63 | eqtrd 2778 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0g‘𝐺)) |
65 | 59 | oveq1d 7290 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑌) = (0 · 𝑌)) |
66 | 3, 50, 34 | mulg0 18707 |
. . . . . 6
⊢ (𝑌 ∈ 𝐵 → (0 · 𝑌) = (0g‘𝐺)) |
67 | 48, 66 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑌) = (0g‘𝐺)) |
68 | 65, 67 | eqtrd 2778 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑌) = (0g‘𝐺)) |
69 | 64, 68 | oveq12d 7293 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 · 𝑋) + (𝑀 · 𝑌)) = ((0g‘𝐺) + (0g‘𝐺))) |
70 | 58, 60, 69 | 3eqtr4d 2788 |
. 2
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) |
71 | | simpr1 1193 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑀 ∈
ℕ0) |
72 | | elnn0 12235 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
73 | 71, 72 | sylib 217 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 ∈ ℕ ∨ 𝑀 = 0)) |
74 | 45, 70, 73 | mpjaodan 956 |
1
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) |