symgcntz

Description: All elements of a (finite) set of permutations commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Hypotheses	symgcntz.s	$⊢ S = SymGrp (D)$
	symgcntz.b	$⊢ B = {Base}_{S}$
	symgcntz.z	$⊢ Z = Cntz (S)$
	symgcntz.a	$⊢ φ \to A \subseteq B$
	symgcntz.1	$⊢ φ \to \underset{x \in A}{Disj} dom (x ∖ I)$
Assertion	symgcntz	$⊢ φ \to A \subseteq Z (A)$

Proof

Step	Hyp	Ref	Expression
1		symgcntz.s	$⊢ S = SymGrp (D)$
2		symgcntz.b	$⊢ B = {Base}_{S}$
3		symgcntz.z	$⊢ Z = Cntz (S)$
4		symgcntz.a	$⊢ φ \to A \subseteq B$
5		symgcntz.1	$⊢ φ \to \underset{x \in A}{Disj} dom (x ∖ I)$
6		simpr	$⊢ ((φ \land (c \in A \land d \in A)) \land c = d) \to c = d$
7	6	oveq1d	$⊢ ((φ \land (c \in A \land d \in A)) \land c = d) \to c +_{S} d = d +_{S} d$
8	6	oveq2d	$⊢ ((φ \land (c \in A \land d \in A)) \land c = d) \to d +_{S} c = d +_{S} d$
9	7 8	eqtr4d	$⊢ ((φ \land (c \in A \land d \in A)) \land c = d) \to c +_{S} d = d +_{S} c$
10	4	ad2antrr	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to A \subseteq B$
11		simplrl	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to c \in A$
12	10 11	sseldd	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to c \in B$
13		simplrr	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to d \in A$
14	10 13	sseldd	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to d \in B$
15	5	ad2antrr	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to \underset{x \in A}{Disj} dom (x ∖ I)$
16		simpr	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to c \neq d$
17		difeq1	$⊢ x = c \to x ∖ I = c ∖ I$
18	17	dmeqd	$⊢ x = c \to dom (x ∖ I) = dom (c ∖ I)$
19		difeq1	$⊢ x = d \to x ∖ I = d ∖ I$
20	19	dmeqd	$⊢ x = d \to dom (x ∖ I) = dom (d ∖ I)$
21	18 20	disji2	$⊢ (\underset{x \in A}{Disj} dom (x ∖ I) \land (c \in A \land d \in A) \land c \neq d) \to dom (c ∖ I) \cap dom (d ∖ I) = \emptyset$
22	15 11 13 16 21	syl121anc	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to dom (c ∖ I) \cap dom (d ∖ I) = \emptyset$
23	1 2 12 14 22	symgcom2	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to c \circ d = d \circ c$
24		eqid	$⊢ +_{S} = +_{S}$
25	1 2 24	symgov	$⊢ (c \in B \land d \in B) \to c +_{S} d = c \circ d$
26	12 14 25	syl2anc	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to c +_{S} d = c \circ d$
27	1 2 24	symgov	$⊢ (d \in B \land c \in B) \to d +_{S} c = d \circ c$
28	14 12 27	syl2anc	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to d +_{S} c = d \circ c$
29	23 26 28	3eqtr4d	$⊢ ((φ \land (c \in A \land d \in A)) \land c \neq d) \to c +_{S} d = d +_{S} c$
30	9 29	pm2.61dane	$⊢ (φ \land (c \in A \land d \in A)) \to c +_{S} d = d +_{S} c$
31	30	ralrimivva	$⊢ φ \to \forall c \in A \forall d \in A c +_{S} d = d +_{S} c$
32	2 24 3	sscntz	$⊢ (A \subseteq B \land A \subseteq B) \to (A \subseteq Z (A) \leftrightarrow \forall c \in A \forall d \in A c +_{S} d = d +_{S} c)$
33	4 4 32	syl2anc	$⊢ φ \to (A \subseteq Z (A) \leftrightarrow \forall c \in A \forall d \in A c +_{S} d = d +_{S} c)$
34	31 33	mpbird	$⊢ φ \to A \subseteq Z (A)$

Metamath Proof Explorer

Theorem symgcntz

Proof