symgtrinv

Description: To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015)

	Ref	Expression
Hypotheses	symgtrinv.t	$⊢ T = ran pmTrsp (D)$
	symgtrinv.g	$⊢ G = SymGrp (D)$
	symgtrinv.i	$⊢ I = {inv}_{g} (G)$
Assertion	symgtrinv	$⊢ (D \in V \land W \in Word T) \to I (\sum_{G} W) = \sum_{G} reverse (W)$

Proof

Step	Hyp	Ref	Expression
1		symgtrinv.t	$⊢ T = ran pmTrsp (D)$
2		symgtrinv.g	$⊢ G = SymGrp (D)$
3		symgtrinv.i	$⊢ I = {inv}_{g} (G)$
4	2	symggrp	$⊢ D \in V \to G \in Grp$
5		eqid	$⊢ {opp}_{𝑔} (G) = {opp}_{𝑔} (G)$
6	5 3	invoppggim	$⊢ G \in Grp \to I \in (G GrpIso {opp}_{𝑔} (G))$
7		gimghm	$⊢ I \in (G GrpIso {opp}_{𝑔} (G)) \to I \in (G GrpHom {opp}_{𝑔} (G))$
8		ghmmhm	$⊢ I \in (G GrpHom {opp}_{𝑔} (G)) \to I \in (G MndHom {opp}_{𝑔} (G))$
9	4 6 7 8	4syl	$⊢ D \in V \to I \in (G MndHom {opp}_{𝑔} (G))$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	1 2 10	symgtrf	$⊢ T \subseteq {Base}_{G}$
12		sswrd	$⊢ T \subseteq {Base}_{G} \to Word T \subseteq Word {Base}_{G}$
13	11 12	ax-mp	$⊢ Word T \subseteq Word {Base}_{G}$
14	13	sseli	$⊢ W \in Word T \to W \in Word {Base}_{G}$
15	10	gsumwmhm	$⊢ (I \in (G MndHom {opp}_{𝑔} (G)) \land W \in Word {Base}_{G}) \to I (\sum_{G} W) = \sum_{{opp}_{𝑔} (G)} (I \circ W)$
16	9 14 15	syl2an	$⊢ (D \in V \land W \in Word T) \to I (\sum_{G} W) = \sum_{{opp}_{𝑔} (G)} (I \circ W)$
17	10 3	grpinvf	$⊢ G \in Grp \to I : {Base}_{G} ⟶ {Base}_{G}$
18	4 17	syl	$⊢ D \in V \to I : {Base}_{G} ⟶ {Base}_{G}$
19		wrdf	$⊢ W \in Word T \to W : (0 ..^\|W\|) ⟶ T$
20	19	adantl	$⊢ (D \in V \land W \in Word T) \to W : (0 ..^\|W\|) ⟶ T$
21		fss	$⊢ (W : (0 ..^\|W\|) ⟶ T \land T \subseteq {Base}_{G}) \to W : (0 ..^\|W\|) ⟶ {Base}_{G}$
22	20 11 21	sylancl	$⊢ (D \in V \land W \in Word T) \to W : (0 ..^\|W\|) ⟶ {Base}_{G}$
23		fco	$⊢ (I : {Base}_{G} ⟶ {Base}_{G} \land W : (0 ..^\|W\|) ⟶ {Base}_{G}) \to (I \circ W) : (0 ..^\|W\|) ⟶ {Base}_{G}$
24	18 22 23	syl2an2r	$⊢ (D \in V \land W \in Word T) \to (I \circ W) : (0 ..^\|W\|) ⟶ {Base}_{G}$
25	24	ffnd	$⊢ (D \in V \land W \in Word T) \to (I \circ W) Fn (0 ..^\|W\|)$
26	20	ffnd	$⊢ (D \in V \land W \in Word T) \to W Fn (0 ..^\|W\|)$
27		fvco2	$⊢ (W Fn (0 ..^\|W\|) \land x \in (0 ..^\|W\|)) \to (I \circ W) (x) = I (W (x))$
28	26 27	sylan	$⊢ ((D \in V \land W \in Word T) \land x \in (0 ..^\|W\|)) \to (I \circ W) (x) = I (W (x))$
29	20	ffvelcdmda	$⊢ ((D \in V \land W \in Word T) \land x \in (0 ..^\|W\|)) \to W (x) \in T$
30	11 29	sselid	$⊢ ((D \in V \land W \in Word T) \land x \in (0 ..^\|W\|)) \to W (x) \in {Base}_{G}$
31	2 10 3	symginv	$⊢ W (x) \in {Base}_{G} \to I (W (x)) = {W (x)}^{-1}$
32	30 31	syl	$⊢ ((D \in V \land W \in Word T) \land x \in (0 ..^\|W\|)) \to I (W (x)) = {W (x)}^{-1}$
33		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
34	33 1	pmtrfcnv	$⊢ W (x) \in T \to {W (x)}^{-1} = W (x)$
35	29 34	syl	$⊢ ((D \in V \land W \in Word T) \land x \in (0 ..^\|W\|)) \to {W (x)}^{-1} = W (x)$
36	28 32 35	3eqtrd	$⊢ ((D \in V \land W \in Word T) \land x \in (0 ..^\|W\|)) \to (I \circ W) (x) = W (x)$
37	25 26 36	eqfnfvd	$⊢ (D \in V \land W \in Word T) \to I \circ W = W$
38	37	oveq2d	$⊢ (D \in V \land W \in Word T) \to \sum_{{opp}_{𝑔} (G)} (I \circ W) = \sum_{{opp}_{𝑔} (G)} W$
39	4	grpmndd	$⊢ D \in V \to G \in Mnd$
40	10 5	gsumwrev	$⊢ (G \in Mnd \land W \in Word {Base}_{G}) \to \sum_{{opp}_{𝑔} (G)} W = \sum_{G} reverse (W)$
41	39 14 40	syl2an	$⊢ (D \in V \land W \in Word T) \to \sum_{{opp}_{𝑔} (G)} W = \sum_{G} reverse (W)$
42	16 38 41	3eqtrd	$⊢ (D \in V \land W \in Word T) \to I (\sum_{G} W) = \sum_{G} reverse (W)$

Metamath Proof Explorer

Theorem symgtrinv

Proof