Theorem cycpmgcl

Description: Cyclic permutations are permutations, similar to cycpmcl , but where the set of cyclic permutations of length P is expressed in terms of a preimage. (Contributed by Thierry Arnoux, 13-Oct-2023)

	Ref	Expression
Hypotheses	cycpmconjs.c	⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) )
	cycpmconjs.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	cycpmconjs.n	⊢ 𝑁 = ( ♯ ‘ 𝐷 )
	cycpmconjs.m	⊢ 𝑀 = ( toCyc ‘ 𝐷 )
	cycpmgcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	cycpmgcl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cycpmconjs.c	⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) )
2		cycpmconjs.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3		cycpmconjs.n	⊢ 𝑁 = ( ♯ ‘ 𝐷 )
4		cycpmconjs.m	⊢ 𝑀 = ( toCyc ‘ 𝐷 )
5		cycpmgcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
6		simpr	⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑝 ) → ( 𝑀 ‘ 𝑢 ) = 𝑝 )
7		simplll	⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) → 𝐷 ∈ 𝑉 )
8		simpr	⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) → 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) )
9	8	elin1d	⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) → 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
10		elrabi	⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } → 𝑢 ∈ Word 𝐷 )
11	9 10	syl	⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) → 𝑢 ∈ Word 𝐷 )
12		id	⊢ ( 𝑤 = 𝑢 → 𝑤 = 𝑢 )
13		dmeq	⊢ ( 𝑤 = 𝑢 → dom 𝑤 = dom 𝑢 )
14		eqidd	⊢ ( 𝑤 = 𝑢 → 𝐷 = 𝐷 )
15	12 13 14	f1eq123d	⊢ ( 𝑤 = 𝑢 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
16	15	elrab	⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
17	16	simprbi	⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } → 𝑢 : dom 𝑢 –1-1→ 𝐷 )
18	9 17	syl	⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) → 𝑢 : dom 𝑢 –1-1→ 𝐷 )
19	4 7 11 18 2	cycpmcl	⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) → ( 𝑀 ‘ 𝑢 ) ∈ ( Base ‘ 𝑆 ) )
20	19	adantr	⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑝 ) → ( 𝑀 ‘ 𝑢 ) ∈ ( Base ‘ 𝑆 ) )
21	20 5	eleqtrrdi	⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑝 ) → ( 𝑀 ‘ 𝑢 ) ∈ 𝐵 )
22	6 21	eqeltrrd	⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ) ∧ ( 𝑀 ‘ 𝑢 ) = 𝑝 ) → 𝑝 ∈ 𝐵 )
23		nfcv	⊢ Ⅎ 𝑢 𝑀
24		simpl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → 𝐷 ∈ 𝑉 )
25	4 2 5	tocycf	⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 )
26		ffn	⊢ ( 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
27	24 25 26	3syl	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
28	27	adantr	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) → 𝑀 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
29	1	eleq2i	⊢ ( 𝑝 ∈ 𝐶 ↔ 𝑝 ∈ ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) ) )
30	29	a1i	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → ( 𝑝 ∈ 𝐶 ↔ 𝑝 ∈ ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) ) ) )
31	30	biimpa	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) → 𝑝 ∈ ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) ) )
32	23 28 31	fvelimad	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) → ∃ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ∩ ( ◡ ♯ “ { 𝑃 } ) ) ( 𝑀 ‘ 𝑢 ) = 𝑝 )
33	22 32	r19.29a	⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑝 ∈ 𝐶 ) → 𝑝 ∈ 𝐵 )
34	33	ex	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → ( 𝑝 ∈ 𝐶 → 𝑝 ∈ 𝐵 ) )
35	34	ssrdv	⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ⊆ 𝐵 )