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 \in Mnd \land W \in Word B) \to \sum_{O} W = \sum_{M} reverse (W)$

Proof

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

Metamath Proof Explorer

Theorem gsumwrev

Proof