cycpmconjv

Description: A formula for computing conjugacy classes of cyclic permutations. Formula in property (b) of Lang p. 32. (Contributed by Thierry Arnoux, 9-Oct-2023)

	Ref	Expression
Hypotheses	cycpmconjv.s	$⊢ S = SymGrp (D)$
	cycpmconjv.m	$⊢ M = toCyc (D)$
	cycpmconjv.p	$⊢ \underset{˙}{+} = +_{S}$
	cycpmconjv.l	$⊢ \underset{˙}{-} = -_{S}$
	cycpmconjv.b	$⊢ B = {Base}_{S}$
Assertion	cycpmconjv	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = M (G \circ W)$

Proof

Step	Hyp	Ref	Expression
1		cycpmconjv.s	$⊢ S = SymGrp (D)$
2		cycpmconjv.m	$⊢ M = toCyc (D)$
3		cycpmconjv.p	$⊢ \underset{˙}{+} = +_{S}$
4		cycpmconjv.l	$⊢ \underset{˙}{-} = -_{S}$
5		cycpmconjv.b	$⊢ B = {Base}_{S}$
6	1 5	symgbasf1o	$⊢ G \in B \to G : D \underset{1-1 onto}{⟶} D$
7	6	3ad2ant2	$⊢ (D \in V \land G \in B \land W \in dom M) \to G : D \underset{1-1 onto}{⟶} D$
8		simp3	$⊢ (D \in V \land G \in B \land W \in dom M) \to W \in dom M$
9	2 1 5	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ B$
10	9	3ad2ant1	$⊢ (D \in V \land G \in B \land W \in dom M) \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ B$
11	10	fdmd	$⊢ (D \in V \land G \in B \land W \in dom M) \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
12	8 11	eleqtrd	$⊢ (D \in V \land G \in B \land W \in dom M) \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
13		id	$⊢ w = W \to w = W$
14		dmeq	$⊢ w = W \to dom w = dom W$
15		eqidd	$⊢ w = W \to D = D$
16	13 14 15	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
17	16	elrab	$⊢ W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
18	12 17	sylib	$⊢ (D \in V \land G \in B \land W \in dom M) \to (W \in Word D \land W : dom W \underset{1-1}{⟶} D)$
19	18	simprd	$⊢ (D \in V \land G \in B \land W \in dom M) \to W : dom W \underset{1-1}{⟶} D$
20		f1f	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W ⟶ D$
21	19 20	syl	$⊢ (D \in V \land G \in B \land W \in dom M) \to W : dom W ⟶ D$
22	21	frnd	$⊢ (D \in V \land G \in B \land W \in dom M) \to ran W \subseteq D$
23	7 22	cycpmconjvlem	$⊢ (D \in V \land G \in B \land W \in dom M) \to ({G ↾}_{(D ∖ ran W)}) \circ G^{-1} = {I ↾}_{(D ∖ ran ({G ↾}_{ran W}))}$
24		rnco	$⊢ ran (G \circ W) = ran ({G ↾}_{ran W})$
25	24	difeq2i	$⊢ D ∖ ran (G \circ W) = D ∖ ran ({G ↾}_{ran W})$
26	25	reseq2i	$⊢ {I ↾}_{(D ∖ ran (G \circ W))} = {I ↾}_{(D ∖ ran ({G ↾}_{ran W}))}$
27	23 26	eqtr4di	$⊢ (D \in V \land G \in B \land W \in dom M) \to ({G ↾}_{(D ∖ ran W)}) \circ G^{-1} = {I ↾}_{(D ∖ ran (G \circ W))}$
28		coass	$⊢ (((G \circ W) cyclShift 1) \circ W^{-1}) \circ G^{-1} = ((G \circ W) cyclShift 1) \circ (W^{-1} \circ G^{-1})$
29		cnvco	$⊢ {(G \circ W)}^{-1} = W^{-1} \circ G^{-1}$
30	29	coeq2i	$⊢ ((G \circ W) cyclShift 1) \circ {(G \circ W)}^{-1} = ((G \circ W) cyclShift 1) \circ (W^{-1} \circ G^{-1})$
31	28 30	eqtr4i	$⊢ (((G \circ W) cyclShift 1) \circ W^{-1}) \circ G^{-1} = ((G \circ W) cyclShift 1) \circ {(G \circ W)}^{-1}$
32	31	a1i	$⊢ (D \in V \land G \in B \land W \in dom M) \to (((G \circ W) cyclShift 1) \circ W^{-1}) \circ G^{-1} = ((G \circ W) cyclShift 1) \circ {(G \circ W)}^{-1}$
33	27 32	uneq12d	$⊢ (D \in V \land G \in B \land W \in dom M) \to (({G ↾}_{(D ∖ ran W)}) \circ G^{-1}) \cup ((((G \circ W) cyclShift 1) \circ W^{-1}) \circ G^{-1}) = ({I ↾}_{(D ∖ ran (G \circ W))}) \cup (((G \circ W) cyclShift 1) \circ {(G \circ W)}^{-1})$
34		simp2	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \in B$
35	10 12	ffvelcdmd	$⊢ (D \in V \land G \in B \land W \in dom M) \to M (W) \in B$
36	1 5 3	symgcl	$⊢ (G \in B \land M (W) \in B) \to G \underset{˙}{+} M (W) \in B$
37	34 35 36	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \underset{˙}{+} M (W) \in B$
38		eqid	$⊢ {inv}_{g} (S) = {inv}_{g} (S)$
39	5 3 38 4	grpsubval	$⊢ (G \underset{˙}{+} M (W) \in B \land G \in B) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = (G \underset{˙}{+} M (W)) \underset{˙}{+} {inv}_{g} (S) (G)$
40	37 34 39	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = (G \underset{˙}{+} M (W)) \underset{˙}{+} {inv}_{g} (S) (G)$
41	1 5 38	symginv	$⊢ G \in B \to {inv}_{g} (S) (G) = G^{-1}$
42	41	3ad2ant2	$⊢ (D \in V \land G \in B \land W \in dom M) \to {inv}_{g} (S) (G) = G^{-1}$
43	42	oveq2d	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{+} {inv}_{g} (S) (G) = (G \underset{˙}{+} M (W)) \underset{˙}{+} G^{-1}$
44		simp1	$⊢ (D \in V \land G \in B \land W \in dom M) \to D \in V$
45		f1ocnv	$⊢ G : D \underset{1-1 onto}{⟶} D \to G^{-1} : D \underset{1-1 onto}{⟶} D$
46	7 45	syl	$⊢ (D \in V \land G \in B \land W \in dom M) \to G^{-1} : D \underset{1-1 onto}{⟶} D$
47	1 5	elsymgbas	$⊢ D \in V \to (G^{-1} \in B \leftrightarrow G^{-1} : D \underset{1-1 onto}{⟶} D)$
48	47	biimpar	$⊢ (D \in V \land G^{-1} : D \underset{1-1 onto}{⟶} D) \to G^{-1} \in B$
49	44 46 48	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to G^{-1} \in B$
50	1 5 3	symgov	$⊢ (G \underset{˙}{+} M (W) \in B \land G^{-1} \in B) \to (G \underset{˙}{+} M (W)) \underset{˙}{+} G^{-1} = (G \underset{˙}{+} M (W)) \circ G^{-1}$
51	37 49 50	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{+} G^{-1} = (G \underset{˙}{+} M (W)) \circ G^{-1}$
52	40 43 51	3eqtrd	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = (G \underset{˙}{+} M (W)) \circ G^{-1}$
53	1 5 3	symgov	$⊢ (G \in B \land M (W) \in B) \to G \underset{˙}{+} M (W) = G \circ M (W)$
54	34 35 53	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \underset{˙}{+} M (W) = G \circ M (W)$
55	18	simpld	$⊢ (D \in V \land G \in B \land W \in dom M) \to W \in Word D$
56	2 44 55 19	tocycfv	$⊢ (D \in V \land G \in B \land W \in dom M) \to M (W) = ({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})$
57	56	coeq2d	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \circ M (W) = G \circ (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1}))$
58		coundi	$⊢ G \circ (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) = (G \circ ({I ↾}_{(D ∖ ran W)})) \cup (G \circ ((W cyclShift 1) \circ W^{-1}))$
59	58	a1i	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \circ (({I ↾}_{(D ∖ ran W)}) \cup ((W cyclShift 1) \circ W^{-1})) = (G \circ ({I ↾}_{(D ∖ ran W)})) \cup (G \circ ((W cyclShift 1) \circ W^{-1}))$
60	54 57 59	3eqtrd	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \underset{˙}{+} M (W) = (G \circ ({I ↾}_{(D ∖ ran W)})) \cup (G \circ ((W cyclShift 1) \circ W^{-1}))$
61		coires1	$⊢ G \circ ({I ↾}_{(D ∖ ran W)}) = {G ↾}_{(D ∖ ran W)}$
62	61	a1i	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \circ ({I ↾}_{(D ∖ ran W)}) = {G ↾}_{(D ∖ ran W)}$
63		coass	$⊢ (G \circ (W cyclShift 1)) \circ W^{-1} = G \circ ((W cyclShift 1) \circ W^{-1})$
64		1zzd	$⊢ (D \in V \land G \in B \land W \in dom M) \to 1 \in ℤ$
65		f1of	$⊢ G : D \underset{1-1 onto}{⟶} D \to G : D ⟶ D$
66	7 65	syl	$⊢ (D \in V \land G \in B \land W \in dom M) \to G : D ⟶ D$
67		cshco	$⊢ (W \in Word D \land 1 \in ℤ \land G : D ⟶ D) \to G \circ (W cyclShift 1) = (G \circ W) cyclShift 1$
68	55 64 66 67	syl3anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \circ (W cyclShift 1) = (G \circ W) cyclShift 1$
69	68	coeq1d	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \circ (W cyclShift 1)) \circ W^{-1} = ((G \circ W) cyclShift 1) \circ W^{-1}$
70	63 69	eqtr3id	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \circ ((W cyclShift 1) \circ W^{-1}) = ((G \circ W) cyclShift 1) \circ W^{-1}$
71	62 70	uneq12d	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \circ ({I ↾}_{(D ∖ ran W)})) \cup (G \circ ((W cyclShift 1) \circ W^{-1})) = ({G ↾}_{(D ∖ ran W)}) \cup (((G \circ W) cyclShift 1) \circ W^{-1})$
72	60 71	eqtrd	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \underset{˙}{+} M (W) = ({G ↾}_{(D ∖ ran W)}) \cup (((G \circ W) cyclShift 1) \circ W^{-1})$
73	72	coeq1d	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \circ G^{-1} = (({G ↾}_{(D ∖ ran W)}) \cup (((G \circ W) cyclShift 1) \circ W^{-1})) \circ G^{-1}$
74	52 73	eqtrd	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = (({G ↾}_{(D ∖ ran W)}) \cup (((G \circ W) cyclShift 1) \circ W^{-1})) \circ G^{-1}$
75		coundir	$⊢ (({G ↾}_{(D ∖ ran W)}) \cup (((G \circ W) cyclShift 1) \circ W^{-1})) \circ G^{-1} = (({G ↾}_{(D ∖ ran W)}) \circ G^{-1}) \cup ((((G \circ W) cyclShift 1) \circ W^{-1}) \circ G^{-1})$
76	74 75	eqtrdi	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = (({G ↾}_{(D ∖ ran W)}) \circ G^{-1}) \cup ((((G \circ W) cyclShift 1) \circ W^{-1}) \circ G^{-1})$
77		wrdco	$⊢ (W \in Word D \land G : D ⟶ D) \to G \circ W \in Word D$
78	55 66 77	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to G \circ W \in Word D$
79		f1of1	$⊢ G : D \underset{1-1 onto}{⟶} D \to G : D \underset{1-1}{⟶} D$
80	7 79	syl	$⊢ (D \in V \land G \in B \land W \in dom M) \to G : D \underset{1-1}{⟶} D$
81		f1co	$⊢ (G : D \underset{1-1}{⟶} D \land W : dom W \underset{1-1}{⟶} D) \to (G \circ W) : dom W \underset{1-1}{⟶} D$
82	80 19 81	syl2anc	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \circ W) : dom W \underset{1-1}{⟶} D$
83	66	fdmd	$⊢ (D \in V \land G \in B \land W \in dom M) \to dom G = D$
84	22 83	sseqtrrd	$⊢ (D \in V \land G \in B \land W \in dom M) \to ran W \subseteq dom G$
85		dmcosseq	$⊢ ran W \subseteq dom G \to dom (G \circ W) = dom W$
86	84 85	syl	$⊢ (D \in V \land G \in B \land W \in dom M) \to dom (G \circ W) = dom W$
87		f1eq2	$⊢ dom (G \circ W) = dom W \to ((G \circ W) : dom (G \circ W) \underset{1-1}{⟶} D \leftrightarrow (G \circ W) : dom W \underset{1-1}{⟶} D)$
88	86 87	syl	$⊢ (D \in V \land G \in B \land W \in dom M) \to ((G \circ W) : dom (G \circ W) \underset{1-1}{⟶} D \leftrightarrow (G \circ W) : dom W \underset{1-1}{⟶} D)$
89	82 88	mpbird	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \circ W) : dom (G \circ W) \underset{1-1}{⟶} D$
90	2 44 78 89	tocycfv	$⊢ (D \in V \land G \in B \land W \in dom M) \to M (G \circ W) = ({I ↾}_{(D ∖ ran (G \circ W))}) \cup (((G \circ W) cyclShift 1) \circ {(G \circ W)}^{-1})$
91	33 76 90	3eqtr4d	$⊢ (D \in V \land G \in B \land W \in dom M) \to (G \underset{˙}{+} M (W)) \underset{˙}{-} G = M (G \circ W)$

Metamath Proof Explorer

Theorem cycpmconjv

Proof