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	$⊢ C = M [{\|.\|}^{-1} [\{P\}]]$
	cycpmconjs.s	$⊢ S = SymGrp (D)$
	cycpmconjs.n	$⊢ N = \|D\|$
	cycpmconjs.m	$⊢ M = toCyc (D)$
	cycpmgcl.b	$⊢ B = {Base}_{S}$
Assertion	cycpmgcl	$⊢ (D \in V \land P \in (0 \dots N)) \to C \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		cycpmconjs.c	$⊢ C = M [{\|.\|}^{-1} [\{P\}]]$
2		cycpmconjs.s	$⊢ S = SymGrp (D)$
3		cycpmconjs.n	$⊢ N = \|D\|$
4		cycpmconjs.m	$⊢ M = toCyc (D)$
5		cycpmgcl.b	$⊢ B = {Base}_{S}$
6		simpr	$⊢ ((((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \land M (u) = p) \to M (u) = p$
7		simplll	$⊢ (((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \to D \in V$
8		simpr	$⊢ (((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \to u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])$
9	8	elin1d	$⊢ (((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \to u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
10		elrabi	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \to u \in Word D$
11	9 10	syl	$⊢ (((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \to u \in Word D$
12		id	$⊢ w = u \to w = u$
13		dmeq	$⊢ w = u \to dom w = dom u$
14		eqidd	$⊢ w = u \to D = D$
15	12 13 14	f1eq123d	$⊢ w = u \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow u : dom u \underset{1-1}{⟶} D)$
16	15	elrab	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow (u \in Word D \land u : dom u \underset{1-1}{⟶} D)$
17	16	simprbi	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \to u : dom u \underset{1-1}{⟶} D$
18	9 17	syl	$⊢ (((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \to u : dom u \underset{1-1}{⟶} D$
19	4 7 11 18 2	cycpmcl	$⊢ (((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \to M (u) \in {Base}_{S}$
20	19	adantr	$⊢ ((((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \land M (u) = p) \to M (u) \in {Base}_{S}$
21	20 5	eleqtrrdi	$⊢ ((((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \land M (u) = p) \to M (u) \in B$
22	6 21	eqeltrrd	$⊢ ((((D \in V \land P \in (0 \dots N)) \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}])) \land M (u) = p) \to p \in B$
23		nfcv	$⊢ \underline{Ⅎ} u M$
24		simpl	$⊢ (D \in V \land P \in (0 \dots N)) \to D \in V$
25	4 2 5	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ B$
26		ffn	$⊢ M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ B \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
27	24 25 26	3syl	$⊢ (D \in V \land P \in (0 \dots N)) \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
28	27	adantr	$⊢ ((D \in V \land P \in (0 \dots N)) \land p \in C) \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
29	1	eleq2i	$⊢ p \in C \leftrightarrow p \in M [{\|.\|}^{-1} [\{P\}]]$
30	29	bilani	$⊢ ((D \in V \land P \in (0 \dots N)) \land p \in C) \to p \in M [{\|.\|}^{-1} [\{P\}]]$
31	23 28 30	fvelimad	$⊢ ((D \in V \land P \in (0 \dots N)) \land p \in C) \to \exists u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{P\}]) M (u) = p$
32	22 31	r19.29a	$⊢ ((D \in V \land P \in (0 \dots N)) \land p \in C) \to p \in B$
33	32	ex	$⊢ (D \in V \land P \in (0 \dots N)) \to (p \in C \to p \in B)$
34	33	ssrdv	$⊢ (D \in V \land P \in (0 \dots N)) \to C \subseteq B$

Metamath Proof Explorer

Theorem cycpmgcl

Proof