| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑂 Σg
𝑥) = (𝑂 Σg
∅)) |
| 2 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = ∅ →
(reverse‘𝑥) =
(reverse‘∅)) |
| 3 | | rev0 14802 |
. . . . . . 7
⊢
(reverse‘∅) = ∅ |
| 4 | 2, 3 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑥 = ∅ →
(reverse‘𝑥) =
∅) |
| 5 | 4 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑀 Σg
(reverse‘𝑥)) = (𝑀 Σg
∅)) |
| 6 | 1, 5 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = ∅ → ((𝑂 Σg
𝑥) = (𝑀 Σg
(reverse‘𝑥)) ↔
(𝑂
Σg ∅) = (𝑀 Σg
∅))) |
| 7 | 6 | imbi2d 340 |
. . 3
⊢ (𝑥 = ∅ → ((𝑀 ∈ Mnd → (𝑂 Σg
𝑥) = (𝑀 Σg
(reverse‘𝑥))) ↔
(𝑀 ∈ Mnd → (𝑂 Σg
∅) = (𝑀
Σg ∅)))) |
| 8 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑂 Σg 𝑥) = (𝑂 Σg 𝑦)) |
| 9 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (reverse‘𝑥) = (reverse‘𝑦)) |
| 10 | 9 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑀 Σg
(reverse‘𝑥)) = (𝑀 Σg
(reverse‘𝑦))) |
| 11 | 8, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑂 Σg 𝑥) = (𝑀 Σg
(reverse‘𝑥)) ↔
(𝑂
Σg 𝑦) = (𝑀 Σg
(reverse‘𝑦)))) |
| 12 | 11 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑀 ∈ Mnd → (𝑂 Σg 𝑥) = (𝑀 Σg
(reverse‘𝑥))) ↔
(𝑀 ∈ Mnd → (𝑂 Σg
𝑦) = (𝑀 Σg
(reverse‘𝑦))))) |
| 13 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝑂 Σg 𝑥) = (𝑂 Σg (𝑦 ++ 〈“𝑧”〉))) |
| 14 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (reverse‘𝑥) = (reverse‘(𝑦 ++ 〈“𝑧”〉))) |
| 15 | 14 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → (𝑀 Σg
(reverse‘𝑥)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉)))) |
| 16 | 13, 15 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → ((𝑂 Σg 𝑥) = (𝑀 Σg
(reverse‘𝑥)) ↔
(𝑂
Σg (𝑦 ++ 〈“𝑧”〉)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉))))) |
| 17 | 16 | imbi2d 340 |
. . 3
⊢ (𝑥 = (𝑦 ++ 〈“𝑧”〉) → ((𝑀 ∈ Mnd → (𝑂 Σg 𝑥) = (𝑀 Σg
(reverse‘𝑥))) ↔
(𝑀 ∈ Mnd → (𝑂 Σg
(𝑦 ++ 〈“𝑧”〉)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉)))))) |
| 18 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑊 → (𝑂 Σg 𝑥) = (𝑂 Σg 𝑊)) |
| 19 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑊 → (reverse‘𝑥) = (reverse‘𝑊)) |
| 20 | 19 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑊 → (𝑀 Σg
(reverse‘𝑥)) = (𝑀 Σg
(reverse‘𝑊))) |
| 21 | 18, 20 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑊 → ((𝑂 Σg 𝑥) = (𝑀 Σg
(reverse‘𝑥)) ↔
(𝑂
Σg 𝑊) = (𝑀 Σg
(reverse‘𝑊)))) |
| 22 | 21 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑊 → ((𝑀 ∈ Mnd → (𝑂 Σg 𝑥) = (𝑀 Σg
(reverse‘𝑥))) ↔
(𝑀 ∈ Mnd → (𝑂 Σg
𝑊) = (𝑀 Σg
(reverse‘𝑊))))) |
| 23 | | gsumwrev.o |
. . . . . . 7
⊢ 𝑂 =
(oppg‘𝑀) |
| 24 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 25 | 23, 24 | oppgid 19375 |
. . . . . 6
⊢
(0g‘𝑀) = (0g‘𝑂) |
| 26 | 25 | gsum0 18697 |
. . . . 5
⊢ (𝑂 Σg
∅) = (0g‘𝑀) |
| 27 | 24 | gsum0 18697 |
. . . . 5
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
| 28 | 26, 27 | eqtr4i 2768 |
. . . 4
⊢ (𝑂 Σg
∅) = (𝑀
Σg ∅) |
| 29 | 28 | a1i 11 |
. . 3
⊢ (𝑀 ∈ Mnd → (𝑂 Σg
∅) = (𝑀
Σg ∅)) |
| 30 | | oveq2 7439 |
. . . . . 6
⊢ ((𝑂 Σg
𝑦) = (𝑀 Σg
(reverse‘𝑦)) →
(𝑧(+g‘𝑀)(𝑂 Σg 𝑦)) = (𝑧(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦)))) |
| 31 | 23 | oppgmnd 19373 |
. . . . . . . . . 10
⊢ (𝑀 ∈ Mnd → 𝑂 ∈ Mnd) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑂 ∈ Mnd) |
| 33 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ Word 𝐵) |
| 34 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵) |
| 35 | 34 | s1cld 14641 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → 〈“𝑧”〉 ∈ Word 𝐵) |
| 36 | | gsumwrev.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑀) |
| 37 | 23, 36 | oppgbas 19370 |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑂) |
| 38 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑂) = (+g‘𝑂) |
| 39 | 37, 38 | gsumccat 18854 |
. . . . . . . . 9
⊢ ((𝑂 ∈ Mnd ∧ 𝑦 ∈ Word 𝐵 ∧ 〈“𝑧”〉 ∈ Word 𝐵) → (𝑂 Σg (𝑦 ++ 〈“𝑧”〉)) = ((𝑂 Σg
𝑦)(+g‘𝑂)(𝑂 Σg
〈“𝑧”〉))) |
| 40 | 32, 33, 35, 39 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑂 Σg (𝑦 ++ 〈“𝑧”〉)) = ((𝑂 Σg
𝑦)(+g‘𝑂)(𝑂 Σg
〈“𝑧”〉))) |
| 41 | 37 | gsumws1 18851 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐵 → (𝑂 Σg
〈“𝑧”〉) = 𝑧) |
| 42 | 41 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑂 Σg
〈“𝑧”〉) = 𝑧) |
| 43 | 42 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑂 Σg 𝑦)(+g‘𝑂)(𝑂 Σg
〈“𝑧”〉)) = ((𝑂 Σg 𝑦)(+g‘𝑂)𝑧)) |
| 44 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 45 | 44, 23, 38 | oppgplus 19367 |
. . . . . . . . 9
⊢ ((𝑂 Σg
𝑦)(+g‘𝑂)𝑧) = (𝑧(+g‘𝑀)(𝑂 Σg 𝑦)) |
| 46 | 43, 45 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑂 Σg 𝑦)(+g‘𝑂)(𝑂 Σg
〈“𝑧”〉)) = (𝑧(+g‘𝑀)(𝑂 Σg 𝑦))) |
| 47 | 40, 46 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑂 Σg (𝑦 ++ 〈“𝑧”〉)) = (𝑧(+g‘𝑀)(𝑂 Σg 𝑦))) |
| 48 | | revccat 14804 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ Word 𝐵 ∧ 〈“𝑧”〉 ∈ Word 𝐵) → (reverse‘(𝑦 ++ 〈“𝑧”〉)) =
((reverse‘〈“𝑧”〉) ++ (reverse‘𝑦))) |
| 49 | 33, 35, 48 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (reverse‘(𝑦 ++ 〈“𝑧”〉)) =
((reverse‘〈“𝑧”〉) ++ (reverse‘𝑦))) |
| 50 | | revs1 14803 |
. . . . . . . . . . 11
⊢
(reverse‘〈“𝑧”〉) = 〈“𝑧”〉 |
| 51 | 50 | oveq1i 7441 |
. . . . . . . . . 10
⊢
((reverse‘〈“𝑧”〉) ++ (reverse‘𝑦)) = (〈“𝑧”〉 ++
(reverse‘𝑦)) |
| 52 | 49, 51 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (reverse‘(𝑦 ++ 〈“𝑧”〉)) = (〈“𝑧”〉 ++
(reverse‘𝑦))) |
| 53 | 52 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉))) = (𝑀 Σg
(〈“𝑧”〉 ++ (reverse‘𝑦)))) |
| 54 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑀 ∈ Mnd) |
| 55 | | revcl 14799 |
. . . . . . . . . 10
⊢ (𝑦 ∈ Word 𝐵 → (reverse‘𝑦) ∈ Word 𝐵) |
| 56 | 55 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (reverse‘𝑦) ∈ Word 𝐵) |
| 57 | 36, 44 | gsumccat 18854 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧
〈“𝑧”〉
∈ Word 𝐵 ∧
(reverse‘𝑦) ∈
Word 𝐵) → (𝑀 Σg
(〈“𝑧”〉 ++ (reverse‘𝑦))) = ((𝑀 Σg
〈“𝑧”〉)(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦)))) |
| 58 | 54, 35, 56, 57 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 Σg
(〈“𝑧”〉 ++ (reverse‘𝑦))) = ((𝑀 Σg
〈“𝑧”〉)(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦)))) |
| 59 | 36 | gsumws1 18851 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐵 → (𝑀 Σg
〈“𝑧”〉) = 𝑧) |
| 60 | 59 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 Σg
〈“𝑧”〉) = 𝑧) |
| 61 | 60 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑀 Σg
〈“𝑧”〉)(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦))) =
(𝑧(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦)))) |
| 62 | 53, 58, 61 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉))) = (𝑧(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦)))) |
| 63 | 47, 62 | eqeq12d 2753 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑂 Σg (𝑦 ++ 〈“𝑧”〉)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉))) ↔ (𝑧(+g‘𝑀)(𝑂 Σg 𝑦)) = (𝑧(+g‘𝑀)(𝑀 Σg
(reverse‘𝑦))))) |
| 64 | 30, 63 | imbitrrid 246 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ (𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑂 Σg 𝑦) = (𝑀 Σg
(reverse‘𝑦)) →
(𝑂
Σg (𝑦 ++ 〈“𝑧”〉)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉))))) |
| 65 | 64 | expcom 413 |
. . . 4
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑀 ∈ Mnd → ((𝑂 Σg 𝑦) = (𝑀 Σg
(reverse‘𝑦)) →
(𝑂
Σg (𝑦 ++ 〈“𝑧”〉)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉)))))) |
| 66 | 65 | a2d 29 |
. . 3
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑀 ∈ Mnd → (𝑂 Σg 𝑦) = (𝑀 Σg
(reverse‘𝑦))) →
(𝑀 ∈ Mnd → (𝑂 Σg
(𝑦 ++ 〈“𝑧”〉)) = (𝑀 Σg
(reverse‘(𝑦 ++
〈“𝑧”〉)))))) |
| 67 | 7, 12, 17, 22, 29, 66 | wrdind 14760 |
. 2
⊢ (𝑊 ∈ Word 𝐵 → (𝑀 ∈ Mnd → (𝑂 Σg 𝑊) = (𝑀 Σg
(reverse‘𝑊)))) |
| 68 | 67 | impcom 407 |
1
⊢ ((𝑀 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝑂 Σg 𝑊) = (𝑀 Σg
(reverse‘𝑊))) |