Metamath Proof Explorer

Theorem cycpm2tr

Description: A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses cycpm2.c 
|- C = ( toCyc ` D )
cycpm2.d 
|- ( ph -> D e. V )
cycpm2.i 
|- ( ph -> I e. D )
cycpm2.j 
|- ( ph -> J e. D )
cycpm2.1 
|- ( ph -> I =/= J )
cycpm2tr.t 
|- T = ( pmTrsp ` D )
Assertion cycpm2tr 
|- ( ph -> ( C ` <" I J "> ) = ( T ` { I , J } ) )

Proof

Step Hyp Ref Expression
1 cycpm2.c 
 |-  C = ( toCyc ` D )
2 cycpm2.d 
 |-  ( ph -> D e. V )
3 cycpm2.i 
 |-  ( ph -> I e. D )
4 cycpm2.j 
 |-  ( ph -> J e. D )
5 cycpm2.1 
 |-  ( ph -> I =/= J )
6 cycpm2tr.t 
 |-  T = ( pmTrsp ` D )
7 partfun 
 |-  ( x e. D |-> if ( x e. { I , J } , U. ( { I , J } \ { x } ) , x ) ) = ( ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) u. ( x e. ( D \ { I , J } ) |-> x ) )
8 7 a1i 
 |-  ( ph -> ( x e. D |-> if ( x e. { I , J } , U. ( { I , J } \ { x } ) , x ) ) = ( ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) u. ( x e. ( D \ { I , J } ) |-> x ) ) )
9 cshw1s2 
 |-  ( ( I e. D /\ J e. D ) -> ( <" I J "> cyclShift 1 ) = <" J I "> )
10 3 4 9 syl2anc 
 |-  ( ph -> ( <" I J "> cyclShift 1 ) = <" J I "> )
11 10 coeq1d 
 |-  ( ph -> ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) = ( <" J I "> o. `' <" I J "> ) )
12 0nn0 
 |-  0 e. NN0
13 12 a1i 
 |-  ( ph -> 0 e. NN0 )
14 1nn0 
 |-  1 e. NN0
15 14 a1i 
 |-  ( ph -> 1 e. NN0 )
16 0ne1 
 |-  0 =/= 1
17 16 a1i 
 |-  ( ph -> 0 =/= 1 )
18 13 4 15 3 17 3 4 5 coprprop 
 |-  ( ph -> ( { <. 0 , J >. , <. 1 , I >. } o. { <. I , 0 >. , <. J , 1 >. } ) = { <. I , J >. , <. J , I >. } )
19 s2prop 
 |-  ( ( J e. D /\ I e. D ) -> <" J I "> = { <. 0 , J >. , <. 1 , I >. } )
20 4 3 19 syl2anc 
 |-  ( ph -> <" J I "> = { <. 0 , J >. , <. 1 , I >. } )
21 s2prop 
 |-  ( ( I e. D /\ J e. D ) -> <" I J "> = { <. 0 , I >. , <. 1 , J >. } )
22 3 4 21 syl2anc 
 |-  ( ph -> <" I J "> = { <. 0 , I >. , <. 1 , J >. } )
23 22 cnveqd 
 |-  ( ph -> `' <" I J "> = `' { <. 0 , I >. , <. 1 , J >. } )
24 cnvprop 
 |-  ( ( ( 0 e. NN0 /\ I e. D ) /\ ( 1 e. NN0 /\ J e. D ) ) -> `' { <. 0 , I >. , <. 1 , J >. } = { <. I , 0 >. , <. J , 1 >. } )
25 13 3 15 4 24 syl22anc 
 |-  ( ph -> `' { <. 0 , I >. , <. 1 , J >. } = { <. I , 0 >. , <. J , 1 >. } )
26 23 25 eqtrd 
 |-  ( ph -> `' <" I J "> = { <. I , 0 >. , <. J , 1 >. } )
27 20 26 coeq12d 
 |-  ( ph -> ( <" J I "> o. `' <" I J "> ) = ( { <. 0 , J >. , <. 1 , I >. } o. { <. I , 0 >. , <. J , 1 >. } ) )
28 3 4 4 3 5 mptprop 
 |-  ( ph -> { <. I , J >. , <. J , I >. } = ( x e. { I , J } |-> if ( x = I , J , I ) ) )
29 3 4 prssd 
 |-  ( ph -> { I , J } C_ D )
30 dfss2 
 |-  ( { I , J } C_ D <-> ( { I , J } i^i D ) = { I , J } )
31 29 30 sylib 
 |-  ( ph -> ( { I , J } i^i D ) = { I , J } )
32 incom 
 |-  ( { I , J } i^i D ) = ( D i^i { I , J } )
33 31 32 eqtr3di 
 |-  ( ph -> { I , J } = ( D i^i { I , J } ) )
34 simpr 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ x = I ) -> x = I )
35 34 sneqd 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ x = I ) -> { x } = { I } )
36 35 difeq2d 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ x = I ) -> ( { I , J } \ { x } ) = ( { I , J } \ { I } ) )
37 36 unieqd 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ x = I ) -> U. ( { I , J } \ { x } ) = U. ( { I , J } \ { I } ) )
38 difprsn1 
 |-  ( I =/= J -> ( { I , J } \ { I } ) = { J } )
39 38 unieqd 
 |-  ( I =/= J -> U. ( { I , J } \ { I } ) = U. { J } )
40 5 39 syl 
 |-  ( ph -> U. ( { I , J } \ { I } ) = U. { J } )
41 unisng 
 |-  ( J e. D -> U. { J } = J )
42 4 41 syl 
 |-  ( ph -> U. { J } = J )
