Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  symgcom2 Structured version   Visualization version   GIF version

Theorem symgcom2 30883
 Description: Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.)
Hypotheses
Ref Expression
symgcom.g 𝐺 = (SymGrp‘𝐴)
symgcom.b 𝐵 = (Base‘𝐺)
symgcom.x (𝜑𝑋𝐵)
symgcom.y (𝜑𝑌𝐵)
symgcom2.1 (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅)
Assertion
Ref Expression
symgcom2 (𝜑 → (𝑋𝑌) = (𝑌𝑋))

Proof of Theorem symgcom2
StepHypRef Expression
1 symgcom.g . 2 𝐺 = (SymGrp‘𝐴)
2 symgcom.b . 2 𝐵 = (Base‘𝐺)
3 symgcom.x . 2 (𝜑𝑋𝐵)
4 symgcom.y . 2 (𝜑𝑌𝐵)
51, 2symgbasf 18576 . . . . . 6 (𝑋𝐵𝑋:𝐴𝐴)
63, 5syl 17 . . . . 5 (𝜑𝑋:𝐴𝐴)
76ffnd 6503 . . . 4 (𝜑𝑋 Fn 𝐴)
8 fnresi 6463 . . . . 5 ( I ↾ 𝐴) Fn 𝐴
98a1i 11 . . . 4 (𝜑 → ( I ↾ 𝐴) Fn 𝐴)
10 difssd 4040 . . . 4 (𝜑 → (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ 𝐴)
11 ssidd 3917 . . . . 5 (𝜑 → (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ (𝐴 ∖ dom (𝑋 ∖ I )))
12 nfpconfp 30494 . . . . . . 7 (𝑋 Fn 𝐴 → (𝐴 ∖ dom (𝑋 ∖ I )) = dom (𝑋 ∩ I ))
137, 12syl 17 . . . . . 6 (𝜑 → (𝐴 ∖ dom (𝑋 ∖ I )) = dom (𝑋 ∩ I ))
14 inres 5845 . . . . . . . 8 (𝑋 ∩ ( I ↾ 𝐴)) = ((𝑋 ∩ I ) ↾ 𝐴)
15 reli 5672 . . . . . . . . . 10 Rel I
16 relin2 5659 . . . . . . . . . 10 (Rel I → Rel (𝑋 ∩ I ))
1715, 16ax-mp 5 . . . . . . . . 9 Rel (𝑋 ∩ I )
1813, 10eqsstrrd 3933 . . . . . . . . 9 (𝜑 → dom (𝑋 ∩ I ) ⊆ 𝐴)
19 relssres 5868 . . . . . . . . 9 ((Rel (𝑋 ∩ I ) ∧ dom (𝑋 ∩ I ) ⊆ 𝐴) → ((𝑋 ∩ I ) ↾ 𝐴) = (𝑋 ∩ I ))
2017, 18, 19sylancr 590 . . . . . . . 8 (𝜑 → ((𝑋 ∩ I ) ↾ 𝐴) = (𝑋 ∩ I ))
2114, 20syl5eq 2805 . . . . . . 7 (𝜑 → (𝑋 ∩ ( I ↾ 𝐴)) = (𝑋 ∩ I ))
2221dmeqd 5750 . . . . . 6 (𝜑 → dom (𝑋 ∩ ( I ↾ 𝐴)) = dom (𝑋 ∩ I ))
2313, 22eqtr4d 2796 . . . . 5 (𝜑 → (𝐴 ∖ dom (𝑋 ∖ I )) = dom (𝑋 ∩ ( I ↾ 𝐴)))
2411, 23sseqtrd 3934 . . . 4 (𝜑 → (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ dom (𝑋 ∩ ( I ↾ 𝐴)))
25 fnreseql 6813 . . . . 5 ((𝑋 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴 ∧ (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ 𝐴) → ((𝑋 ↾ (𝐴 ∖ dom (𝑋 ∖ I ))) = (( I ↾ 𝐴) ↾ (𝐴 ∖ dom (𝑋 ∖ I ))) ↔ (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ dom (𝑋 ∩ ( I ↾ 𝐴))))
2625biimpar 481 . . . 4 (((𝑋 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴 ∧ (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ 𝐴) ∧ (𝐴 ∖ dom (𝑋 ∖ I )) ⊆ dom (𝑋 ∩ ( I ↾ 𝐴))) → (𝑋 ↾ (𝐴 ∖ dom (𝑋 ∖ I ))) = (( I ↾ 𝐴) ↾ (𝐴 ∖ dom (𝑋 ∖ I ))))
277, 9, 10, 24, 26syl31anc 1370 . . 3 (𝜑 → (𝑋 ↾ (𝐴 ∖ dom (𝑋 ∖ I ))) = (( I ↾ 𝐴) ↾ (𝐴 ∖ dom (𝑋 ∖ I ))))
2810resabs1d 5858 . . 3 (𝜑 → (( I ↾ 𝐴) ↾ (𝐴 ∖ dom (𝑋 ∖ I ))) = ( I ↾ (𝐴 ∖ dom (𝑋 ∖ I ))))
2927, 28eqtrd 2793 . 2 (𝜑 → (𝑋 ↾ (𝐴 ∖ dom (𝑋 ∖ I ))) = ( I ↾ (𝐴 ∖ dom (𝑋 ∖ I ))))
301, 2symgbasf 18576 . . . . . 6 (𝑌𝐵𝑌:𝐴𝐴)
314, 30syl 17 . . . . 5 (𝜑𝑌:𝐴𝐴)
3231ffnd 6503 . . . 4 (𝜑𝑌 Fn 𝐴)
33 difss 4039 . . . . . 6 (𝑋 ∖ I ) ⊆ 𝑋
34 dmss 5747 . . . . . 6 ((𝑋 ∖ I ) ⊆ 𝑋 → dom (𝑋 ∖ I ) ⊆ dom 𝑋)
3533, 34ax-mp 5 . . . . 5 dom (𝑋 ∖ I ) ⊆ dom 𝑋
36 fdm 6510 . . . . . 6 (𝑋:𝐴𝐴 → dom 𝑋 = 𝐴)
373, 5, 363syl 18 . . . . 5 (𝜑 → dom 𝑋 = 𝐴)
3835, 37sseqtrid 3946 . . . 4 (𝜑 → dom (𝑋 ∖ I ) ⊆ 𝐴)
39 symgcom2.1 . . . . . . 7 (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅)
40 reldisj 4351 . . . . . . . 8 (dom (𝑋 ∖ I ) ⊆ 𝐴 → ((dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅ ↔ dom (𝑋 ∖ I ) ⊆ (𝐴 ∖ dom (𝑌 ∖ I ))))
4138, 40syl 17 . . . . . . 7 (𝜑 → ((dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅ ↔ dom (𝑋 ∖ I ) ⊆ (𝐴 ∖ dom (𝑌 ∖ I ))))
4239, 41mpbid 235 . . . . . 6 (𝜑 → dom (𝑋 ∖ I ) ⊆ (𝐴 ∖ dom (𝑌 ∖ I )))
43 nfpconfp 30494 . . . . . . 7 (𝑌 Fn 𝐴 → (𝐴 ∖ dom (𝑌 ∖ I )) = dom (𝑌 ∩ I ))
4432, 43syl 17 . . . . . 6 (𝜑 → (𝐴 ∖ dom (𝑌 ∖ I )) = dom (𝑌 ∩ I ))
4542, 44sseqtrd 3934 . . . . 5 (𝜑 → dom (𝑋 ∖ I ) ⊆ dom (𝑌 ∩ I ))
46 inres 5845 . . . . . . 7 (𝑌 ∩ ( I ↾ 𝐴)) = ((𝑌 ∩ I ) ↾ 𝐴)
47 relin2 5659 . . . . . . . . 9 (Rel I → Rel (𝑌 ∩ I ))
4815, 47ax-mp 5 . . . . . . . 8 Rel (𝑌 ∩ I )
49 difssd 4040 . . . . . . . . 9 (𝜑 → (𝐴 ∖ dom (𝑌 ∖ I )) ⊆ 𝐴)
5044, 49eqsstrrd 3933 . . . . . . . 8 (𝜑 → dom (𝑌 ∩ I ) ⊆ 𝐴)
51 relssres 5868 . . . . . . . 8 ((Rel (𝑌 ∩ I ) ∧ dom (𝑌 ∩ I ) ⊆ 𝐴) → ((𝑌 ∩ I ) ↾ 𝐴) = (𝑌 ∩ I ))
5248, 50, 51sylancr 590 . . . . . . 7 (𝜑 → ((𝑌 ∩ I ) ↾ 𝐴) = (𝑌 ∩ I ))
5346, 52syl5eq 2805 . . . . . 6 (𝜑 → (𝑌 ∩ ( I ↾ 𝐴)) = (𝑌 ∩ I ))
5453dmeqd 5750 . . . . 5 (𝜑 → dom (𝑌 ∩ ( I ↾ 𝐴)) = dom (𝑌 ∩ I ))
5545, 54sseqtrrd 3935 . . . 4 (𝜑 → dom (𝑋 ∖ I ) ⊆ dom (𝑌 ∩ ( I ↾ 𝐴)))
56 fnreseql 6813 . . . . 5 ((𝑌 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴 ∧ dom (𝑋 ∖ I ) ⊆ 𝐴) → ((𝑌 ↾ dom (𝑋 ∖ I )) = (( I ↾ 𝐴) ↾ dom (𝑋 ∖ I )) ↔ dom (𝑋 ∖ I ) ⊆ dom (𝑌 ∩ ( I ↾ 𝐴))))
5756biimpar 481 . . . 4 (((𝑌 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴 ∧ dom (𝑋 ∖ I ) ⊆ 𝐴) ∧ dom (𝑋 ∖ I ) ⊆ dom (𝑌 ∩ ( I ↾ 𝐴))) → (𝑌 ↾ dom (𝑋 ∖ I )) = (( I ↾ 𝐴) ↾ dom (𝑋 ∖ I )))
5832, 9, 38, 55, 57syl31anc 1370 . . 3 (𝜑 → (𝑌 ↾ dom (𝑋 ∖ I )) = (( I ↾ 𝐴) ↾ dom (𝑋 ∖ I )))
5938resabs1d 5858 . . 3 (𝜑 → (( I ↾ 𝐴) ↾ dom (𝑋 ∖ I )) = ( I ↾ dom (𝑋 ∖ I )))
6058, 59eqtrd 2793 . 2 (𝜑 → (𝑌 ↾ dom (𝑋 ∖ I )) = ( I ↾ dom (𝑋 ∖ I )))
61 difid 4271 . . 3 (dom (𝑋 ∖ I ) ∖ dom (𝑋 ∖ I )) = ∅
62 difin2 4198 . . . 4 (dom (𝑋 ∖ I ) ⊆ 𝐴 → (dom (𝑋 ∖ I ) ∖ dom (𝑋 ∖ I )) = ((𝐴 ∖ dom (𝑋 ∖ I )) ∩ dom (𝑋 ∖ I )))
6338, 62syl 17 . . 3 (𝜑 → (dom (𝑋 ∖ I ) ∖ dom (𝑋 ∖ I )) = ((𝐴 ∖ dom (𝑋 ∖ I )) ∩ dom (𝑋 ∖ I )))
6461, 63syl5reqr 2808 . 2 (𝜑 → ((𝐴 ∖ dom (𝑋 ∖ I )) ∩ dom (𝑋 ∖ I )) = ∅)
65 undif1 4375 . . 3 ((𝐴 ∖ dom (𝑋 ∖ I )) ∪ dom (𝑋 ∖ I )) = (𝐴 ∪ dom (𝑋 ∖ I ))
66 ssequn2 4090 . . . 4 (dom (𝑋 ∖ I ) ⊆ 𝐴 ↔ (𝐴 ∪ dom (𝑋 ∖ I )) = 𝐴)
6738, 66sylib 221 . . 3 (𝜑 → (𝐴 ∪ dom (𝑋 ∖ I )) = 𝐴)
6865, 67syl5eq 2805 . 2 (𝜑 → ((𝐴 ∖ dom (𝑋 ∖ I )) ∪ dom (𝑋 ∖ I )) = 𝐴)
691, 2, 3, 4, 29, 60, 64, 68symgcom 30882 1 (𝜑 → (𝑋𝑌) = (𝑌𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ∖ cdif 3857   ∪ cun 3858   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227   I cid 5432  dom cdm 5527   ↾ cres 5529   ∘ ccom 5531  Rel wrel 5532   Fn wfn 6334  ⟶wf 6335  ‘cfv 6339  Basecbs 16546  SymGrpcsymg 18567 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7585  df-1st 7698  df-2nd 7699  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-er 8304  df-map 8423  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-nn 11680  df-2 11742  df-3 11743  df-4 11744  df-5 11745  df-6 11746  df-7 11747  df-8 11748  df-9 11749  df-n0 11940  df-z 12026  df-uz 12288  df-fz 12945  df-struct 16548  df-ndx 16549  df-slot 16550  df-base 16552  df-sets 16553  df-ress 16554  df-plusg 16641  df-tset 16647  df-efmnd 18105  df-symg 18568 This theorem is referenced by:  symgcntz  30884
 Copyright terms: Public domain W3C validator