This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
gsumwrev.o ⊢ 𝑂 = ( oppg ‘ 𝑀 )
Assertion gsumwrev ( ( 𝑀 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ) → ( 𝑂 Σg 𝑊 ) = ( 𝑀 Σg ( reverse ‘ 𝑊 ) ) )

Proof

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