Metamath Proof Explorer

Theorem pmtrfconj

Description: Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t 
|- T = ( pmTrsp ` D )
pmtrrn.r 
|- R = ran T
Assertion pmtrfconj 
|- ( ( F e. R /\ G : D -1-1-onto-> D ) -> ( ( G o. F ) o. `' G ) e. R )

Proof

Step Hyp Ref Expression
1 pmtrrn.t 
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r 
 |-  R = ran T
3 1 2 pmtrfb 
 |-  ( F e. R <-> ( D e. _V /\ F : D -1-1-onto-> D /\ dom ( F \ _I ) ~~ 2o ) )
4 3 simp1bi 
 |-  ( F e. R -> D e. _V )
5 4 adantr 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> D e. _V )
6 simpr 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> G : D -1-1-onto-> D )
7 1 2 pmtrff1o 
 |-  ( F e. R -> F : D -1-1-onto-> D )
8 7 adantr 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> F : D -1-1-onto-> D )
9 f1oco 
 |-  ( ( G : D -1-1-onto-> D /\ F : D -1-1-onto-> D ) -> ( G o. F ) : D -1-1-onto-> D )
10 6 8 9 syl2anc 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> ( G o. F ) : D -1-1-onto-> D )
11 f1ocnv 
 |-  ( G : D -1-1-onto-> D -> `' G : D -1-1-onto-> D )
12 11 adantl 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> `' G : D -1-1-onto-> D )
13 f1oco 
 |-  ( ( ( G o. F ) : D -1-1-onto-> D /\ `' G : D -1-1-onto-> D ) -> ( ( G o. F ) o. `' G ) : D -1-1-onto-> D )
14 10 12 13 syl2anc 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> ( ( G o. F ) o. `' G ) : D -1-1-onto-> D )
15 f1of 
 |-  ( F : D -1-1-onto-> D -> F : D --> D )
16 7 15 syl 
 |-  ( F e. R -> F : D --> D )
17 16 adantr 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> F : D --> D )
18 f1omvdconj 
 |-  ( ( F : D --> D /\ G : D -1-1-onto-> D ) -> dom ( ( ( G o. F ) o. `' G ) \ _I ) = ( G " dom ( F \ _I ) ) )
19 17 6 18 syl2anc 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> dom ( ( ( G o. F ) o. `' G ) \ _I ) = ( G " dom ( F \ _I ) ) )
20 f1of1 
 |-  ( G : D -1-1-onto-> D -> G : D -1-1-> D )
21 20 adantl 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> G : D -1-1-> D )
22 difss 
 |-  ( F \ _I ) C_ F
23 dmss 
 |-  ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
24 22 23 ax-mp 
 |-  dom ( F \ _I ) C_ dom F
25 24 17 fssdm 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> dom ( F \ _I ) C_ D )
26 5 25 ssexd 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> dom ( F \ _I ) e. _V )
27 f1imaeng 
 |-  ( ( G : D -1-1-> D /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) e. _V ) -> ( G " dom ( F \ _I ) ) ~~ dom ( F \ _I ) )
28 21 25 26 27 syl3anc 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> ( G " dom ( F \ _I ) ) ~~ dom ( F \ _I ) )
29 19 28 eqbrtrd 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> dom ( ( ( G o. F ) o. `' G ) \ _I ) ~~ dom ( F \ _I ) )
30 3 simp3bi 
 |-  ( F e. R -> dom ( F \ _I ) ~~ 2o )
31 30 adantr 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> dom ( F \ _I ) ~~ 2o )
32 entr 
 |-  ( ( dom ( ( ( G o. F ) o. `' G ) \ _I ) ~~ dom ( F \ _I ) /\ dom ( F \ _I ) ~~ 2o ) -> dom ( ( ( G o. F ) o. `' G ) \ _I ) ~~ 2o )
33 29 31 32 syl2anc 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> dom ( ( ( G o. F ) o. `' G ) \ _I ) ~~ 2o )
34 1 2 pmtrfb 
 |-  ( ( ( G o. F ) o. `' G ) e. R <-> ( D e. _V /\ ( ( G o. F ) o. `' G ) : D -1-1-onto-> D /\ dom ( ( ( G o. F ) o. `' G ) \ _I ) ~~ 2o ) )
35 5 14 33 34 syl3anbrc 
 |-  ( ( F e. R /\ G : D -1-1-onto-> D ) -> ( ( G o. F ) o. `' G ) e. R )