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	syl5ibr	⊢ ( ( 𝑀 ∈ 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 ‘ 𝑊 ) ) )