![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > symgtrinv | Structured version Visualization version GIF version |
Description: To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
Ref | Expression |
---|---|
symgtrinv.t | ⊢ 𝑇 = ran (pmTrsp‘𝐷) |
symgtrinv.g | ⊢ 𝐺 = (SymGrp‘𝐷) |
symgtrinv.i | ⊢ 𝐼 = (invg‘𝐺) |
Ref | Expression |
---|---|
symgtrinv | ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼‘(𝐺 Σg 𝑊)) = (𝐺 Σg (reverse‘𝑊))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | symgtrinv.g | . . . . 5 ⊢ 𝐺 = (SymGrp‘𝐷) | |
2 | 1 | symggrp 18263 | . . . 4 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) |
3 | eqid 2797 | . . . . 5 ⊢ (oppg‘𝐺) = (oppg‘𝐺) | |
4 | symgtrinv.i | . . . . 5 ⊢ 𝐼 = (invg‘𝐺) | |
5 | 3, 4 | invoppggim 18233 | . . . 4 ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso (oppg‘𝐺))) |
6 | gimghm 18149 | . . . 4 ⊢ (𝐼 ∈ (𝐺 GrpIso (oppg‘𝐺)) → 𝐼 ∈ (𝐺 GrpHom (oppg‘𝐺))) | |
7 | ghmmhm 18113 | . . . 4 ⊢ (𝐼 ∈ (𝐺 GrpHom (oppg‘𝐺)) → 𝐼 ∈ (𝐺 MndHom (oppg‘𝐺))) | |
8 | 2, 5, 6, 7 | 4syl 19 | . . 3 ⊢ (𝐷 ∈ 𝑉 → 𝐼 ∈ (𝐺 MndHom (oppg‘𝐺))) |
9 | symgtrinv.t | . . . . . 6 ⊢ 𝑇 = ran (pmTrsp‘𝐷) | |
10 | eqid 2797 | . . . . . 6 ⊢ (Base‘𝐺) = (Base‘𝐺) | |
11 | 9, 1, 10 | symgtrf 18332 | . . . . 5 ⊢ 𝑇 ⊆ (Base‘𝐺) |
12 | sswrd 13719 | . . . . 5 ⊢ (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺)) | |
13 | 11, 12 | ax-mp 5 | . . . 4 ⊢ Word 𝑇 ⊆ Word (Base‘𝐺) |
14 | 13 | sseli 3891 | . . 3 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊 ∈ Word (Base‘𝐺)) |
15 | 10 | gsumwmhm 17825 | . . 3 ⊢ ((𝐼 ∈ (𝐺 MndHom (oppg‘𝐺)) ∧ 𝑊 ∈ Word (Base‘𝐺)) → (𝐼‘(𝐺 Σg 𝑊)) = ((oppg‘𝐺) Σg (𝐼 ∘ 𝑊))) |
16 | 8, 14, 15 | syl2an 595 | . 2 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼‘(𝐺 Σg 𝑊)) = ((oppg‘𝐺) Σg (𝐼 ∘ 𝑊))) |
17 | 10, 4 | grpinvf 17911 | . . . . . . 7 ⊢ (𝐺 ∈ Grp → 𝐼:(Base‘𝐺)⟶(Base‘𝐺)) |
18 | 2, 17 | syl 17 | . . . . . 6 ⊢ (𝐷 ∈ 𝑉 → 𝐼:(Base‘𝐺)⟶(Base‘𝐺)) |
19 | wrdf 13716 | . . . . . . . 8 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(♯‘𝑊))⟶𝑇) | |
20 | 19 | adantl 482 | . . . . . . 7 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → 𝑊:(0..^(♯‘𝑊))⟶𝑇) |
21 | fss 6402 | . . . . . . 7 ⊢ ((𝑊:(0..^(♯‘𝑊))⟶𝑇 ∧ 𝑇 ⊆ (Base‘𝐺)) → 𝑊:(0..^(♯‘𝑊))⟶(Base‘𝐺)) | |
22 | 20, 11, 21 | sylancl 586 | . . . . . 6 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → 𝑊:(0..^(♯‘𝑊))⟶(Base‘𝐺)) |
23 | fco 6406 | . . . . . 6 ⊢ ((𝐼:(Base‘𝐺)⟶(Base‘𝐺) ∧ 𝑊:(0..^(♯‘𝑊))⟶(Base‘𝐺)) → (𝐼 ∘ 𝑊):(0..^(♯‘𝑊))⟶(Base‘𝐺)) | |
24 | 18, 22, 23 | syl2an2r 681 | . . . . 5 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼 ∘ 𝑊):(0..^(♯‘𝑊))⟶(Base‘𝐺)) |
25 | 24 | ffnd 6390 | . . . 4 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼 ∘ 𝑊) Fn (0..^(♯‘𝑊))) |
26 | 20 | ffnd 6390 | . . . 4 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → 𝑊 Fn (0..^(♯‘𝑊))) |
27 | fvco2 6632 | . . . . . 6 ⊢ ((𝑊 Fn (0..^(♯‘𝑊)) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐼 ∘ 𝑊)‘𝑥) = (𝐼‘(𝑊‘𝑥))) | |
28 | 26, 27 | sylan 580 | . . . . 5 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐼 ∘ 𝑊)‘𝑥) = (𝐼‘(𝑊‘𝑥))) |
29 | 20 | ffvelrnda 6723 | . . . . . . 7 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝑥) ∈ 𝑇) |
30 | 11, 29 | sseldi 3893 | . . . . . 6 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝑥) ∈ (Base‘𝐺)) |
31 | 1, 10, 4 | symginv 18265 | . . . . . 6 ⊢ ((𝑊‘𝑥) ∈ (Base‘𝐺) → (𝐼‘(𝑊‘𝑥)) = ◡(𝑊‘𝑥)) |
32 | 30, 31 | syl 17 | . . . . 5 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → (𝐼‘(𝑊‘𝑥)) = ◡(𝑊‘𝑥)) |
33 | eqid 2797 | . . . . . . 7 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷) | |
34 | 33, 9 | pmtrfcnv 18327 | . . . . . 6 ⊢ ((𝑊‘𝑥) ∈ 𝑇 → ◡(𝑊‘𝑥) = (𝑊‘𝑥)) |
35 | 29, 34 | syl 17 | . . . . 5 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ◡(𝑊‘𝑥) = (𝑊‘𝑥)) |
36 | 28, 32, 35 | 3eqtrd 2837 | . . . 4 ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) ∧ 𝑥 ∈ (0..^(♯‘𝑊))) → ((𝐼 ∘ 𝑊)‘𝑥) = (𝑊‘𝑥)) |
37 | 25, 26, 36 | eqfnfvd 6677 | . . 3 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼 ∘ 𝑊) = 𝑊) |
38 | 37 | oveq2d 7039 | . 2 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → ((oppg‘𝐺) Σg (𝐼 ∘ 𝑊)) = ((oppg‘𝐺) Σg 𝑊)) |
39 | grpmnd 17872 | . . . 4 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
40 | 2, 39 | syl 17 | . . 3 ⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Mnd) |
41 | 10, 3 | gsumwrev 18239 | . . 3 ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺)) → ((oppg‘𝐺) Σg 𝑊) = (𝐺 Σg (reverse‘𝑊))) |
42 | 40, 14, 41 | syl2an 595 | . 2 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → ((oppg‘𝐺) Σg 𝑊) = (𝐺 Σg (reverse‘𝑊))) |
43 | 16, 38, 42 | 3eqtrd 2837 | 1 ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼‘(𝐺 Σg 𝑊)) = (𝐺 Σg (reverse‘𝑊))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ⊆ wss 3865 ◡ccnv 5449 ran crn 5451 ∘ ccom 5454 Fn wfn 6227 ⟶wf 6228 ‘cfv 6232 (class class class)co 7023 0cc0 10390 ..^cfzo 12887 ♯chash 13544 Word cword 13711 reversecreverse 13960 Basecbs 16316 Σg cgsu 16547 Mndcmnd 17737 MndHom cmhm 17776 Grpcgrp 17865 invgcminusg 17866 GrpHom cghm 18100 GrpIso cgim 18142 oppgcoppg 18218 SymGrpcsymg 18240 pmTrspcpmtr 18304 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-cnex 10446 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 ax-pre-mulgt0 10467 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-int 4789 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-om 7444 df-1st 7552 df-2nd 7553 df-tpos 7750 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-1o 7960 df-2o 7961 df-oadd 7964 df-er 8146 df-map 8265 df-en 8365 df-dom 8366 df-sdom 8367 df-fin 8368 df-card 9221 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-sub 10725 df-neg 10726 df-nn 11493 df-2 11554 df-3 11555 df-4 11556 df-5 11557 df-6 11558 df-7 11559 df-8 11560 df-9 11561 df-n0 11752 df-xnn0 11822 df-z 11836 df-uz 12098 df-fz 12747 df-fzo 12888 df-seq 13224 df-hash 13545 df-word 13712 df-lsw 13765 df-concat 13773 df-s1 13798 df-substr 13843 df-pfx 13873 df-reverse 13961 df-struct 16318 df-ndx 16319 df-slot 16320 df-base 16322 df-sets 16323 df-ress 16324 df-plusg 16411 df-tset 16417 df-0g 16548 df-gsum 16549 df-mgm 17685 df-sgrp 17727 df-mnd 17738 df-mhm 17778 df-submnd 17779 df-grp 17868 df-minusg 17869 df-ghm 18101 df-gim 18144 df-oppg 18219 df-symg 18241 df-pmtr 18305 |
This theorem is referenced by: psgnuni 18362 |
Copyright terms: Public domain | W3C validator |