43 40 42 eqtrd 
 |-  ( ph -> U. ( { I , J } \ { I } ) = J )
44 43 ad2antrr 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ x = I ) -> U. ( { I , J } \ { I } ) = J )
45 37 44 eqtr2d 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ x = I ) -> J = U. ( { I , J } \ { x } ) )
46 vex 
 |-  x e. _V
47 46 elpr 
 |-  ( x e. { I , J } <-> ( x = I \/ x = J ) )
48 df-or 
 |-  ( ( x = I \/ x = J ) <-> ( -. x = I -> x = J ) )
49 47 48 sylbb 
 |-  ( x e. { I , J } -> ( -. x = I -> x = J ) )
50 49 imp 
 |-  ( ( x e. { I , J } /\ -. x = I ) -> x = J )
51 50 adantll 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ -. x = I ) -> x = J )
52 51 sneqd 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ -. x = I ) -> { x } = { J } )
53 52 difeq2d 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ -. x = I ) -> ( { I , J } \ { x } ) = ( { I , J } \ { J } ) )
54 53 unieqd 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ -. x = I ) -> U. ( { I , J } \ { x } ) = U. ( { I , J } \ { J } ) )
55 difprsn2 
 |-  ( I =/= J -> ( { I , J } \ { J } ) = { I } )
56 55 unieqd 
 |-  ( I =/= J -> U. ( { I , J } \ { J } ) = U. { I } )
57 5 56 syl 
 |-  ( ph -> U. ( { I , J } \ { J } ) = U. { I } )
58 unisng 
 |-  ( I e. D -> U. { I } = I )
59 3 58 syl 
 |-  ( ph -> U. { I } = I )
60 57 59 eqtrd 
 |-  ( ph -> U. ( { I , J } \ { J } ) = I )
61 60 ad2antrr 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ -. x = I ) -> U. ( { I , J } \ { J } ) = I )
62 54 61 eqtr2d 
 |-  ( ( ( ph /\ x e. { I , J } ) /\ -. x = I ) -> I = U. ( { I , J } \ { x } ) )
63 45 62 ifeqda 
 |-  ( ( ph /\ x e. { I , J } ) -> if ( x = I , J , I ) = U. ( { I , J } \ { x } ) )
64 33 63 mpteq12dva 
 |-  ( ph -> ( x e. { I , J } |-> if ( x = I , J , I ) ) = ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) )
65 28 64 eqtr2d 
 |-  ( ph -> ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) = { <. I , J >. , <. J , I >. } )
66 18 27 65 3eqtr4d 
 |-  ( ph -> ( <" J I "> o. `' <" I J "> ) = ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) )
67 11 66 eqtrd 
 |-  ( ph -> ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) = ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) )
68 3 4 s2rn 
 |-  ( ph -> ran <" I J "> = { I , J } )
69 68 difeq2d 
 |-  ( ph -> ( D \ ran <" I J "> ) = ( D \ { I , J } ) )
70 69 reseq2d 
 |-  ( ph -> ( _I |` ( D \ ran <" I J "> ) ) = ( _I |` ( D \ { I , J } ) ) )
71 mptresid 
 |-  ( _I |` ( D \ { I , J } ) ) = ( x e. ( D \ { I , J } ) |-> x )
72 70 71 eqtrdi 
 |-  ( ph -> ( _I |` ( D \ ran <" I J "> ) ) = ( x e. ( D \ { I , J } ) |-> x ) )
73 67 72 uneq12d 
 |-  ( ph -> ( ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) u. ( _I |` ( D \ ran <" I J "> ) ) ) = ( ( x e. ( D i^i { I , J } ) |-> U. ( { I , J } \ { x } ) ) u. ( x e. ( D \ { I , J } ) |-> x ) ) )
74 uncom 
 |-  ( ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) u. ( _I |` ( D \ ran <" I J "> ) ) ) = ( ( _I |` ( D \ ran <" I J "> ) ) u. ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) )
75 74 a1i 
 |-  ( ph -> ( ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) u. ( _I |` ( D \ ran <" I J "> ) ) ) = ( ( _I |` ( D \ ran <" I J "> ) ) u. ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) ) )
76 8 73 75 3eqtr2rd 
 |-  ( ph -> ( ( _I |` ( D \ ran <" I J "> ) ) u. ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) ) = ( x e. D |-> if ( x e. { I , J } , U. ( { I , J } \ { x } ) , x ) ) )
77 3 4 s2cld 
 |-  ( ph -> <" I J "> e. Word D )
78 3 4 5 s2f1 
 |-  ( ph -> <" I J "> : dom <" I J "> -1-1-> D )
79 1 2 77 78 tocycfv 
 |-  ( ph -> ( C ` <" I J "> ) = ( ( _I |` ( D \ ran <" I J "> ) ) u. ( ( <" I J "> cyclShift 1 ) o. `' <" I J "> ) ) )
80 enpr2 
 |-  ( ( I e. D /\ J e. D /\ I =/= J ) -> { I , J } ~~ 2o )
81 3 4 5 80 syl3anc 
 |-  ( ph -> { I , J } ~~ 2o )
82 6 pmtrval 
 |-  ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> ( T ` { I , J } ) = ( x e. D |-> if ( x e. { I , J } , U. ( { I , J } \ { x } ) , x ) ) )
83 2 29 81 82 syl3anc 
 |-  ( ph -> ( T ` { I , J } ) = ( x e. D |-> if ( x e. { I , J } , U. ( { I , J } \ { x } ) , x ) ) )
84 76 79 83 3eqtr4d 
 |-  ( ph -> ( C ` <" I J "> ) = ( T ` { I , J } ) )