Step | Hyp | Ref
| Expression |
1 | | cmnmnd 19042 |
. . . . . 6
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
2 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝐺 ∈ Mnd) |
3 | | mulgdi.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
4 | | mulgdi.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
5 | 3, 4 | mndcl 18037 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
6 | 5 | 3expb 1121 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
7 | 2, 6 | sylan 583 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
8 | 3, 4 | cmncom 19043 |
. . . . . 6
⊢ ((𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
9 | 8 | 3expb 1121 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
10 | 9 | ad4ant14 752 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
11 | 3, 4 | mndass 18038 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
12 | 2, 11 | sylan 583 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
13 | | simpr 488 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℕ) |
14 | | nnuz 12365 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
15 | 13, 14 | eleqtrdi 2843 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
(ℤ≥‘1)) |
16 | | simplr2 1217 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑋 ∈ 𝐵) |
17 | | elfznn 13029 |
. . . . . 6
⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ) |
18 | | fvconst2g 6976 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑋})‘𝑘) = 𝑋) |
19 | 16, 17, 18 | syl2an 599 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑋})‘𝑘) = 𝑋) |
20 | 16 | adantr 484 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → 𝑋 ∈ 𝐵) |
21 | 19, 20 | eqeltrd 2833 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑋})‘𝑘) ∈ 𝐵) |
22 | | simplr3 1218 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝑌 ∈ 𝐵) |
23 | | fvconst2g 6976 |
. . . . . 6
⊢ ((𝑌 ∈ 𝐵 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{𝑌})‘𝑘) = 𝑌) |
24 | 22, 17, 23 | syl2an 599 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑌})‘𝑘) = 𝑌) |
25 | 22 | adantr 484 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → 𝑌 ∈ 𝐵) |
26 | 24, 25 | eqeltrd 2833 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {𝑌})‘𝑘) ∈ 𝐵) |
27 | 3, 4 | mndcl 18037 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) |
28 | 2, 16, 22, 27 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑋 + 𝑌) ∈ 𝐵) |
29 | | fvconst2g 6976 |
. . . . . 6
⊢ (((𝑋 + 𝑌) ∈ 𝐵 ∧ 𝑘 ∈ ℕ) → ((ℕ ×
{(𝑋 + 𝑌)})‘𝑘) = (𝑋 + 𝑌)) |
30 | 28, 17, 29 | syl2an 599 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {(𝑋 + 𝑌)})‘𝑘) = (𝑋 + 𝑌)) |
31 | 19, 24 | oveq12d 7190 |
. . . . 5
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → (((ℕ × {𝑋})‘𝑘) + ((ℕ × {𝑌})‘𝑘)) = (𝑋 + 𝑌)) |
32 | 30, 31 | eqtr4d 2776 |
. . . 4
⊢ ((((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑀)) → ((ℕ × {(𝑋 + 𝑌)})‘𝑘) = (((ℕ × {𝑋})‘𝑘) + ((ℕ × {𝑌})‘𝑘))) |
33 | 7, 10, 12, 15, 21, 26, 32 | seqcaopr 13501 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (seq1( + , (ℕ
× {(𝑋 + 𝑌)}))‘𝑀) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq1( + , (ℕ × {𝑌}))‘𝑀))) |
34 | | mulgdi.m |
. . . . 5
⊢ · =
(.g‘𝐺) |
35 | | eqid 2738 |
. . . . 5
⊢ seq1(
+ ,
(ℕ × {(𝑋 + 𝑌)})) = seq1( + , (ℕ × {(𝑋 + 𝑌)})) |
36 | 3, 4, 34, 35 | mulgnn 18352 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ (𝑋 + 𝑌) ∈ 𝐵) → (𝑀 · (𝑋 + 𝑌)) = (seq1( + , (ℕ × {(𝑋 + 𝑌)}))‘𝑀)) |
37 | 13, 28, 36 | syl2anc 587 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · (𝑋 + 𝑌)) = (seq1( + , (ℕ × {(𝑋 + 𝑌)}))‘𝑀)) |
38 | | eqid 2738 |
. . . . . 6
⊢ seq1(
+ ,
(ℕ × {𝑋})) =
seq1( + ,
(ℕ × {𝑋})) |
39 | 3, 4, 34, 38 | mulgnn 18352 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
40 | 13, 16, 39 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
41 | | eqid 2738 |
. . . . . 6
⊢ seq1(
+ ,
(ℕ × {𝑌})) =
seq1( + ,
(ℕ × {𝑌})) |
42 | 3, 4, 34, 41 | mulgnn 18352 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑌 ∈ 𝐵) → (𝑀 · 𝑌) = (seq1( + , (ℕ × {𝑌}))‘𝑀)) |
43 | 13, 22, 42 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · 𝑌) = (seq1( + , (ℕ × {𝑌}))‘𝑀)) |
44 | 40, 43 | oveq12d 7190 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 · 𝑋) + (𝑀 · 𝑌)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq1( + , (ℕ × {𝑌}))‘𝑀))) |
45 | 33, 37, 44 | 3eqtr4d 2783 |
. 2
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) |
46 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝐺 ∈ Mnd) |
47 | | simplr2 1217 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝑋 ∈ 𝐵) |
48 | | simplr3 1218 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝑌 ∈ 𝐵) |
49 | 46, 47, 48, 27 | syl3anc 1372 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑋 + 𝑌) ∈ 𝐵) |
50 | | eqid 2738 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
51 | 3, 50, 34 | mulg0 18351 |
. . . . 5
⊢ ((𝑋 + 𝑌) ∈ 𝐵 → (0 · (𝑋 + 𝑌)) = (0g‘𝐺)) |
52 | 49, 51 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · (𝑋 + 𝑌)) = (0g‘𝐺)) |
53 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
54 | 53, 50 | mndidcl 18044 |
. . . . . 6
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ (Base‘𝐺)) |
55 | 53, 4, 50 | mndlid 18049 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧
(0g‘𝐺)
∈ (Base‘𝐺))
→ ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺)) |
56 | 1, 54, 55 | syl2anc2 588 |
. . . . 5
⊢ (𝐺 ∈ CMnd →
((0g‘𝐺)
+
(0g‘𝐺)) =
(0g‘𝐺)) |
57 | 56 | ad2antrr 726 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺)) |
58 | 52, 57 | eqtr4d 2776 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · (𝑋 + 𝑌)) = ((0g‘𝐺) + (0g‘𝐺))) |
59 | | simpr 488 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → 𝑀 = 0) |
60 | 59 | oveq1d 7187 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · (𝑋 + 𝑌)) = (0 · (𝑋 + 𝑌))) |
61 | 59 | oveq1d 7187 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0 · 𝑋)) |
62 | 3, 50, 34 | mulg0 18351 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
63 | 47, 62 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
64 | 61, 63 | eqtrd 2773 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0g‘𝐺)) |
65 | 59 | oveq1d 7187 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑌) = (0 · 𝑌)) |
66 | 3, 50, 34 | mulg0 18351 |
. . . . . 6
⊢ (𝑌 ∈ 𝐵 → (0 · 𝑌) = (0g‘𝐺)) |
67 | 48, 66 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑌) = (0g‘𝐺)) |
68 | 65, 67 | eqtrd 2773 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑌) = (0g‘𝐺)) |
69 | 64, 68 | oveq12d 7190 |
. . 3
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 · 𝑋) + (𝑀 · 𝑌)) = ((0g‘𝐺) + (0g‘𝐺))) |
70 | 58, 60, 69 | 3eqtr4d 2783 |
. 2
⊢ (((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) |
71 | | simpr1 1195 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → 𝑀 ∈
ℕ0) |
72 | | elnn0 11980 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
73 | 71, 72 | sylib 221 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 ∈ ℕ ∨ 𝑀 = 0)) |
74 | 45, 70, 73 | mpjaodan 958 |
1
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) |