# Metamath Proof Explorer

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