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 ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
symgtrinv.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
symgtrinv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion symgtrinv ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐼 ‘ ( 𝐺 Σg 𝑊 ) ) = ( 𝐺 Σg ( reverse ‘ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 symgtrinv.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
2 symgtrinv.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
3 symgtrinv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 2 symggrp ⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Grp )
5 eqid ⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 )
6 5 3 invoppggim ⊢ ( 𝐺 ∈ Grp → 𝐼 ∈ ( 𝐺 GrpIso ( oppg ‘ 𝐺 ) ) )
7 gimghm ⊢ ( 𝐼 ∈ ( 𝐺 GrpIso ( oppg ‘ 𝐺 ) ) → 𝐼 ∈ ( 𝐺 GrpHom ( oppg ‘ 𝐺 ) ) )
8 ghmmhm ⊢ ( 𝐼 ∈ ( 𝐺 GrpHom ( oppg ‘ 𝐺 ) ) → 𝐼 ∈ ( 𝐺 MndHom ( oppg ‘ 𝐺 ) ) )
9 4 6 7 8 4syl ⊢ ( 𝐷 ∈ 𝑉 → 𝐼 ∈ ( 𝐺 MndHom ( oppg ‘ 𝐺 ) ) )
10 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 1 2 10 symgtrf ⊢ 𝑇 ⊆ ( Base ‘ 𝐺 )
12 sswrd ⊢ ( 𝑇 ⊆ ( Base ‘ 𝐺 ) → Word 𝑇 ⊆ Word ( Base ‘ 𝐺 ) )
13 11 12 ax-mp ⊢ Word 𝑇 ⊆ Word ( Base ‘ 𝐺 )
14 13 sseli ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 ∈ Word ( Base ‘ 𝐺 ) )
15 10 gsumwmhm ⊢ ( ( 𝐼 ∈ ( 𝐺 MndHom ( oppg ‘ 𝐺 ) ) ∧ 𝑊 ∈ Word ( Base ‘ 𝐺 ) ) → ( 𝐼 ‘ ( 𝐺 Σg 𝑊 ) ) = ( ( oppg ‘ 𝐺 ) Σg ( 𝐼 ∘ 𝑊 ) ) )
16 9 14 15 syl2an ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐼 ‘ ( 𝐺 Σg 𝑊 ) ) = ( ( oppg ‘ 𝐺 ) Σg ( 𝐼 ∘ 𝑊 ) ) )
17 10 3 grpinvf ⊢ ( 𝐺 ∈ Grp → 𝐼 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
18 4 17 syl ⊢ ( 𝐷 ∈ 𝑉 → 𝐼 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) )
19 wrdf ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
20 19 adantl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
21 fss ⊢ ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝐺 ) )
22 20 11 21 sylancl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝐺 ) )
23 fco ⊢ ( ( 𝐼 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐺 ) ∧ 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝐺 ) ) → ( 𝐼 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝐺 ) )
24 18 22 23 syl2an2r ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐼 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝐺 ) )
25 24 ffnd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐼 ∘ 𝑊 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
26 20 ffnd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 fvco2 ⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 ∘ 𝑊 ) ‘ 𝑥 ) = ( 𝐼 ‘ ( 𝑊 ‘ 𝑥 ) ) )
28 26 27 sylan ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 ∘ 𝑊 ) ‘ 𝑥 ) = ( 𝐼 ‘ ( 𝑊 ‘ 𝑥 ) ) )
29 20 ffvelcdmda ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑥 ) ∈ 𝑇 )
30 11 29 sselid ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
31 2 10 3 symginv ⊢ ( ( 𝑊 ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) → ( 𝐼 ‘ ( 𝑊 ‘ 𝑥 ) ) = ◡ ( 𝑊 ‘ 𝑥 ) )
32 30 31 syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 ‘ ( 𝑊 ‘ 𝑥 ) ) = ◡ ( 𝑊 ‘ 𝑥 ) )
33 eqid ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
34 33 1 pmtrfcnv ⊢ ( ( 𝑊 ‘ 𝑥 ) ∈ 𝑇 → ◡ ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ 𝑥 ) )
35 29 34 syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ◡ ( 𝑊 ‘ 𝑥 ) = ( 𝑊 ‘ 𝑥 ) )
36 28 32 35 3eqtrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 ∘ 𝑊 ) ‘ 𝑥 ) = ( 𝑊 ‘ 𝑥 ) )
37 25 26 36 eqfnfvd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐼 ∘ 𝑊 ) = 𝑊 )
38 37 oveq2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( ( oppg ‘ 𝐺 ) Σg ( 𝐼 ∘ 𝑊 ) ) = ( ( oppg ‘ 𝐺 ) Σg 𝑊 ) )
39 4 grpmndd ⊢ ( 𝐷 ∈ 𝑉 → 𝐺 ∈ Mnd )
40 10 5 gsumwrev ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word ( Base ‘ 𝐺 ) ) → ( ( oppg ‘ 𝐺 ) Σg 𝑊 ) = ( 𝐺 Σg ( reverse ‘ 𝑊 ) ) )
41 39 14 40 syl2an ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( ( oppg ‘ 𝐺 ) Σg 𝑊 ) = ( 𝐺 Σg ( reverse ‘ 𝑊 ) ) )
42 16 38 41 3eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝐼 ‘ ( 𝐺 Σg 𝑊 ) ) = ( 𝐺 Σg ( reverse ‘ 𝑊 ) ) )