MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pmtrfconj Structured version   Visualization version   GIF version

Theorem pmtrfconj 18891
Description: Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.)
Hypotheses
Ref Expression
pmtrrn.t 𝑇 = (pmTrsp‘𝐷)
pmtrrn.r 𝑅 = ran 𝑇
Assertion
Ref Expression
pmtrfconj ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → ((𝐺𝐹) ∘ 𝐺) ∈ 𝑅)

Proof of Theorem pmtrfconj
StepHypRef Expression
1 pmtrrn.t . . . . 5 𝑇 = (pmTrsp‘𝐷)
2 pmtrrn.r . . . . 5 𝑅 = ran 𝑇
31, 2pmtrfb 18890 . . . 4 (𝐹𝑅 ↔ (𝐷 ∈ V ∧ 𝐹:𝐷1-1-onto𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o))
43simp1bi 1147 . . 3 (𝐹𝑅𝐷 ∈ V)
54adantr 484 . 2 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → 𝐷 ∈ V)
6 simpr 488 . . . 4 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → 𝐺:𝐷1-1-onto𝐷)
71, 2pmtrff1o 18888 . . . . 5 (𝐹𝑅𝐹:𝐷1-1-onto𝐷)
87adantr 484 . . . 4 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → 𝐹:𝐷1-1-onto𝐷)
9 f1oco 6705 . . . 4 ((𝐺:𝐷1-1-onto𝐷𝐹:𝐷1-1-onto𝐷) → (𝐺𝐹):𝐷1-1-onto𝐷)
106, 8, 9syl2anc 587 . . 3 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → (𝐺𝐹):𝐷1-1-onto𝐷)
11 f1ocnv 6695 . . . 4 (𝐺:𝐷1-1-onto𝐷𝐺:𝐷1-1-onto𝐷)
1211adantl 485 . . 3 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → 𝐺:𝐷1-1-onto𝐷)
13 f1oco 6705 . . 3 (((𝐺𝐹):𝐷1-1-onto𝐷𝐺:𝐷1-1-onto𝐷) → ((𝐺𝐹) ∘ 𝐺):𝐷1-1-onto𝐷)
1410, 12, 13syl2anc 587 . 2 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → ((𝐺𝐹) ∘ 𝐺):𝐷1-1-onto𝐷)
15 f1of 6683 . . . . . . 7 (𝐹:𝐷1-1-onto𝐷𝐹:𝐷𝐷)
167, 15syl 17 . . . . . 6 (𝐹𝑅𝐹:𝐷𝐷)
1716adantr 484 . . . . 5 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → 𝐹:𝐷𝐷)
18 f1omvdconj 18871 . . . . 5 ((𝐹:𝐷𝐷𝐺:𝐷1-1-onto𝐷) → dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) = (𝐺 “ dom (𝐹 ∖ I )))
1917, 6, 18syl2anc 587 . . . 4 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) = (𝐺 “ dom (𝐹 ∖ I )))
20 f1of1 6682 . . . . . 6 (𝐺:𝐷1-1-onto𝐷𝐺:𝐷1-1𝐷)
2120adantl 485 . . . . 5 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → 𝐺:𝐷1-1𝐷)
22 difss 4063 . . . . . . 7 (𝐹 ∖ I ) ⊆ 𝐹
23 dmss 5789 . . . . . . 7 ((𝐹 ∖ I ) ⊆ 𝐹 → dom (𝐹 ∖ I ) ⊆ dom 𝐹)
2422, 23ax-mp 5 . . . . . 6 dom (𝐹 ∖ I ) ⊆ dom 𝐹
2524, 17fssdm 6587 . . . . 5 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → dom (𝐹 ∖ I ) ⊆ 𝐷)
265, 25ssexd 5234 . . . . 5 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → dom (𝐹 ∖ I ) ∈ V)
27 f1imaeng 8714 . . . . 5 ((𝐺:𝐷1-1𝐷 ∧ dom (𝐹 ∖ I ) ⊆ 𝐷 ∧ dom (𝐹 ∖ I ) ∈ V) → (𝐺 “ dom (𝐹 ∖ I )) ≈ dom (𝐹 ∖ I ))
2821, 25, 26, 27syl3anc 1373 . . . 4 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → (𝐺 “ dom (𝐹 ∖ I )) ≈ dom (𝐹 ∖ I ))
2919, 28eqbrtrd 5092 . . 3 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) ≈ dom (𝐹 ∖ I ))
303simp3bi 1149 . . . 4 (𝐹𝑅 → dom (𝐹 ∖ I ) ≈ 2o)
3130adantr 484 . . 3 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → dom (𝐹 ∖ I ) ≈ 2o)
32 entr 8706 . . 3 ((dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) ≈ dom (𝐹 ∖ I ) ∧ dom (𝐹 ∖ I ) ≈ 2o) → dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) ≈ 2o)
3329, 31, 32syl2anc 587 . 2 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) ≈ 2o)
341, 2pmtrfb 18890 . 2 (((𝐺𝐹) ∘ 𝐺) ∈ 𝑅 ↔ (𝐷 ∈ V ∧ ((𝐺𝐹) ∘ 𝐺):𝐷1-1-onto𝐷 ∧ dom (((𝐺𝐹) ∘ 𝐺) ∖ I ) ≈ 2o))
355, 14, 33, 34syl3anbrc 1345 1 ((𝐹𝑅𝐺:𝐷1-1-onto𝐷) → ((𝐺𝐹) ∘ 𝐺) ∈ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2112  Vcvv 3423  cdif 3880  wss 3883   class class class wbr 5070   I cid 5471  ccnv 5568  dom cdm 5569  ran crn 5570  cima 5572  ccom 5573  wf 6397  1-1wf1 6398  1-1-ontowf1o 6400  cfv 6401  2oc2o 8220  cen 8647  pmTrspcpmtr 18866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-om 7667  df-1o 8226  df-2o 8227  df-er 8415  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-pmtr 18867
This theorem is referenced by:  psgnunilem1  18918
  Copyright terms: Public domain W3C validator