symgcom2

Description: Two permutations X and Y commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023)

	Ref	Expression
Hypotheses	symgcom.g	$⊢ G = SymGrp (A)$
	symgcom.b	$⊢ B = {Base}_{G}$
	symgcom.x	$⊢ φ \to X \in B$
	symgcom.y	$⊢ φ \to Y \in B$
	symgcom2.1	$⊢ φ \to dom (X ∖ I) \cap dom (Y ∖ I) = \emptyset$
Assertion	symgcom2	$⊢ φ \to X \circ Y = Y \circ X$

Proof

Step	Hyp	Ref	Expression
1		symgcom.g	$⊢ G = SymGrp (A)$
2		symgcom.b	$⊢ B = {Base}_{G}$
3		symgcom.x	$⊢ φ \to X \in B$
4		symgcom.y	$⊢ φ \to Y \in B$
5		symgcom2.1	$⊢ φ \to dom (X ∖ I) \cap dom (Y ∖ I) = \emptyset$
6	1 2	symgbasf	$⊢ X \in B \to X : A ⟶ A$
7	3 6	syl	$⊢ φ \to X : A ⟶ A$
8	7	ffnd	$⊢ φ \to X Fn A$
9		fnresi	$⊢ ({I ↾}_{A}) Fn A$
10	9	a1i	$⊢ φ \to ({I ↾}_{A}) Fn A$
11		difssd	$⊢ φ \to A ∖ dom (X ∖ I) \subseteq A$
12		ssidd	$⊢ φ \to A ∖ dom (X ∖ I) \subseteq A ∖ dom (X ∖ I)$
13		nfpconfp	$⊢ X Fn A \to A ∖ dom (X ∖ I) = dom (X \cap I)$
14	8 13	syl	$⊢ φ \to A ∖ dom (X ∖ I) = dom (X \cap I)$
15		inres	$⊢ X \cap ({I ↾}_{A}) = {(X \cap I) ↾}_{A}$
16		reli	$⊢ Rel I$
17		relin2	$⊢ Rel I \to Rel (X \cap I)$
18	16 17	ax-mp	$⊢ Rel (X \cap I)$
19	14 11	eqsstrrd	$⊢ φ \to dom (X \cap I) \subseteq A$
20		relssres	$⊢ (Rel (X \cap I) \land dom (X \cap I) \subseteq A) \to {(X \cap I) ↾}_{A} = X \cap I$
21	18 19 20	sylancr	$⊢ φ \to {(X \cap I) ↾}_{A} = X \cap I$
22	15 21	syl5eq	$⊢ φ \to X \cap ({I ↾}_{A}) = X \cap I$
23	22	dmeqd	$⊢ φ \to dom (X \cap ({I ↾}_{A})) = dom (X \cap I)$
24	14 23	eqtr4d	$⊢ φ \to A ∖ dom (X ∖ I) = dom (X \cap ({I ↾}_{A}))$
25	12 24	sseqtrd	$⊢ φ \to A ∖ dom (X ∖ I) \subseteq dom (X \cap ({I ↾}_{A}))$
26		fnreseql	$⊢ (X Fn A \land ({I ↾}_{A}) Fn A \land A ∖ dom (X ∖ I) \subseteq A) \to ({X ↾}_{(A ∖ dom (X ∖ I))} = {({I ↾}_{A}) ↾}_{(A ∖ dom (X ∖ I))} \leftrightarrow A ∖ dom (X ∖ I) \subseteq dom (X \cap ({I ↾}_{A})))$
27	26	biimpar	$⊢ ((X Fn A \land ({I ↾}_{A}) Fn A \land A ∖ dom (X ∖ I) \subseteq A) \land A ∖ dom (X ∖ I) \subseteq dom (X \cap ({I ↾}_{A}))) \to {X ↾}_{(A ∖ dom (X ∖ I))} = {({I ↾}_{A}) ↾}_{(A ∖ dom (X ∖ I))}$
28	8 10 11 25 27	syl31anc	$⊢ φ \to {X ↾}_{(A ∖ dom (X ∖ I))} = {({I ↾}_{A}) ↾}_{(A ∖ dom (X ∖ I))}$
29	11	resabs1d	$⊢ φ \to {({I ↾}_{A}) ↾}_{(A ∖ dom (X ∖ I))} = {I ↾}_{(A ∖ dom (X ∖ I))}$
30	28 29	eqtrd	$⊢ φ \to {X ↾}_{(A ∖ dom (X ∖ I))} = {I ↾}_{(A ∖ dom (X ∖ I))}$
31	1 2	symgbasf	$⊢ Y \in B \to Y : A ⟶ A$
32	4 31	syl	$⊢ φ \to Y : A ⟶ A$
33	32	ffnd	$⊢ φ \to Y Fn A$
34		difss	$⊢ X ∖ I \subseteq X$
35		dmss	$⊢ X ∖ I \subseteq X \to dom (X ∖ I) \subseteq dom X$
36	34 35	ax-mp	$⊢ dom (X ∖ I) \subseteq dom X$
37		fdm	$⊢ X : A ⟶ A \to dom X = A$
38	3 6 37	3syl	$⊢ φ \to dom X = A$
39	36 38	sseqtrid	$⊢ φ \to dom (X ∖ I) \subseteq A$
40		reldisj	$⊢ dom (X ∖ I) \subseteq A \to (dom (X ∖ I) \cap dom (Y ∖ I) = \emptyset \leftrightarrow dom (X ∖ I) \subseteq A ∖ dom (Y ∖ I))$
41	39 40	syl	$⊢ φ \to (dom (X ∖ I) \cap dom (Y ∖ I) = \emptyset \leftrightarrow dom (X ∖ I) \subseteq A ∖ dom (Y ∖ I))$
42	5 41	mpbid	$⊢ φ \to dom (X ∖ I) \subseteq A ∖ dom (Y ∖ I)$
43		nfpconfp	$⊢ Y Fn A \to A ∖ dom (Y ∖ I) = dom (Y \cap I)$
44	33 43	syl	$⊢ φ \to A ∖ dom (Y ∖ I) = dom (Y \cap I)$
45	42 44	sseqtrd	$⊢ φ \to dom (X ∖ I) \subseteq dom (Y \cap I)$
46		inres	$⊢ Y \cap ({I ↾}_{A}) = {(Y \cap I) ↾}_{A}$
47		relin2	$⊢ Rel I \to Rel (Y \cap I)$
48	16 47	ax-mp	$⊢ Rel (Y \cap I)$
49		difssd	$⊢ φ \to A ∖ dom (Y ∖ I) \subseteq A$
50	44 49	eqsstrrd	$⊢ φ \to dom (Y \cap I) \subseteq A$
51		relssres	$⊢ (Rel (Y \cap I) \land dom (Y \cap I) \subseteq A) \to {(Y \cap I) ↾}_{A} = Y \cap I$
52	48 50 51	sylancr	$⊢ φ \to {(Y \cap I) ↾}_{A} = Y \cap I$
53	46 52	syl5eq	$⊢ φ \to Y \cap ({I ↾}_{A}) = Y \cap I$
54	53	dmeqd	$⊢ φ \to dom (Y \cap ({I ↾}_{A})) = dom (Y \cap I)$
55	45 54	sseqtrrd	$⊢ φ \to dom (X ∖ I) \subseteq dom (Y \cap ({I ↾}_{A}))$
56		fnreseql	$⊢ (Y Fn A \land ({I ↾}_{A}) Fn A \land dom (X ∖ I) \subseteq A) \to ({Y ↾}_{dom (X ∖ I)} = {({I ↾}_{A}) ↾}_{dom (X ∖ I)} \leftrightarrow dom (X ∖ I) \subseteq dom (Y \cap ({I ↾}_{A})))$
57	56	biimpar	$⊢ ((Y Fn A \land ({I ↾}_{A}) Fn A \land dom (X ∖ I) \subseteq A) \land dom (X ∖ I) \subseteq dom (Y \cap ({I ↾}_{A}))) \to {Y ↾}_{dom (X ∖ I)} = {({I ↾}_{A}) ↾}_{dom (X ∖ I)}$
58	33 10 39 55 57	syl31anc	$⊢ φ \to {Y ↾}_{dom (X ∖ I)} = {({I ↾}_{A}) ↾}_{dom (X ∖ I)}$
59	39	resabs1d	$⊢ φ \to {({I ↾}_{A}) ↾}_{dom (X ∖ I)} = {I ↾}_{dom (X ∖ I)}$
60	58 59	eqtrd	$⊢ φ \to {Y ↾}_{dom (X ∖ I)} = {I ↾}_{dom (X ∖ I)}$
61		difin2	$⊢ dom (X ∖ I) \subseteq A \to dom (X ∖ I) ∖ dom (X ∖ I) = (A ∖ dom (X ∖ I)) \cap dom (X ∖ I)$
62	39 61	syl	$⊢ φ \to dom (X ∖ I) ∖ dom (X ∖ I) = (A ∖ dom (X ∖ I)) \cap dom (X ∖ I)$
63		difid	$⊢ dom (X ∖ I) ∖ dom (X ∖ I) = \emptyset$
64	62 63	eqtr3di	$⊢ φ \to (A ∖ dom (X ∖ I)) \cap dom (X ∖ I) = \emptyset$
65		undif1	$⊢ (A ∖ dom (X ∖ I)) \cup dom (X ∖ I) = A \cup dom (X ∖ I)$
66		ssequn2	$⊢ dom (X ∖ I) \subseteq A \leftrightarrow A \cup dom (X ∖ I) = A$
67	39 66	sylib	$⊢ φ \to A \cup dom (X ∖ I) = A$
68	65 67	syl5eq	$⊢ φ \to (A ∖ dom (X ∖ I)) \cup dom (X ∖ I) = A$
69	1 2 3 4 30 60 64 68	symgcom	$⊢ φ \to X \circ Y = Y \circ X$

Metamath Proof Explorer

Theorem symgcom2

Proof