Metamath Proof Explorer

Theorem 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 
|- ( ph -> X e. B )
symgcom.y 
|- ( ph -> Y e. B )
symgcom2.1 
|- ( ph -> ( dom ( X \ _I ) i^i dom ( Y \ _I ) ) = (/) )
Assertion symgcom2 
|- ( 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 symgcom2.1 
 |-  ( ph -> ( dom ( X \ _I ) i^i dom ( Y \ _I ) ) = (/) )
6 1 2 symgbasf 
 |-  ( X e. B -> X : A --> A )
7 3 6 syl 
 |-  ( ph -> X : A --> A )
8 7 ffnd 
 |-  ( ph -> X Fn A )
9 fnresi 
 |-  ( _I |` A ) Fn A
10 9 a1i 
 |-  ( ph -> ( _I |` A ) Fn A )
11 difssd 
 |-  ( ph -> ( A \ dom ( X \ _I ) ) C_ A )
12 ssidd 
 |-  ( ph -> ( A \ dom ( X \ _I ) ) C_ ( A \ dom ( X \ _I ) ) )
13 nfpconfp 
 |-  ( X Fn A -> ( A \ dom ( X \ _I ) ) = dom ( X i^i _I ) )
14 8 13 syl 
 |-  ( ph -> ( A \ dom ( X \ _I ) ) = dom ( X i^i _I ) )
