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 
|- ( ph -> X e. B )
symgcom.y 
|- ( ph -> Y e. B )
symgcom.1 
|- ( ph -> ( X |` E ) = ( _I |` E ) )
symgcom.2 
|- ( ph -> ( Y |` F ) = ( _I |` F ) )
symgcom.3 
|- ( ph -> ( E i^i F ) = (/) )
symgcom.4 
|- ( ph -> ( E u. F ) = A )
Assertion symgcom 
|- ( ph -> ( X o. Y ) = ( Y o. X ) )

Proof

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