Metamath Proof Explorer


Theorem gsumwrev

Description: A sum in an opposite monoid is the regular sum of a reversed word. (Contributed by Stefan O'Rear, 27-Aug-2015) (Proof shortened by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses gsumwrev.b B = Base M
gsumwrev.o O = opp 𝑔 M
Assertion gsumwrev M Mnd W Word B O W = M reverse W

Proof

Step Hyp Ref Expression
1 gsumwrev.b B = Base M
2 gsumwrev.o O = opp 𝑔 M
3 oveq2 x = O x = O
4 fveq2 x = reverse x = reverse
5 rev0 reverse =
6 4 5 eqtrdi x = reverse x =
7 6 oveq2d x = M reverse x = M
8 3 7 eqeq12d x = O x = M reverse x O = M
9 8 imbi2d x = M Mnd O x = M reverse x M Mnd O = M
10 oveq2 x = y O x = O y
11 fveq2 x = y reverse x = reverse y
12 11 oveq2d x = y M reverse x = M reverse y
13 10 12 eqeq12d x = y O x = M reverse x O y = M reverse y
14 13 imbi2d x = y M Mnd O x = M reverse x M Mnd O y = M reverse y
15 oveq2 x = y ++ ⟨“ z ”⟩ O x = O y ++ ⟨“ z ”⟩
16 fveq2 x = y ++ ⟨“ z ”⟩ reverse x = reverse y ++ ⟨“ z ”⟩
17 16 oveq2d x = y ++ ⟨“ z ”⟩ M reverse x = M reverse y ++ ⟨“ z ”⟩
18 15 17 eqeq12d x = y ++ ⟨“ z ”⟩ O x = M reverse x O y ++ ⟨“ z ”⟩ = M reverse y ++ ⟨“ z ”⟩
19 18 imbi2d x = y ++ ⟨“ z ”⟩ M Mnd O x = M reverse x M Mnd O y ++ ⟨“ z ”⟩ = M reverse y ++ ⟨“ z ”⟩
20 oveq2 x = W O x = O W
21 fveq2 x = W reverse x = reverse W
22 21 oveq2d x = W M reverse x = M reverse W
23 20 22 eqeq12d x = W O x = M reverse x O W = M reverse W
24 23 imbi2d x = W M Mnd O x = M reverse x M Mnd O W = M reverse W
25 eqid 0 M = 0 M
26 2 25 oppgid 0 M = 0 O
27 26 gsum0 O = 0 M
28 25 gsum0 M = 0 M
29 27 28 eqtr4i O = M
30 29 a1i M Mnd O = M
31 oveq2 O y = M reverse y z + M O y = z + M M reverse y
32 2 oppgmnd M Mnd O Mnd
33 32 adantr M Mnd y Word B z B O Mnd
34 simprl M Mnd y Word B z B y Word B
35 simprr M Mnd y Word B z B z B
36 35 s1cld M Mnd y Word B z B ⟨“ z ”⟩ Word B
37 2 1 oppgbas B = Base O
38 eqid + O = + O
39 37 38 gsumccat O Mnd y Word B ⟨“ z ”⟩ Word B O y ++ ⟨“ z ”⟩ = O y + O O ⟨“ z ”⟩
40 33 34 36 39 syl3anc M Mnd y Word B z B O y ++ ⟨“ z ”⟩ = O y + O O ⟨“ z ”⟩
41 37 gsumws1 z B O ⟨“ z ”⟩ = z
42 41 ad2antll M Mnd y Word B z B O ⟨“ z ”⟩ = z
43 42 oveq2d M Mnd y Word B z B O y + O O ⟨“ z ”⟩ = O y + O z
44 eqid + M = + M
45 44 2 38 oppgplus O y + O z = z + M O y
46 43 45 eqtrdi M Mnd y Word B z B O y + O O ⟨“ z ”⟩ = z + M O y
47 40 46 eqtrd M Mnd y Word B z B O y ++ ⟨“ z ”⟩ = z + M O y
48 revccat y Word B ⟨“ z ”⟩ Word B reverse y ++ ⟨“ z ”⟩ = reverse ⟨“ z ”⟩ ++ reverse y
49 34 36 48 syl2anc M Mnd y Word B z B reverse y ++ ⟨“ z ”⟩ = reverse ⟨“ z ”⟩ ++ reverse y
50 revs1 reverse ⟨“ z ”⟩ = ⟨“ z ”⟩
51 50 oveq1i reverse ⟨“ z ”⟩ ++ reverse y = ⟨“ z ”⟩ ++ reverse y
52 49 51 eqtrdi M Mnd y Word B z B reverse y ++ ⟨“ z ”⟩ = ⟨“ z ”⟩ ++ reverse y
53 52 oveq2d M Mnd y Word B z B M reverse y ++ ⟨“ z ”⟩ = M ⟨“ z ”⟩ ++ reverse y
54 simpl M Mnd y Word B z B M Mnd
55 revcl y Word B reverse y Word B
56 55 ad2antrl M Mnd y Word B z B reverse y Word B
57 1 44 gsumccat M Mnd ⟨“ z ”⟩ Word B reverse y Word B M ⟨“ z ”⟩ ++ reverse y = M ⟨“ z ”⟩ + M M reverse y
58 54 36 56 57 syl3anc M Mnd y Word B z B M ⟨“ z ”⟩ ++ reverse y = M ⟨“ z ”⟩ + M M reverse y
59 1 gsumws1 z B M ⟨“ z ”⟩ = z
60 59 ad2antll M Mnd y Word B z B M ⟨“ z ”⟩ = z
61 60 oveq1d M Mnd y Word B z B M ⟨“ z ”⟩ + M M reverse y = z + M M reverse y
62 53 58 61 3eqtrd M Mnd y Word B z B M reverse y ++ ⟨“ z ”⟩ = z + M M reverse y
63 47 62 eqeq12d M Mnd y Word B z B O y ++ ⟨“ z ”⟩ = M reverse y ++ ⟨“ z ”⟩ z + M O y = z + M M reverse y
64 31 63 syl5ibr M Mnd y Word B z B O y = M reverse y O y ++ ⟨“ z ”⟩ = M reverse y ++ ⟨“ z ”⟩
65 64 expcom y Word B z B M Mnd O y = M reverse y O y ++ ⟨“ z ”⟩ = M reverse y ++ ⟨“ z ”⟩
66 65 a2d y Word B z B M Mnd O y = M reverse y M Mnd O y ++ ⟨“ z ”⟩ = M reverse y ++ ⟨“ z ”⟩
67 9 14 19 24 30 66 wrdind W Word B M Mnd O W = M reverse W
68 67 impcom M Mnd W Word B O W = M reverse W