15 inres 
 |-  ( X i^i ( _I |` A ) ) = ( ( X i^i _I ) |` A )
16 reli 
 |-  Rel _I
17 relin2 
 |-  ( Rel _I -> Rel ( X i^i _I ) )
18 16 17 ax-mp 
 |-  Rel ( X i^i _I )
19 14 11 eqsstrrd 
 |-  ( ph -> dom ( X i^i _I ) C_ A )
20 relssres 
 |-  ( ( Rel ( X i^i _I ) /\ dom ( X i^i _I ) C_ A ) -> ( ( X i^i _I ) |` A ) = ( X i^i _I ) )
21 18 19 20 sylancr 
 |-  ( ph -> ( ( X i^i _I ) |` A ) = ( X i^i _I ) )
22 15 21 syl5eq 
 |-  ( ph -> ( X i^i ( _I |` A ) ) = ( X i^i _I ) )
23 22 dmeqd 
 |-  ( ph -> dom ( X i^i ( _I |` A ) ) = dom ( X i^i _I ) )
24 14 23 eqtr4d 
 |-  ( ph -> ( A \ dom ( X \ _I ) ) = dom ( X i^i ( _I |` A ) ) )
25 12 24 sseqtrd 
 |-  ( ph -> ( A \ dom ( X \ _I ) ) C_ dom ( X i^i ( _I |` A ) ) )
26 fnreseql 
 |-  ( ( X Fn A /\ ( _I |` A ) Fn A /\ ( A \ dom ( X \ _I ) ) C_ A ) -> ( ( X |` ( A \ dom ( X \ _I ) ) ) = ( ( _I |` A ) |` ( A \ dom ( X \ _I ) ) ) <-> ( A \ dom ( X \ _I ) ) C_ dom ( X i^i ( _I |` A ) ) ) )
27 26 biimpar 
 |-  ( ( ( X Fn A /\ ( _I |` A ) Fn A /\ ( A \ dom ( X \ _I ) ) C_ A ) /\ ( A \ dom ( X \ _I ) ) C_ dom ( X i^i ( _I |` A ) ) ) -> ( X |` ( A \ dom ( X \ _I ) ) ) = ( ( _I |` A ) |` ( A \ dom ( X \ _I ) ) ) )
28 8 10 11 25 27 syl31anc 
 |-  ( ph -> ( X |` ( A \ dom ( X \ _I ) ) ) = ( ( _I |` A ) |` ( A \ dom ( X \ _I ) ) ) )
29 11 resabs1d 
 |-  ( ph -> ( ( _I |` A ) |` ( A \ dom ( X \ _I ) ) ) = ( _I |` ( A \ dom ( X \ _I ) ) ) )
30 28 29 eqtrd 
 |-  ( ph -> ( X |` ( A \ dom ( X \ _I ) ) ) = ( _I |` ( A \ dom ( X \ _I ) ) ) )
31 1 2 symgbasf 
 |-  ( Y e. B -> Y : A --> A )
32 4 31 syl 
 |-  ( ph -> Y : A --> A )
33 32 ffnd 
 |-  ( ph -> Y Fn A )
34 difss 
 |-  ( X \ _I ) C_ X
35 dmss 
 |-  ( ( X \ _I ) C_ X -> dom ( X \ _I ) C_ dom X )
36 34 35 ax-mp 
 |-  dom ( X \ _I ) C_ dom X
37 fdm 
 |-  ( X : A --> A -> dom X = A )
38 3 6 37 3syl 
 |-  ( ph -> dom X = A )
39 36 38 sseqtrid 
 |-  ( ph -> dom ( X \ _I ) C_ A )
40 reldisj 
 |-  ( dom ( X \ _I ) C_ A -> ( ( dom ( X \ _I ) i^i dom ( Y \ _I ) ) = (/) <-> dom ( X \ _I ) C_ ( A \ dom ( Y \ _I ) ) ) )
41 39 40 syl 
 |-  ( ph -> ( ( dom ( X \ _I ) i^i dom ( Y \ _I ) ) = (/) <-> dom ( X \ _I ) C_ ( A \ dom ( Y \ _I ) ) ) )
42 5 41 mpbid 
 |-  ( ph -> dom ( X \ _I ) C_ ( A \ dom ( Y \ _I ) ) )
43 nfpconfp 
 |-  ( Y Fn A -> ( A \ dom ( Y \ _I ) ) = dom ( Y i^i _I ) )
44 33 43 syl 
 |-  ( ph -> ( A \ dom ( Y \ _I ) ) = dom ( Y i^i _I ) )
45 42 44 sseqtrd 
 |-  ( ph -> dom ( X \ _I ) C_ dom ( Y i^i _I ) )
46 inres 
 |-  ( Y i^i ( _I |` A ) ) = ( ( Y i^i _I ) |` A )
47 relin2 
 |-  ( Rel _I -> Rel ( Y i^i _I ) )
48 16 47 ax-mp 
 |-  Rel ( Y i^i _I )
49 difssd 
 |-  ( ph -> ( A \ dom ( Y \ _I ) ) C_ A )
50 44 49 eqsstrrd 
 |-  ( ph -> dom ( Y i^i _I ) C_ A )
51 relssres 
 |-  ( ( Rel ( Y i^i _I ) /\ dom ( Y i^i _I ) C_ A ) -> ( ( Y i^i _I ) |` A ) = ( Y i^i _I ) )
52 48 50 51 sylancr 
 |-  ( ph -> ( ( Y i^i _I ) |` A ) = ( Y i^i _I ) )
53 46 52 syl5eq 
 |-  ( ph -> ( Y i^i ( _I |` A ) ) = ( Y i^i _I ) )
54 53 dmeqd 
 |-  ( ph -> dom ( Y i^i ( _I |` A ) ) = dom ( Y i^i _I ) )
55 45 54 sseqtrrd 
 |-  ( ph -> dom ( X \ _I ) C_ dom ( Y i^i ( _I |` A ) ) )
56 fnreseql 
 |-  ( ( Y Fn A /\ ( _I |` A ) Fn A /\ dom ( X \ _I ) C_ A ) -> ( ( Y |` dom ( X \ _I ) ) = ( ( _I |` A ) |` dom ( X \ _I ) ) <-> dom ( X \ _I ) C_ dom ( Y i^i ( _I |` A ) ) ) )
57 56 biimpar 
 |-  ( ( ( Y Fn A /\ ( _I |` A ) Fn A /\ dom ( X \ _I ) C_ A ) /\ dom ( X \ _I ) C_ dom ( Y i^i ( _I |` A ) ) ) -> ( Y |` dom ( X \ _I ) ) = ( ( _I |` A ) |` dom ( X \ _I ) ) )
58 33 10 39 55 57 syl31anc 
 |-  ( ph -> ( Y |` dom ( X \ _I ) ) = ( ( _I |` A ) |` dom ( X \ _I ) ) )
59 39 resabs1d 
 |-  ( ph -> ( ( _I |` A ) |` dom ( X \ _I ) ) = ( _I |` dom ( X \ _I ) ) )
60 58 59 eqtrd 
 |-  ( ph -> ( Y |` dom ( X \ _I ) ) = ( _I |` dom ( X \ _I ) ) )
61 difin2 
 |-  ( dom ( X \ _I ) C_ A -> ( dom ( X \ _I ) \ dom ( X \ _I ) ) = ( ( A \ dom ( X \ _I ) ) i^i dom ( X \ _I ) ) )
62 39 61 syl 
 |-  ( ph -> ( dom ( X \ _I ) \ dom ( X \ _I ) ) = ( ( A \ dom ( X \ _I ) ) i^i dom ( X \ _I ) ) )
63 difid 
 |-  ( dom ( X \ _I ) \ dom ( X \ _I ) ) = (/)
64 62 63 eqtr3di 
 |-  ( ph -> ( ( A \ dom ( X \ _I ) ) i^i dom ( X \ _I ) ) = (/) )
65 undif1 
 |-  ( ( A \ dom ( X \ _I ) ) u. dom ( X \ _I ) ) = ( A u. dom ( X \ _I ) )
66 ssequn2 
 |-  ( dom ( X \ _I ) C_ A <-> ( A u. dom ( X \ _I ) ) = A )
67 39 66 sylib 
 |-  ( ph -> ( A u. dom ( X \ _I ) ) = A )
68 65 67 syl5eq 
 |-  ( ph -> ( ( A \ dom ( X \ _I ) ) u. dom ( X \ _I ) ) = A )
69 1 2 3 4 30 60 64 68 symgcom 
 |-  ( ph -> ( X o. Y ) = ( Y o. X ) )