Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . 5
β’ (π₯ = β
β (π Ξ£g
π₯) = (π Ξ£g
β
)) |
2 | | fveq2 6847 |
. . . . . . 7
β’ (π₯ = β
β
(reverseβπ₯) =
(reverseββ
)) |
3 | | rev0 14659 |
. . . . . . 7
β’
(reverseββ
) = β
|
4 | 2, 3 | eqtrdi 2793 |
. . . . . 6
β’ (π₯ = β
β
(reverseβπ₯) =
β
) |
5 | 4 | oveq2d 7378 |
. . . . 5
β’ (π₯ = β
β (π Ξ£g
(reverseβπ₯)) = (π Ξ£g
β
)) |
6 | 1, 5 | eqeq12d 2753 |
. . . 4
β’ (π₯ = β
β ((π Ξ£g
π₯) = (π Ξ£g
(reverseβπ₯)) β
(π
Ξ£g β
) = (π Ξ£g
β
))) |
7 | 6 | imbi2d 341 |
. . 3
β’ (π₯ = β
β ((π β Mnd β (π Ξ£g
π₯) = (π Ξ£g
(reverseβπ₯))) β
(π β Mnd β (π Ξ£g
β
) = (π
Ξ£g β
)))) |
8 | | oveq2 7370 |
. . . . 5
β’ (π₯ = π¦ β (π Ξ£g π₯) = (π Ξ£g π¦)) |
9 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π¦ β (reverseβπ₯) = (reverseβπ¦)) |
10 | 9 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π¦ β (π Ξ£g
(reverseβπ₯)) = (π Ξ£g
(reverseβπ¦))) |
11 | 8, 10 | eqeq12d 2753 |
. . . 4
β’ (π₯ = π¦ β ((π Ξ£g π₯) = (π Ξ£g
(reverseβπ₯)) β
(π
Ξ£g π¦) = (π Ξ£g
(reverseβπ¦)))) |
12 | 11 | imbi2d 341 |
. . 3
β’ (π₯ = π¦ β ((π β Mnd β (π Ξ£g π₯) = (π Ξ£g
(reverseβπ₯))) β
(π β Mnd β (π Ξ£g
π¦) = (π Ξ£g
(reverseβπ¦))))) |
13 | | oveq2 7370 |
. . . . 5
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (π Ξ£g π₯) = (π Ξ£g (π¦ ++ β¨βπ§ββ©))) |
14 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (reverseβπ₯) = (reverseβ(π¦ ++ β¨βπ§ββ©))) |
15 | 14 | oveq2d 7378 |
. . . . 5
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (π Ξ£g
(reverseβπ₯)) = (π Ξ£g
(reverseβ(π¦ ++
β¨βπ§ββ©)))) |
16 | 13, 15 | eqeq12d 2753 |
. . . 4
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β ((π Ξ£g π₯) = (π Ξ£g
(reverseβπ₯)) β
(π
Ξ£g (π¦ ++ β¨βπ§ββ©)) = (π Ξ£g
(reverseβ(π¦ ++
β¨βπ§ββ©))))) |
17 | 16 | imbi2d 341 |
. . 3
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β ((π β Mnd β (π Ξ£g π₯) = (π Ξ£g
(reverseβπ₯))) β
(π β Mnd β (π Ξ£g
(π¦ ++ β¨βπ§ββ©)) = (π Ξ£g
(reverseβ(π¦ ++
β¨βπ§ββ©)))))) |
18 | | oveq2 7370 |
. . . . 5
β’ (π₯ = π β (π Ξ£g π₯) = (π Ξ£g π)) |
19 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π β (reverseβπ₯) = (reverseβπ)) |
20 | 19 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π β (π Ξ£g
(reverseβπ₯)) = (π Ξ£g
(reverseβπ))) |
21 | 18, 20 | eqeq12d 2753 |
. . . 4
β’ (π₯ = π β ((π Ξ£g π₯) = (π Ξ£g
(reverseβπ₯)) β
(π
Ξ£g π) = (π Ξ£g
(reverseβπ)))) |
22 | 21 | imbi2d 341 |
. . 3
β’ (π₯ = π β ((π β Mnd β (π Ξ£g π₯) = (π Ξ£g
(reverseβπ₯))) β
(π β Mnd β (π Ξ£g
π) = (π Ξ£g
(reverseβπ))))) |
23 | | gsumwrev.o |
. . . . . . 7
β’ π =
(oppgβπ) |
24 | | eqid 2737 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
25 | 23, 24 | oppgid 19144 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
26 | 25 | gsum0 18546 |
. . . . 5
β’ (π Ξ£g
β
) = (0gβπ) |
27 | 24 | gsum0 18546 |
. . . . 5
β’ (π Ξ£g
β
) = (0gβπ) |
28 | 26, 27 | eqtr4i 2768 |
. . . 4
β’ (π Ξ£g
β
) = (π
Ξ£g β
) |
29 | 28 | a1i 11 |
. . 3
β’ (π β Mnd β (π Ξ£g
β
) = (π
Ξ£g β
)) |
30 | | oveq2 7370 |
. . . . . 6
β’ ((π Ξ£g
π¦) = (π Ξ£g
(reverseβπ¦)) β
(π§(+gβπ)(π Ξ£g π¦)) = (π§(+gβπ)(π Ξ£g
(reverseβπ¦)))) |
31 | 23 | oppgmnd 19142 |
. . . . . . . . . 10
β’ (π β Mnd β π β Mnd) |
32 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β π β Mnd) |
33 | | simprl 770 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β π¦ β Word π΅) |
34 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β π§ β π΅) |
35 | 34 | s1cld 14498 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β β¨βπ§ββ© β Word π΅) |
36 | | gsumwrev.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ) |
37 | 23, 36 | oppgbas 19137 |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
38 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
39 | 37, 38 | gsumccat 18658 |
. . . . . . . . 9
β’ ((π β Mnd β§ π¦ β Word π΅ β§ β¨βπ§ββ© β Word π΅) β (π Ξ£g (π¦ ++ β¨βπ§ββ©)) = ((π Ξ£g
π¦)(+gβπ)(π Ξ£g
β¨βπ§ββ©))) |
40 | 32, 33, 35, 39 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (π Ξ£g (π¦ ++ β¨βπ§ββ©)) = ((π Ξ£g
π¦)(+gβπ)(π Ξ£g
β¨βπ§ββ©))) |
41 | 37 | gsumws1 18655 |
. . . . . . . . . . 11
β’ (π§ β π΅ β (π Ξ£g
β¨βπ§ββ©) = π§) |
42 | 41 | ad2antll 728 |
. . . . . . . . . 10
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (π Ξ£g
β¨βπ§ββ©) = π§) |
43 | 42 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β ((π Ξ£g π¦)(+gβπ)(π Ξ£g
β¨βπ§ββ©)) = ((π Ξ£g π¦)(+gβπ)π§)) |
44 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
45 | 44, 23, 38 | oppgplus 19134 |
. . . . . . . . 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 14661 |
. . . . . . . . . . 11
β’ ((π¦ β Word π΅ β§ β¨βπ§ββ© β Word π΅) β (reverseβ(π¦ ++ β¨βπ§ββ©)) =
((reverseββ¨βπ§ββ©) ++ (reverseβπ¦))) |
49 | 33, 35, 48 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (reverseβ(π¦ ++ β¨βπ§ββ©)) =
((reverseββ¨βπ§ββ©) ++ (reverseβπ¦))) |
50 | | revs1 14660 |
. . . . . . . . . . 11
β’
(reverseββ¨βπ§ββ©) = β¨βπ§ββ© |
51 | 50 | oveq1i 7372 |
. . . . . . . . . 10
β’
((reverseββ¨βπ§ββ©) ++ (reverseβπ¦)) = (β¨βπ§ββ© ++
(reverseβπ¦)) |
52 | 49, 51 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (reverseβ(π¦ ++ β¨βπ§ββ©)) = (β¨βπ§ββ© ++
(reverseβπ¦))) |
53 | 52 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (π Ξ£g
(reverseβ(π¦ ++
β¨βπ§ββ©))) = (π Ξ£g
(β¨βπ§ββ© ++ (reverseβπ¦)))) |
54 | | simpl 484 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β π β Mnd) |
55 | | revcl 14656 |
. . . . . . . . . 10
β’ (π¦ β Word π΅ β (reverseβπ¦) β Word π΅) |
56 | 55 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (reverseβπ¦) β Word π΅) |
57 | 36, 44 | gsumccat 18658 |
. . . . . . . . 9
β’ ((π β Mnd β§
β¨βπ§ββ©
β Word π΅ β§
(reverseβπ¦) β
Word π΅) β (π Ξ£g
(β¨βπ§ββ© ++ (reverseβπ¦))) = ((π Ξ£g
β¨βπ§ββ©)(+gβπ)(π Ξ£g
(reverseβπ¦)))) |
58 | 54, 35, 56, 57 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (π Ξ£g
(β¨βπ§ββ© ++ (reverseβπ¦))) = ((π Ξ£g
β¨βπ§ββ©)(+gβπ)(π Ξ£g
(reverseβπ¦)))) |
59 | 36 | gsumws1 18655 |
. . . . . . . . . 10
β’ (π§ β π΅ β (π Ξ£g
β¨βπ§ββ©) = π§) |
60 | 59 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β (π Ξ£g
β¨βπ§ββ©) = π§) |
61 | 60 | oveq1d 7377 |
. . . . . . . 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 | syl5ibr 246 |
. . . . 5
β’ ((π β Mnd β§ (π¦ β Word π΅ β§ π§ β π΅)) β ((π Ξ£g π¦) = (π Ξ£g
(reverseβπ¦)) β
(π
Ξ£g (π¦ ++ β¨βπ§ββ©)) = (π Ξ£g
(reverseβ(π¦ ++
β¨βπ§ββ©))))) |
65 | 64 | expcom 415 |
. . . 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 14617 |
. 2
β’ (π β Word π΅ β (π β Mnd β (π Ξ£g π) = (π Ξ£g
(reverseβπ)))) |
68 | 67 | impcom 409 |
1
β’ ((π β Mnd β§ π β Word π΅) β (π Ξ£g π) = (π Ξ£g
(reverseβπ))) |