Metamath Proof Explorer

Theorem 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 ∈ V ∧ W ∈ Word T → I ⁡ ∑ G W = ∑ 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 ∈ V → G ∈ Grp
5 eqid ⊢ opp 𝑔 ⁡ G = opp 𝑔 ⁡ G
6 5 3 invoppggim ⊢ G ∈ Grp → I ∈ G GrpIso opp 𝑔 ⁡ G
7 gimghm ⊢ I ∈ G GrpIso opp 𝑔 ⁡ G → I ∈ G GrpHom opp 𝑔 ⁡ G
8 ghmmhm ⊢ I ∈ G GrpHom opp 𝑔 ⁡ G → I ∈ G MndHom opp 𝑔 ⁡ G
9 4 6 7 8 4syl ⊢ D ∈ V → I ∈ G MndHom opp 𝑔 ⁡ G
10 eqid ⊢ Base G = Base G
11 1 2 10 symgtrf ⊢ T ⊆ Base G
12 sswrd ⊢ T ⊆ Base G → Word T ⊆ Word Base G
13 11 12 ax-mp ⊢ Word T ⊆ Word Base G
14 13 sseli ⊢ W ∈ Word T → W ∈ Word Base G
15 10 gsumwmhm ⊢ I ∈ G MndHom opp 𝑔 ⁡ G ∧ W ∈ Word Base G → I ⁡ ∑ G W = ∑ opp 𝑔 ⁡ G I ∘ W
16 9 14 15 syl2an ⊢ D ∈ V ∧ W ∈ Word T → I ⁡ ∑ G W = ∑ opp 𝑔 ⁡ G I ∘ W
17 10 3 grpinvf ⊢ G ∈ Grp → I : Base G ⟶ Base G
18 4 17 syl ⊢ D ∈ V → I : Base G ⟶ Base G
19 wrdf ⊢ W ∈ Word T → W : 0 ..^ W ⟶ T
20 19 adantl ⊢ D ∈ V ∧ W ∈ Word T → W : 0 ..^ W ⟶ T
21 fss ⊢ W : 0 ..^ W ⟶ T ∧ T ⊆ Base G → W : 0 ..^ W ⟶ Base G
22 20 11 21 sylancl ⊢ D ∈ V ∧ W ∈ Word T → W : 0 ..^ W ⟶ Base G
23 fco ⊢ I : Base G ⟶ Base G ∧ W : 0 ..^ W ⟶ Base G → I ∘ W : 0 ..^ W ⟶ Base G
24 18 22 23 syl2an2r ⊢ D ∈ V ∧ W ∈ Word T → I ∘ W : 0 ..^ W ⟶ Base G
25 24 ffnd ⊢ D ∈ V ∧ W ∈ Word T → I ∘ W Fn 0 ..^ W
26 20 ffnd ⊢ D ∈ V ∧ W ∈ Word T → W Fn 0 ..^ W
27 fvco2 ⊢ W Fn 0 ..^ W ∧ x ∈ 0 ..^ W → I ∘ W ⁡ x = I ⁡ W ⁡ x
28 26 27 sylan ⊢ D ∈ V ∧ W ∈ Word T ∧ x ∈ 0 ..^ W → I ∘ W ⁡ x = I ⁡ W ⁡ x
29 20 ffvelcdmda ⊢ D ∈ V ∧ W ∈ Word T ∧ x ∈ 0 ..^ W → W ⁡ x ∈ T
30 11 29 sselid ⊢ D ∈ V ∧ W ∈ Word T ∧ x ∈ 0 ..^ W → W ⁡ x ∈ Base G
31 2 10 3 symginv ⊢ W ⁡ x ∈ Base G → I ⁡ W ⁡ x = W ⁡ x -1
32 30 31 syl ⊢ D ∈ V ∧ W ∈ Word T ∧ x ∈ 0 ..^ W → I ⁡ W ⁡ x = W ⁡ x -1
33 eqid ⊢ pmTrsp ⁡ D = pmTrsp ⁡ D
34 33 1 pmtrfcnv ⊢ W ⁡ x ∈ T → W ⁡ x -1 = W ⁡ x
35 29 34 syl ⊢ D ∈ V ∧ W ∈ Word T ∧ x ∈ 0 ..^ W → W ⁡ x -1 = W ⁡ x
36 28 32 35 3eqtrd ⊢ D ∈ V ∧ W ∈ Word T ∧ x ∈ 0 ..^ W → I ∘ W ⁡ x = W ⁡ x
37 25 26 36 eqfnfvd ⊢ D ∈ V ∧ W ∈ Word T → I ∘ W = W
38 37 oveq2d ⊢ D ∈ V ∧ W ∈ Word T → ∑ opp 𝑔 ⁡ G I ∘ W = ∑ opp 𝑔 ⁡ G W
39 4 grpmndd ⊢ D ∈ V → G ∈ Mnd
40 10 5 gsumwrev ⊢ G ∈ Mnd ∧ W ∈ Word Base G → ∑ opp 𝑔 ⁡ G W = ∑ G reverse ⁡ W
41 39 14 40 syl2an ⊢ D ∈ V ∧ W ∈ Word T → ∑ opp 𝑔 ⁡ G W = ∑ G reverse ⁡ W
42 16 38 41 3eqtrd ⊢ D ∈ V ∧ W ∈ Word T → I ⁡ ∑ G W = ∑ G reverse ⁡ W