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 
|- B = ( Base ` M )
gsumwrev.o 
|- O = ( oppG ` M )
Assertion gsumwrev 
|- ( ( M e. Mnd /\ W e. Word B ) -> ( O gsum W ) = ( M gsum ( reverse ` W ) ) )

Proof

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