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 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symgcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
symgcom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
symgcom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
symgcom2.1 ⊢ ( 𝜑 → ( dom ( 𝑋 ∖ I ) ∩ dom ( 𝑌 ∖ I ) ) = ∅ )
Assertion symgcom2 ( 𝜑 → ( 𝑋 ∘ 𝑌 ) = ( 𝑌 ∘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 symgcom.g ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 symgcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 symgcom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 symgcom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 symgcom2.1 ⊢ ( 𝜑 → ( dom ( 𝑋 ∖ I ) ∩ dom ( 𝑌 ∖ I ) ) = ∅ )
6 1 2 symgbasf ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 : 𝐴 ⟶ 𝐴 )
7 3 6 syl ⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐴 )
8 7 ffnd ⊢ ( 𝜑 → 𝑋 Fn 𝐴 )
9 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
10 9 a1i ⊢ ( 𝜑 → ( I ↾ 𝐴 ) Fn 𝐴 )
11 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ 𝐴 )
12 ssidd ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) )
13 nfpconfp ⊢ ( 𝑋 Fn 𝐴 → ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) = dom ( 𝑋 ∩ I ) )
14 8 13 syl ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) = dom ( 𝑋 ∩ I ) )
15 inres ⊢ ( 𝑋 ∩ ( I ↾ 𝐴 ) ) = ( ( 𝑋 ∩ I ) ↾ 𝐴 )
16 reli ⊢ Rel I
17 relin2 ⊢ ( Rel I → Rel ( 𝑋 ∩ I ) )
18 16 17 ax-mp ⊢ Rel ( 𝑋 ∩ I )
19 14 11 eqsstrrd ⊢ ( 𝜑 → dom ( 𝑋 ∩ I ) ⊆ 𝐴 )
20 relssres ⊢ ( ( Rel ( 𝑋 ∩ I ) ∧ dom ( 𝑋 ∩ I ) ⊆ 𝐴 ) → ( ( 𝑋 ∩ I ) ↾ 𝐴 ) = ( 𝑋 ∩ I ) )
21 18 19 20 sylancr ⊢ ( 𝜑 → ( ( 𝑋 ∩ I ) ↾ 𝐴 ) = ( 𝑋 ∩ I ) )
22 15 21 syl5eq ⊢ ( 𝜑 → ( 𝑋 ∩ ( I ↾ 𝐴 ) ) = ( 𝑋 ∩ I ) )
23 22 dmeqd ⊢ ( 𝜑 → dom ( 𝑋 ∩ ( I ↾ 𝐴 ) ) = dom ( 𝑋 ∩ I ) )
24 14 23 eqtr4d ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) = dom ( 𝑋 ∩ ( I ↾ 𝐴 ) ) )
25 12 24 sseqtrd ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ dom ( 𝑋 ∩ ( I ↾ 𝐴 ) ) )
26 fnreseql ⊢ ( ( 𝑋 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ∧ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ 𝐴 ) → ( ( 𝑋 ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) = ( ( I ↾ 𝐴 ) ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) ↔ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ dom ( 𝑋 ∩ ( I ↾ 𝐴 ) ) ) )
27 26 biimpar ⊢ ( ( ( 𝑋 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ∧ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ 𝐴 ) ∧ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ⊆ dom ( 𝑋 ∩ ( I ↾ 𝐴 ) ) ) → ( 𝑋 ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) = ( ( I ↾ 𝐴 ) ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) )
28 8 10 11 25 27 syl31anc ⊢ ( 𝜑 → ( 𝑋 ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) = ( ( I ↾ 𝐴 ) ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) )
29 11 resabs1d ⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) = ( I ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) )
30 28 29 eqtrd ⊢ ( 𝜑 → ( 𝑋 ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) = ( I ↾ ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ) )
31 1 2 symgbasf ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 : 𝐴 ⟶ 𝐴 )
32 4 31 syl ⊢ ( 𝜑 → 𝑌 : 𝐴 ⟶ 𝐴 )
33 32 ffnd ⊢ ( 𝜑 → 𝑌 Fn 𝐴 )
34 difss ⊢ ( 𝑋 ∖ I ) ⊆ 𝑋
35 dmss ⊢ ( ( 𝑋 ∖ I ) ⊆ 𝑋 → dom ( 𝑋 ∖ I ) ⊆ dom 𝑋 )
36 34 35 ax-mp ⊢ dom ( 𝑋 ∖ I ) ⊆ dom 𝑋
37 fdm ⊢ ( 𝑋 : 𝐴 ⟶ 𝐴 → dom 𝑋 = 𝐴 )
38 3 6 37 3syl ⊢ ( 𝜑 → dom 𝑋 = 𝐴 )
39 36 38 sseqtrid ⊢ ( 𝜑 → dom ( 𝑋 ∖ I ) ⊆ 𝐴 )
40 reldisj ⊢ ( dom ( 𝑋 ∖ I ) ⊆ 𝐴 → ( ( dom ( 𝑋 ∖ I ) ∩ dom ( 𝑌 ∖ I ) ) = ∅ ↔ dom ( 𝑋 ∖ I ) ⊆ ( 𝐴 ∖ dom ( 𝑌 ∖ I ) ) ) )
41 39 40 syl ⊢ ( 𝜑 → ( ( dom ( 𝑋 ∖ I ) ∩ dom ( 𝑌 ∖ I ) ) = ∅ ↔ dom ( 𝑋 ∖ I ) ⊆ ( 𝐴 ∖ dom ( 𝑌 ∖ I ) ) ) )
42 5 41 mpbid ⊢ ( 𝜑 → dom ( 𝑋 ∖ I ) ⊆ ( 𝐴 ∖ dom ( 𝑌 ∖ I ) ) )
43 nfpconfp ⊢ ( 𝑌 Fn 𝐴 → ( 𝐴 ∖ dom ( 𝑌 ∖ I ) ) = dom ( 𝑌 ∩ I ) )
44 33 43 syl ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑌 ∖ I ) ) = dom ( 𝑌 ∩ I ) )
45 42 44 sseqtrd ⊢ ( 𝜑 → dom ( 𝑋 ∖ I ) ⊆ dom ( 𝑌 ∩ I ) )
46 inres ⊢ ( 𝑌 ∩ ( I ↾ 𝐴 ) ) = ( ( 𝑌 ∩ I ) ↾ 𝐴 )
47 relin2 ⊢ ( Rel I → Rel ( 𝑌 ∩ I ) )
48 16 47 ax-mp ⊢ Rel ( 𝑌 ∩ I )
49 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ dom ( 𝑌 ∖ I ) ) ⊆ 𝐴 )
50 44 49 eqsstrrd ⊢ ( 𝜑 → dom ( 𝑌 ∩ I ) ⊆ 𝐴 )
51 relssres ⊢ ( ( Rel ( 𝑌 ∩ I ) ∧ dom ( 𝑌 ∩ I ) ⊆ 𝐴 ) → ( ( 𝑌 ∩ I ) ↾ 𝐴 ) = ( 𝑌 ∩ I ) )
52 48 50 51 sylancr ⊢ ( 𝜑 → ( ( 𝑌 ∩ I ) ↾ 𝐴 ) = ( 𝑌 ∩ I ) )
53 46 52 syl5eq ⊢ ( 𝜑 → ( 𝑌 ∩ ( I ↾ 𝐴 ) ) = ( 𝑌 ∩ I ) )
54 53 dmeqd ⊢ ( 𝜑 → dom ( 𝑌 ∩ ( I ↾ 𝐴 ) ) = dom ( 𝑌 ∩ I ) )
55 45 54 sseqtrrd ⊢ ( 𝜑 → dom ( 𝑋 ∖ I ) ⊆ dom ( 𝑌 ∩ ( I ↾ 𝐴 ) ) )
56 fnreseql ⊢ ( ( 𝑌 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ∧ dom ( 𝑋 ∖ I ) ⊆ 𝐴 ) → ( ( 𝑌 ↾ dom ( 𝑋 ∖ I ) ) = ( ( I ↾ 𝐴 ) ↾ dom ( 𝑋 ∖ I ) ) ↔ dom ( 𝑋 ∖ I ) ⊆ dom ( 𝑌 ∩ ( I ↾ 𝐴 ) ) ) )
57 56 biimpar ⊢ ( ( ( 𝑌 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ∧ dom ( 𝑋 ∖ I ) ⊆ 𝐴 ) ∧ dom ( 𝑋 ∖ I ) ⊆ dom ( 𝑌 ∩ ( I ↾ 𝐴 ) ) ) → ( 𝑌 ↾ dom ( 𝑋 ∖ I ) ) = ( ( I ↾ 𝐴 ) ↾ dom ( 𝑋 ∖ I ) ) )
58 33 10 39 55 57 syl31anc ⊢ ( 𝜑 → ( 𝑌 ↾ dom ( 𝑋 ∖ I ) ) = ( ( I ↾ 𝐴 ) ↾ dom ( 𝑋 ∖ I ) ) )
59 39 resabs1d ⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ↾ dom ( 𝑋 ∖ I ) ) = ( I ↾ dom ( 𝑋 ∖ I ) ) )
60 58 59 eqtrd ⊢ ( 𝜑 → ( 𝑌 ↾ dom ( 𝑋 ∖ I ) ) = ( I ↾ dom ( 𝑋 ∖ I ) ) )
61 difin2 ⊢ ( dom ( 𝑋 ∖ I ) ⊆ 𝐴 → ( dom ( 𝑋 ∖ I ) ∖ dom ( 𝑋 ∖ I ) ) = ( ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ∩ dom ( 𝑋 ∖ I ) ) )
62 39 61 syl ⊢ ( 𝜑 → ( dom ( 𝑋 ∖ I ) ∖ dom ( 𝑋 ∖ I ) ) = ( ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ∩ dom ( 𝑋 ∖ I ) ) )
63 difid ⊢ ( dom ( 𝑋 ∖ I ) ∖ dom ( 𝑋 ∖ I ) ) = ∅
64 62 63 eqtr3di ⊢ ( 𝜑 → ( ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ∩ dom ( 𝑋 ∖ I ) ) = ∅ )
65 undif1 ⊢ ( ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ∪ dom ( 𝑋 ∖ I ) ) = ( 𝐴 ∪ dom ( 𝑋 ∖ I ) )
66 ssequn2 ⊢ ( dom ( 𝑋 ∖ I ) ⊆ 𝐴 ↔ ( 𝐴 ∪ dom ( 𝑋 ∖ I ) ) = 𝐴 )
67 39 66 sylib ⊢ ( 𝜑 → ( 𝐴 ∪ dom ( 𝑋 ∖ I ) ) = 𝐴 )
68 65 67 syl5eq ⊢ ( 𝜑 → ( ( 𝐴 ∖ dom ( 𝑋 ∖ I ) ) ∪ dom ( 𝑋 ∖ I ) ) = 𝐴 )
69 1 2 3 4 30 60 64 68 symgcom ⊢ ( 𝜑 → ( 𝑋 ∘ 𝑌 ) = ( 𝑌 ∘ 𝑋 ) )