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 = SymGrp A
symgcom.b B = Base G
symgcom.x φ X B
symgcom.y φ Y B
symgcom.1 φ X E = I E
symgcom.2 φ Y F = I F
symgcom.3 φ E F =
symgcom.4 φ E F = A
Assertion symgcom φ X Y = Y X

Proof

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