Theorem cycpmco2rn

Description: The orbit of the composition of a cyclic permutation and a well-chosen transposition is one element more than the orbit of the original permutation. (Contributed by Thierry Arnoux, 4-Jan-2024)

	Ref	Expression
Hypotheses	cycpmco2.c	|- M = ( toCyc ` D )
	cycpmco2.s	|- S = ( SymGrp ` D )
	cycpmco2.d	|- ( ph -> D e. V )
	cycpmco2.w	|- ( ph -> W e. dom M )
	cycpmco2.i	|- ( ph -> I e. ( D \ ran W ) )
	cycpmco2.j	|- ( ph -> J e. ran W )
	cycpmco2.e	|- E = ( ( `' W ` J ) + 1 )
	cycpmco2.1	|- U = ( W splice <. E , E , <" I "> >. )
Assertion	cycpmco2rn	|- ( ph -> ran U = ( ran W u. { I } ) )

Proof

Step	Hyp	Ref	Expression
1		cycpmco2.c	|- M = ( toCyc ` D )
2		cycpmco2.s	|- S = ( SymGrp ` D )
3		cycpmco2.d	|- ( ph -> D e. V )
4		cycpmco2.w	|- ( ph -> W e. dom M )
5		cycpmco2.i	|- ( ph -> I e. ( D \ ran W ) )
6		cycpmco2.j	|- ( ph -> J e. ran W )
7		cycpmco2.e	|- E = ( ( `' W ` J ) + 1 )
8		cycpmco2.1	|- U = ( W splice <. E , E , <" I "> >. )
9		un23	|- ( ( ( W " ( 0 ..^ E ) ) u. { I } ) u. ( W " ( E ..^ ( # ` W ) ) ) ) = ( ( ( W " ( 0 ..^ E ) ) u. ( W " ( E ..^ ( # ` W ) ) ) ) u. { I } )
10		ovexd	|- ( ph -> ( ( `' W ` J ) + 1 ) e. _V )
11	7 10	eqeltrid	|- ( ph -> E e. _V )
12	5	eldifad	|- ( ph -> I e. D )
13	12	s1cld	|- ( ph -> <" I "> e. Word D )
14		splval	|- ( ( W e. dom M /\ ( E e. _V /\ E e. _V /\ <" I "> e. Word D ) ) -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
15	4 11 11 13 14	syl13anc	|- ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
16	8 15	syl5eq	|- ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
17	16	rneqd	|- ( ph -> ran U = ran ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) )
18		ssrab2	|- { w e. Word D | w : dom w -1-1-> D } C_ Word D
19		eqid	|- ( Base ` S ) = ( Base ` S )
20	1 2 19	tocycf	|- ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
21	3 20	syl	|- ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
22	21	fdmd	|- ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } )
23	4 22	eleqtrd	|- ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } )
24	18 23	sseldi	|- ( ph -> W e. Word D )
25		pfxcl	|- ( W e. Word D -> ( W prefix E ) e. Word D )
26	24 25	syl	|- ( ph -> ( W prefix E ) e. Word D )
27		ccatcl	|- ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
28	26 13 27	syl2anc	|- ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D )
29		swrdcl	|- ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
30	24 29	syl	|- ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D )
31		ccatrn	|- ( ( ( ( W prefix E ) ++ <" I "> ) e. Word D /\ ( W substr <. E , ( # ` W ) >. ) e. Word D ) -> ran ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) = ( ran ( ( W prefix E ) ++ <" I "> ) u. ran ( W substr <. E , ( # ` W ) >. ) ) )
32	28 30 31	syl2anc	|- ( ph -> ran ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) = ( ran ( ( W prefix E ) ++ <" I "> ) u. ran ( W substr <. E , ( # ` W ) >. ) ) )
33		ccatrn	|- ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ran ( ( W prefix E ) ++ <" I "> ) = ( ran ( W prefix E ) u. ran <" I "> ) )
34	26 13 33	syl2anc	|- ( ph -> ran ( ( W prefix E ) ++ <" I "> ) = ( ran ( W prefix E ) u. ran <" I "> ) )
35		id	|- ( w = W -> w = W )
36		dmeq	|- ( w = W -> dom w = dom W )
37		eqidd	|- ( w = W -> D = D )
38	35 36 37	f1eq123d	|- ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) )
39	38	elrab	|- ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) )
40	23 39	sylib	|- ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) )
41	40	simprd	|- ( ph -> W : dom W -1-1-> D )
42		f1cnv	|- ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W )
43		f1of	|- ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W )
44	41 42 43	3syl	|- ( ph -> `' W : ran W --> dom W )
45	44 6	ffvelrnd	|- ( ph -> ( `' W ` J ) e. dom W )
46		wrddm	|- ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) )
47	24 46	syl	|- ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
48	45 47	eleqtrd	|- ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) )
49		fzofzp1	|- ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
50	48 49	syl	|- ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) )
51	7 50	eqeltrid	|- ( ph -> E e. ( 0 ... ( # ` W ) ) )
52		pfxrn3	|- ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix E ) = ( W " ( 0 ..^ E ) ) )
53	24 51 52	syl2anc	|- ( ph -> ran ( W prefix E ) = ( W " ( 0 ..^ E ) ) )
54		s1rn	|- ( I e. D -> ran <" I "> = { I } )
55	12 54	syl	|- ( ph -> ran <" I "> = { I } )
56	53 55	uneq12d	|- ( ph -> ( ran ( W prefix E ) u. ran <" I "> ) = ( ( W " ( 0 ..^ E ) ) u. { I } ) )
57	34 56	eqtrd	|- ( ph -> ran ( ( W prefix E ) ++ <" I "> ) = ( ( W " ( 0 ..^ E ) ) u. { I } ) )
58		lencl	|- ( W e. Word D -> ( # ` W ) e. NN0 )
59		nn0fz0	|- ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
60	59	biimpi	|- ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
61	24 58 60	3syl	|- ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
62		swrdrn3	|- ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. E , ( # ` W ) >. ) = ( W " ( E ..^ ( # ` W ) ) ) )
63	24 51 61 62	syl3anc	|- ( ph -> ran ( W substr <. E , ( # ` W ) >. ) = ( W " ( E ..^ ( # ` W ) ) ) )
64	57 63	uneq12d	|- ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) u. ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ( W " ( 0 ..^ E ) ) u. { I } ) u. ( W " ( E ..^ ( # ` W ) ) ) ) )
65	17 32 64	3eqtrd	|- ( ph -> ran U = ( ( ( W " ( 0 ..^ E ) ) u. { I } ) u. ( W " ( E ..^ ( # ` W ) ) ) ) )
66		fzosplit	|- ( E e. ( 0 ... ( # ` W ) ) -> ( 0 ..^ ( # ` W ) ) = ( ( 0 ..^ E ) u. ( E ..^ ( # ` W ) ) ) )
67	51 66	syl	|- ( ph -> ( 0 ..^ ( # ` W ) ) = ( ( 0 ..^ E ) u. ( E ..^ ( # ` W ) ) ) )
68	67	imaeq2d	|- ( ph -> ( W " ( 0 ..^ ( # ` W ) ) ) = ( W " ( ( 0 ..^ E ) u. ( E ..^ ( # ` W ) ) ) ) )
69		wrdf	|- ( W e. Word D -> W : ( 0 ..^ ( # ` W ) ) --> D )
70	24 69	syl	|- ( ph -> W : ( 0 ..^ ( # ` W ) ) --> D )
71	70	ffnd	|- ( ph -> W Fn ( 0 ..^ ( # ` W ) ) )
72		fnima	|- ( W Fn ( 0 ..^ ( # ` W ) ) -> ( W " ( 0 ..^ ( # ` W ) ) ) = ran W )
73	71 72	syl	|- ( ph -> ( W " ( 0 ..^ ( # ` W ) ) ) = ran W )
74		elfzuz3	|- ( E e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` E ) )
75		fzoss2	|- ( ( # ` W ) e. ( ZZ>= ` E ) -> ( 0 ..^ E ) C_ ( 0 ..^ ( # ` W ) ) )
76	51 74 75	3syl	|- ( ph -> ( 0 ..^ E ) C_ ( 0 ..^ ( # ` W ) ) )
77		fz0ssnn0	|- ( 0 ... ( # ` W ) ) C_ NN0
78	77 51	sseldi	|- ( ph -> E e. NN0 )
79		nn0uz	|- NN0 = ( ZZ>= ` 0 )
80	78 79	eleqtrdi	|- ( ph -> E e. ( ZZ>= ` 0 ) )
81		fzoss1	|- ( E e. ( ZZ>= ` 0 ) -> ( E ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) )
82	80 81	syl	|- ( ph -> ( E ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) )
83		unima	|- ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ ( 0 ..^ E ) C_ ( 0 ..^ ( # ` W ) ) /\ ( E ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) ) ) -> ( W " ( ( 0 ..^ E ) u. ( E ..^ ( # ` W ) ) ) ) = ( ( W " ( 0 ..^ E ) ) u. ( W " ( E ..^ ( # ` W ) ) ) ) )
84	71 76 82 83	syl3anc	|- ( ph -> ( W " ( ( 0 ..^ E ) u. ( E ..^ ( # ` W ) ) ) ) = ( ( W " ( 0 ..^ E ) ) u. ( W " ( E ..^ ( # ` W ) ) ) ) )
85	68 73 84	3eqtr3d	|- ( ph -> ran W = ( ( W " ( 0 ..^ E ) ) u. ( W " ( E ..^ ( # ` W ) ) ) ) )
86	85	uneq1d	|- ( ph -> ( ran W u. { I } ) = ( ( ( W " ( 0 ..^ E ) ) u. ( W " ( E ..^ ( # ` W ) ) ) ) u. { I } ) )
87	9 65 86	3eqtr4a	|- ( ph -> ran U = ( ran W u. { I } ) )