Theorem symgcom

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

	Ref	Expression
Hypotheses	symgcom.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgcom.b	$$⊢B={\mathrm{Base}}_G$$
	symgcom.x	$$⊢\phi \to X\in B$$
	symgcom.y	$$⊢\phi \to Y\in B$$
	symgcom.1	$$⊢\phi \to {X\upharpoonright }_E={\mathrm{I}\upharpoonright }_E$$
	symgcom.2	$$⊢\phi \to {Y\upharpoonright }_F={\mathrm{I}\upharpoonright }_F$$
	symgcom.3	$$⊢\phi \to E\cap F=\varnothing$$
	symgcom.4	$$⊢\phi \to E\cup F=A$$
Assertion	symgcom	$$⊢\phi \to X\circ Y=Y\circ X$$

Proof

Step	Hyp	Ref	Expression
1		symgcom.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgcom.b	$$⊢B={\mathrm{Base}}_G$$
3		symgcom.x	$$⊢\phi \to X\in B$$
4		symgcom.y	$$⊢\phi \to Y\in B$$
5		symgcom.1	$$⊢\phi \to {X\upharpoonright }_E={\mathrm{I}\upharpoonright }_E$$
6		symgcom.2	$$⊢\phi \to {Y\upharpoonright }_F={\mathrm{I}\upharpoonright }_F$$
7		symgcom.3	$$⊢\phi \to E\cap F=\varnothing$$
8		symgcom.4	$$⊢\phi \to E\cup F=A$$
9	8	reseq2d	$$⊢\phi \to {\left(X\circ Y\right)\upharpoonright }_{\left(E\cup F\right)}={\left(X\circ Y\right)\upharpoonright }_A$$
10		resundi	$$⊢{\left(X\circ Y\right)\upharpoonright }_{\left(E\cup F\right)}=\left({\left(X\circ Y\right)\upharpoonright }_E\right)\cup \left({\left(X\circ Y\right)\upharpoonright }_F\right)$$
11		resco	$$⊢{\left(X\circ Y\right)\upharpoonright }_E=X\circ \left({Y\upharpoonright }_E\right)$$
12	1 2	symgbasf1o	$$⊢Y\in B\to Y:A\underset{1-1\; onto}{⟶}A$$
13	4 12	syl	$$⊢\phi \to Y:A\underset{1-1\; onto}{⟶}A$$
14		f1ocnv	$$⊢Y:A\underset{1-1\; onto}{⟶}A\to Y^{-1}:A\underset{1-1\; onto}{⟶}A$$
15		f1ofun	$$⊢Y^{-1}:A\underset{1-1\; onto}{⟶}A\to \mathrm{Fun}{Y}^{-1}$$
16	13 14 15	3syl	$$⊢\phi \to \mathrm{Fun}{Y}^{-1}$$
17		f1ofn	$$⊢Y:A\underset{1-1\; onto}{⟶}A\to YFnA$$
18		fnresdm	$$⊢YFnA\to {Y\upharpoonright }_A=Y$$
19	13 17 18	3syl	$$⊢\phi \to {Y\upharpoonright }_A=Y$$
20		f1ofo	$$⊢Y:A\underset{1-1\; onto}{⟶}A\to Y:A\underset{onto}{⟶}A$$
21	13 20	syl	$$⊢\phi \to Y:A\underset{onto}{⟶}A$$
22		foeq1	$$⊢{Y\upharpoonright }_A=Y\to \left(\left({Y\upharpoonright }_A\right):A\underset{onto}{⟶}A\leftrightarrow Y:A\underset{onto}{⟶}A\right)$$
23	22	biimpar	$$⊢\left({Y\upharpoonright }_A=Y\wedge Y:A\underset{onto}{⟶}A\right)\to \left({Y\upharpoonright }_A\right):A\underset{onto}{⟶}A$$
24	19 21 23	syl2anc	$$⊢\phi \to \left({Y\upharpoonright }_A\right):A\underset{onto}{⟶}A$$
25		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_F\right):F\underset{1-1\; onto}{⟶}F$$
26		f1ofo	$$⊢\left({\mathrm{I}\upharpoonright }_F\right):F\underset{1-1\; onto}{⟶}F\to \left({\mathrm{I}\upharpoonright }_F\right):F\underset{onto}{⟶}F$$
27	25 26	mp1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_F\right):F\underset{onto}{⟶}F$$
28		foeq1	$$⊢{Y\upharpoonright }_F={\mathrm{I}\upharpoonright }_F\to \left(\left({Y\upharpoonright }_F\right):F\underset{onto}{⟶}F\leftrightarrow \left({\mathrm{I}\upharpoonright }_F\right):F\underset{onto}{⟶}F\right)$$
29	28	biimpar	$$⊢\left({Y\upharpoonright }_F={\mathrm{I}\upharpoonright }_F\wedge \left({\mathrm{I}\upharpoonright }_F\right):F\underset{onto}{⟶}F\right)\to \left({Y\upharpoonright }_F\right):F\underset{onto}{⟶}F$$
30	6 27 29	syl2anc	$$⊢\phi \to \left({Y\upharpoonright }_F\right):F\underset{onto}{⟶}F$$
31		resdif	$$⊢\left(\mathrm{Fun}{Y}^{-1}\wedge \left({Y\upharpoonright }_A\right):A\underset{onto}{⟶}A\wedge \left({Y\upharpoonright }_F\right):F\underset{onto}{⟶}F\right)\to \left({Y\upharpoonright }_{\left(A\setminus F\right)}\right):A\setminus F\underset{1-1\; onto}{⟶}A\setminus F$$
32	16 24 30 31	syl3anc	$$⊢\phi \to \left({Y\upharpoonright }_{\left(A\setminus F\right)}\right):A\setminus F\underset{1-1\; onto}{⟶}A\setminus F$$
33		ssun2	$$⊢F\subseteq E\cup F$$
34	33 8	sseqtrid	$$⊢\phi \to F\subseteq A$$
35		incom	$$⊢E\cap F=F\cap E$$
36	35 7	syl5eqr	$$⊢\phi \to F\cap E=\varnothing$$
37		uncom	$$⊢E\cup F=F\cup E$$
38	37 8	syl5eqr	$$⊢\phi \to F\cup E=A$$
39		uneqdifeq	$$⊢\left(F\subseteq A\wedge F\cap E=\varnothing \right)\to \left(F\cup E=A\leftrightarrow A\setminus F=E\right)$$
40	39	biimpa	$$⊢\left(\left(F\subseteq A\wedge F\cap E=\varnothing \right)\wedge F\cup E=A\right)\to A\setminus F=E$$
41	34 36 38 40	syl21anc	$$⊢\phi \to A\setminus F=E$$
42	41	reseq2d	$$⊢\phi \to {Y\upharpoonright }_{\left(A\setminus F\right)}={Y\upharpoonright }_E$$
43	42 41 41	f1oeq123d	$$⊢\phi \to \left(\left({Y\upharpoonright }_{\left(A\setminus F\right)}\right):A\setminus F\underset{1-1\; onto}{⟶}A\setminus F\leftrightarrow \left({Y\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E\right)$$
44	32 43	mpbid	$$⊢\phi \to \left({Y\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E$$
45		f1of	$$⊢\left({Y\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E\to \left({Y\upharpoonright }_E\right):E⟶E$$
46	44 45	syl	$$⊢\phi \to \left({Y\upharpoonright }_E\right):E⟶E$$
47	46	frnd	$$⊢\phi \to \mathrm{ran}\left({Y\upharpoonright }_E\right)\subseteq E$$
48		cores	$$⊢\mathrm{ran}\left({Y\upharpoonright }_E\right)\subseteq E\to \left({X\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)=X\circ \left({Y\upharpoonright }_E\right)$$
49	47 48	syl	$$⊢\phi \to \left({X\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)=X\circ \left({Y\upharpoonright }_E\right)$$
50	11 49	eqtr4id	$$⊢\phi \to {\left(X\circ Y\right)\upharpoonright }_E=\left({X\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)$$
51	5	coeq1d	$$⊢\phi \to \left({X\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)=\left({\mathrm{I}\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)$$
52		fcoi2	$$⊢\left({Y\upharpoonright }_E\right):E⟶E\to \left({\mathrm{I}\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)={Y\upharpoonright }_E$$
53	46 52	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_E\right)\circ \left({Y\upharpoonright }_E\right)={Y\upharpoonright }_E$$
54	50 51 53	3eqtrd	$$⊢\phi \to {\left(X\circ Y\right)\upharpoonright }_E={Y\upharpoonright }_E$$
55		resco	$$⊢{\left(X\circ Y\right)\upharpoonright }_F=X\circ \left({Y\upharpoonright }_F\right)$$
56	6	coeq2d	$$⊢\phi \to X\circ \left({Y\upharpoonright }_F\right)=X\circ \left({\mathrm{I}\upharpoonright }_F\right)$$
57		coires1	$$⊢X\circ \left({\mathrm{I}\upharpoonright }_F\right)={X\upharpoonright }_F$$
58	56 57	eqtrdi	$$⊢\phi \to X\circ \left({Y\upharpoonright }_F\right)={X\upharpoonright }_F$$
59	55 58	syl5eq	$$⊢\phi \to {\left(X\circ Y\right)\upharpoonright }_F={X\upharpoonright }_F$$
60	54 59	uneq12d	$$⊢\phi \to \left({\left(X\circ Y\right)\upharpoonright }_E\right)\cup \left({\left(X\circ Y\right)\upharpoonright }_F\right)=\left({Y\upharpoonright }_E\right)\cup \left({X\upharpoonright }_F\right)$$
61	10 60	syl5eq	$$⊢\phi \to {\left(X\circ Y\right)\upharpoonright }_{\left(E\cup F\right)}=\left({Y\upharpoonright }_E\right)\cup \left({X\upharpoonright }_F\right)$$
62	1 2	symgbasf1o	$$⊢X\in B\to X:A\underset{1-1\; onto}{⟶}A$$
63	3 62	syl	$$⊢\phi \to X:A\underset{1-1\; onto}{⟶}A$$
64		f1oco	$$⊢\left(X:A\underset{1-1\; onto}{⟶}A\wedge Y:A\underset{1-1\; onto}{⟶}A\right)\to \left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A$$
65	63 13 64	syl2anc	$$⊢\phi \to \left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A$$
66		f1ofn	$$⊢\left(X\circ Y\right):A\underset{1-1\; onto}{⟶}A\to \left(X\circ Y\right)FnA$$
67		fnresdm	$$⊢\left(X\circ Y\right)FnA\to {\left(X\circ Y\right)\upharpoonright }_A=X\circ Y$$
68	65 66 67	3syl	$$⊢\phi \to {\left(X\circ Y\right)\upharpoonright }_A=X\circ Y$$
69	9 61 68	3eqtr3d	$$⊢\phi \to \left({Y\upharpoonright }_E\right)\cup \left({X\upharpoonright }_F\right)=X\circ Y$$
70	8	reseq2d	$$⊢\phi \to {\left(Y\circ X\right)\upharpoonright }_{\left(E\cup F\right)}={\left(Y\circ X\right)\upharpoonright }_A$$
71		resundi	$$⊢{\left(Y\circ X\right)\upharpoonright }_{\left(E\cup F\right)}=\left({\left(Y\circ X\right)\upharpoonright }_E\right)\cup \left({\left(Y\circ X\right)\upharpoonright }_F\right)$$
72		resco	$$⊢{\left(Y\circ X\right)\upharpoonright }_E=Y\circ \left({X\upharpoonright }_E\right)$$
73	5	coeq2d	$$⊢\phi \to Y\circ \left({X\upharpoonright }_E\right)=Y\circ \left({\mathrm{I}\upharpoonright }_E\right)$$
74		coires1	$$⊢Y\circ \left({\mathrm{I}\upharpoonright }_E\right)={Y\upharpoonright }_E$$
75	73 74	eqtrdi	$$⊢\phi \to Y\circ \left({X\upharpoonright }_E\right)={Y\upharpoonright }_E$$
76	72 75	syl5eq	$$⊢\phi \to {\left(Y\circ X\right)\upharpoonright }_E={Y\upharpoonright }_E$$
77		resco	$$⊢{\left(Y\circ X\right)\upharpoonright }_F=Y\circ \left({X\upharpoonright }_F\right)$$
78		f1ocnv	$$⊢X:A\underset{1-1\; onto}{⟶}A\to X^{-1}:A\underset{1-1\; onto}{⟶}A$$
79		f1ofun	$$⊢X^{-1}:A\underset{1-1\; onto}{⟶}A\to \mathrm{Fun}{X}^{-1}$$
80	63 78 79	3syl	$$⊢\phi \to \mathrm{Fun}{X}^{-1}$$
81		f1ofn	$$⊢X:A\underset{1-1\; onto}{⟶}A\to XFnA$$
82		fnresdm	$$⊢XFnA\to {X\upharpoonright }_A=X$$
83	63 81 82	3syl	$$⊢\phi \to {X\upharpoonright }_A=X$$
84		f1ofo	$$⊢X:A\underset{1-1\; onto}{⟶}A\to X:A\underset{onto}{⟶}A$$
85	63 84	syl	$$⊢\phi \to X:A\underset{onto}{⟶}A$$
86		foeq1	$$⊢{X\upharpoonright }_A=X\to \left(\left({X\upharpoonright }_A\right):A\underset{onto}{⟶}A\leftrightarrow X:A\underset{onto}{⟶}A\right)$$
87	86	biimpar	$$⊢\left({X\upharpoonright }_A=X\wedge X:A\underset{onto}{⟶}A\right)\to \left({X\upharpoonright }_A\right):A\underset{onto}{⟶}A$$
88	83 85 87	syl2anc	$$⊢\phi \to \left({X\upharpoonright }_A\right):A\underset{onto}{⟶}A$$
89		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E$$
90		f1ofo	$$⊢\left({\mathrm{I}\upharpoonright }_E\right):E\underset{1-1\; onto}{⟶}E\to \left({\mathrm{I}\upharpoonright }_E\right):E\underset{onto}{⟶}E$$
91	89 90	mp1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_E\right):E\underset{onto}{⟶}E$$
92		foeq1	$$⊢{X\upharpoonright }_E={\mathrm{I}\upharpoonright }_E\to \left(\left({X\upharpoonright }_E\right):E\underset{onto}{⟶}E\leftrightarrow \left({\mathrm{I}\upharpoonright }_E\right):E\underset{onto}{⟶}E\right)$$
93	92	biimpar	$$⊢\left({X\upharpoonright }_E={\mathrm{I}\upharpoonright }_E\wedge \left({\mathrm{I}\upharpoonright }_E\right):E\underset{onto}{⟶}E\right)\to \left({X\upharpoonright }_E\right):E\underset{onto}{⟶}E$$
94	5 91 93	syl2anc	$$⊢\phi \to \left({X\upharpoonright }_E\right):E\underset{onto}{⟶}E$$
95		resdif	$$⊢\left(\mathrm{Fun}{X}^{-1}\wedge \left({X\upharpoonright }_A\right):A\underset{onto}{⟶}A\wedge \left({X\upharpoonright }_E\right):E\underset{onto}{⟶}E\right)\to \left({X\upharpoonright }_{\left(A\setminus E\right)}\right):A\setminus E\underset{1-1\; onto}{⟶}A\setminus E$$
96	80 88 94 95	syl3anc	$$⊢\phi \to \left({X\upharpoonright }_{\left(A\setminus E\right)}\right):A\setminus E\underset{1-1\; onto}{⟶}A\setminus E$$
97		ssun1	$$⊢E\subseteq E\cup F$$
98	97 8	sseqtrid	$$⊢\phi \to E\subseteq A$$
99		uneqdifeq	$$⊢\left(E\subseteq A\wedge E\cap F=\varnothing \right)\to \left(E\cup F=A\leftrightarrow A\setminus E=F\right)$$
100	99	biimpa	$$⊢\left(\left(E\subseteq A\wedge E\cap F=\varnothing \right)\wedge E\cup F=A\right)\to A\setminus E=F$$
101	98 7 8 100	syl21anc	$$⊢\phi \to A\setminus E=F$$
102	101	reseq2d	$$⊢\phi \to {X\upharpoonright }_{\left(A\setminus E\right)}={X\upharpoonright }_F$$
103	102 101 101	f1oeq123d	$$⊢\phi \to \left(\left({X\upharpoonright }_{\left(A\setminus E\right)}\right):A\setminus E\underset{1-1\; onto}{⟶}A\setminus E\leftrightarrow \left({X\upharpoonright }_F\right):F\underset{1-1\; onto}{⟶}F\right)$$
104	96 103	mpbid	$$⊢\phi \to \left({X\upharpoonright }_F\right):F\underset{1-1\; onto}{⟶}F$$
105		f1of	$$⊢\left({X\upharpoonright }_F\right):F\underset{1-1\; onto}{⟶}F\to \left({X\upharpoonright }_F\right):F⟶F$$
106	104 105	syl	$$⊢\phi \to \left({X\upharpoonright }_F\right):F⟶F$$
107	106	frnd	$$⊢\phi \to \mathrm{ran}\left({X\upharpoonright }_F\right)\subseteq F$$
108		cores	$$⊢\mathrm{ran}\left({X\upharpoonright }_F\right)\subseteq F\to \left({Y\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)=Y\circ \left({X\upharpoonright }_F\right)$$
109	107 108	syl	$$⊢\phi \to \left({Y\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)=Y\circ \left({X\upharpoonright }_F\right)$$
110	77 109	eqtr4id	$$⊢\phi \to {\left(Y\circ X\right)\upharpoonright }_F=\left({Y\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)$$
111	6	coeq1d	$$⊢\phi \to \left({Y\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)=\left({\mathrm{I}\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)$$
112		fcoi2	$$⊢\left({X\upharpoonright }_F\right):F⟶F\to \left({\mathrm{I}\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)={X\upharpoonright }_F$$
113	106 112	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_F\right)\circ \left({X\upharpoonright }_F\right)={X\upharpoonright }_F$$
114	110 111 113	3eqtrd	$$⊢\phi \to {\left(Y\circ X\right)\upharpoonright }_F={X\upharpoonright }_F$$
115	76 114	uneq12d	$$⊢\phi \to \left({\left(Y\circ X\right)\upharpoonright }_E\right)\cup \left({\left(Y\circ X\right)\upharpoonright }_F\right)=\left({Y\upharpoonright }_E\right)\cup \left({X\upharpoonright }_F\right)$$
116	71 115	syl5eq	$$⊢\phi \to {\left(Y\circ X\right)\upharpoonright }_{\left(E\cup F\right)}=\left({Y\upharpoonright }_E\right)\cup \left({X\upharpoonright }_F\right)$$
117		f1oco	$$⊢\left(Y:A\underset{1-1\; onto}{⟶}A\wedge X:A\underset{1-1\; onto}{⟶}A\right)\to \left(Y\circ X\right):A\underset{1-1\; onto}{⟶}A$$
118	13 63 117	syl2anc	$$⊢\phi \to \left(Y\circ X\right):A\underset{1-1\; onto}{⟶}A$$
119		f1ofn	$$⊢\left(Y\circ X\right):A\underset{1-1\; onto}{⟶}A\to \left(Y\circ X\right)FnA$$
120		fnresdm	$$⊢\left(Y\circ X\right)FnA\to {\left(Y\circ X\right)\upharpoonright }_A=Y\circ X$$
121	118 119 120	3syl	$$⊢\phi \to {\left(Y\circ X\right)\upharpoonright }_A=Y\circ X$$
122	70 116 121	3eqtr3d	$$⊢\phi \to \left({Y\upharpoonright }_E\right)\cup \left({X\upharpoonright }_F\right)=Y\circ X$$
123	69 122	eqtr3d	$$⊢\phi \to X\circ Y=Y\circ X$$