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

Theorem cyc3conja 30950
 Description: All 3-cycles are conjugate in the alternating group An for n>= 5. Property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 15-Oct-2023.)
Hypotheses
Ref Expression
cyc3conja.c 𝐶 = (𝑀 “ (♯ “ {3}))
cyc3conja.a 𝐴 = (pmEven‘𝐷)
cyc3conja.s 𝑆 = (SymGrp‘𝐷)
cyc3conja.n 𝑁 = (♯‘𝐷)
cyc3conja.m 𝑀 = (toCyc‘𝐷)
cyc3conja.p + = (+g𝑆)
cyc3conja.l = (-g𝑆)
cyc3conja.1 (𝜑 → 5 ≤ 𝑁)
cyc3conja.d (𝜑𝐷 ∈ Fin)
cyc3conja.q (𝜑𝑄𝐶)
cyc3conja.t (𝜑𝑇𝐶)
Assertion
Ref Expression
cyc3conja (𝜑 → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
Distinct variable groups:   + ,𝑝   ,𝑝   𝐴,𝑝   𝐷,𝑝   𝑀,𝑝   𝑄,𝑝   𝑆,𝑝   𝑇,𝑝   𝜑,𝑝
Allowed substitution hints:   𝐶(𝑝)   𝑁(𝑝)

Proof of Theorem cyc3conja
Dummy variables 𝑔 𝑢 𝑥 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 488 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → 𝑔𝐴)
2 simpr 488 . . . . . . 7 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → 𝑝 = 𝑔)
32oveq1d 7165 . . . . . 6 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
43, 2oveq12d 7168 . . . . 5 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) 𝑝) = ((𝑔 + 𝑇) 𝑔))
54eqeq2d 2769 . . . 4 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) 𝑔)))
6 simplr 768 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → 𝑄 = ((𝑔 + 𝑇) 𝑔))
71, 5, 6rspcedvd 3544 . . 3 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
8 cyc3conja.d . . . . . . . . 9 (𝜑𝐷 ∈ Fin)
98ad5antr 733 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝐷 ∈ Fin)
109ad3antrrr 729 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝐷 ∈ Fin)
11 simp-8r 791 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑔 ∈ (Base‘𝑆))
12 simp-6r 787 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ¬ 𝑔𝐴)
1311, 12eldifd 3869 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴))
14 simpllr 775 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥 ∈ (𝐷 ∖ ran 𝑢))
1514eldifad 3870 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥𝐷)
16 simplr 768 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑦 ∈ (𝐷 ∖ ran 𝑢))
1716eldifad 3870 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑦𝐷)
1815, 17prssd 4712 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19 simpr 488 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥𝑦)
20 pr2nelem 9464 . . . . . . . . . . 11 ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥𝑦) → {𝑥, 𝑦} ≈ 2o)
2114, 16, 19, 20syl3anc 1368 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ≈ 2o)
22 eqid 2758 . . . . . . . . . . 11 (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23 eqid 2758 . . . . . . . . . . 11 ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
2422, 23pmtrrn 18652 . . . . . . . . . 10 ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
2510, 18, 21, 24syl3anc 1368 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26 cyc3conja.s . . . . . . . . . 10 𝑆 = (SymGrp‘𝐷)
27 eqid 2758 . . . . . . . . . 10 (Base‘𝑆) = (Base‘𝑆)
2826, 27, 23pmtrodpm 20362 . . . . . . . . 9 ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
2910, 25, 28syl2anc 587 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
30 cyc3conja.a . . . . . . . . 9 𝐴 = (pmEven‘𝐷)
3130difeq2i 4025 . . . . . . . 8 ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
3229, 31eleqtrrdi 2863 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
3326, 27, 30odpmco 30881 . . . . . . 7 ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
3410, 13, 32, 33syl3anc 1368 . . . . . 6 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
35 simpr 488 . . . . . . . . 9 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
3635oveq1d 7165 . . . . . . . 8 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
3736, 35oveq12d 7168 . . . . . . 7 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
3837eqeq2d 2769 . . . . . 6 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
3929eldifad 3870 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40 0zd 12032 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
41 cyc3conja.n . . . . . . . . . . . . . . . . . 18 𝑁 = (♯‘𝐷)
42 hashcl 13767 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0)
438, 42syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘𝐷) ∈ ℕ0)
4441, 43eqeltrid 2856 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ0)
4544nn0zd 12124 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
46 3z 12054 . . . . . . . . . . . . . . . . 17 3 ∈ ℤ
4746a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ∈ ℤ)
48 0red 10682 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
4947zred 12126 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ∈ ℝ)
50 3pos 11779 . . . . . . . . . . . . . . . . . 18 0 < 3
5150a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 3)
5248, 49, 51ltled 10826 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 3)
53 5re 11761 . . . . . . . . . . . . . . . . . 18 5 ∈ ℝ
5453a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℝ)
5544nn0red 11995 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℝ)
56 3lt5 11852 . . . . . . . . . . . . . . . . . . 19 3 < 5
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 3 < 5)
5849, 54, 57ltled 10826 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≤ 5)
59 cyc3conja.1 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ≤ 𝑁)
6049, 54, 55, 58, 59letrd 10835 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ≤ 𝑁)
61 elfz4 12949 . . . . . . . . . . . . . . . 16 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (0 ≤ 3 ∧ 3 ≤ 𝑁)) → 3 ∈ (0...𝑁))
6240, 45, 47, 52, 60, 61syl32anc 1375 . . . . . . . . . . . . . . 15 (𝜑 → 3 ∈ (0...𝑁))
63 cyc3conja.c . . . . . . . . . . . . . . . 16 𝐶 = (𝑀 “ (♯ “ {3}))
64 cyc3conja.m . . . . . . . . . . . . . . . 16 𝑀 = (toCyc‘𝐷)
6563, 26, 41, 64, 27cycpmgcl 30946 . . . . . . . . . . . . . . 15 ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
668, 62, 65syl2anc 587 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ (Base‘𝑆))
67 cyc3conja.t . . . . . . . . . . . . . 14 (𝜑𝑇𝐶)
6866, 67sseldd 3893 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (Base‘𝑆))
6968ad8antr 739 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑇 ∈ (Base‘𝑆))
7064, 10, 15, 17, 19, 22cycpm2tr 30912 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
7170reseq1d 5822 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
7215, 17s2cld 14280 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
7315, 17, 19s2f1 30743 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1𝐷)
7464, 10, 72, 73tocycfvres2 30904 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
7574reseq1d 5822 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢))
76 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3})))
7776elin1d 4103 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
78 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢𝑤 = 𝑢)
79 dmeq 5743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
80 eqidd 2759 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢𝐷 = 𝐷)
8178, 79, 80f1eq123d 6594 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
8281elrab 3602 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
8377, 82sylib 221 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
8483simprd 499 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢:dom 𝑢1-1𝐷)
85 f1f 6560 . . . . . . . . . . . . . . . . . . 19 (𝑢:dom 𝑢1-1𝐷𝑢:dom 𝑢𝐷)
86 frn 6504 . . . . . . . . . . . . . . . . . . 19 (𝑢:dom 𝑢𝐷 → ran 𝑢𝐷)
8784, 85, 863syl 18 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ran 𝑢𝐷)
8887ad3antrrr 729 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢𝐷)
8914, 16prssd 4712 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
90 ssconb 4043 . . . . . . . . . . . . . . . . . 18 (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})))
9190biimpa 480 . . . . . . . . . . . . . . . . 17 ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
9218, 88, 89, 91syl21anc 836 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
9314, 16s2rn 30742 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
9493difeq2d 4028 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
9592, 94sseqtrrd 3933 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
9695resabs1d 5854 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
9795resabs1d 5854 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
9875, 96, 973eqtr3d 2801 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
9971, 98eqtr3d 2795 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
100 simp-4r 783 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑀𝑢) = 𝑇)
101100reseq1d 5822 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑇 ↾ (𝐷 ∖ ran 𝑢)))
10283simpld 498 . . . . . . . . . . . . . . 15 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ Word 𝐷)
103102ad3antrrr 729 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑢 ∈ Word 𝐷)
10484ad3antrrr 729 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑢:dom 𝑢1-1𝐷)
10564, 10, 103, 104tocycfvres2 30904 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106101, 105eqtr3d 2795 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
107 disjdif 4368 . . . . . . . . . . . . 13 (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
108107a1i 11 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
109 undif 4378 . . . . . . . . . . . . 13 (ran 𝑢𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
11088, 109sylib 221 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
11126, 27, 39, 69, 99, 106, 108, 110symgcom 30878 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
112111coeq2d 5702 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
113 cyc3conja.p . . . . . . . . . . . . . . 15 + = (+g𝑆)
11426, 27, 113symgov 18579 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
11511, 39, 114syl2anc 587 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
11626, 27, 113symgcl 18580 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
11711, 39, 116syl2anc 587 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
118115, 117eqeltrrd 2853 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
11926, 27, 113symgov 18579 . . . . . . . . . . . 12 (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
120118, 69, 119syl2anc 587 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
121 coass 6095 . . . . . . . . . . 11 ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
122120, 121eqtrdi 2809 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
123 coass 6095 . . . . . . . . . . 11 ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
124123a1i 11 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
125112, 122, 1243eqtr4d 2803 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
126 cnvco 5725 . . . . . . . . . 10 (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)
127126a1i 11 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔))
128125, 127coeq12d 5704 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)))
129 coass 6095 . . . . . . . . . 10 ((((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑔) = (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔))
130 coass 6095 . . . . . . . . . . 11 (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
131130coeq1i 5699 . . . . . . . . . 10 ((((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑔) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔)
132129, 131eqtr3i 2783 . . . . . . . . 9 (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔)
133132a1i 11 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔))
13426, 27, 113symgov 18579 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔𝑇))
13511, 69, 134syl2anc 587 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + 𝑇) = (𝑔𝑇))
13626, 27, 113symgcl 18580 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
13711, 69, 136syl2anc 587 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
138135, 137eqeltrrd 2853 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔𝑇) ∈ (Base‘𝑆))
13926, 27symgbasf 18571 . . . . . . . . . . . 12 ((𝑔𝑇) ∈ (Base‘𝑆) → (𝑔𝑇):𝐷𝐷)
140 fcoi1 6537 . . . . . . . . . . . 12 ((𝑔𝑇):𝐷𝐷 → ((𝑔𝑇) ∘ ( I ↾ 𝐷)) = (𝑔𝑇))
141138, 139, 1403syl 18 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ ( I ↾ 𝐷)) = (𝑔𝑇))
14226, 27elsymgbas 18569 . . . . . . . . . . . . . . 15 (𝐷 ∈ Fin → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆) ↔ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷))
143142biimpa 480 . . . . . . . . . . . . . 14 ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷)
14410, 39, 143syl2anc 587 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷)
145 f1ococnv2 6628 . . . . . . . . . . . . 13 (((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷 → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
146144, 145syl 17 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
147146coeq2d 5702 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔𝑇) ∘ ( I ↾ 𝐷)))
148141, 147, 1353eqtr4d 2803 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
149148coeq1d 5701 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
150 cyc3conja.l . . . . . . . . . . 11 = (-g𝑆)
15126, 27, 150symgsubg 30882 . . . . . . . . . 10 (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
152137, 11, 151syl2anc 587 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 + 𝑇) 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
153149, 152eqtr4d 2796 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔) = ((𝑔 + 𝑇) 𝑔))
154128, 133, 1533eqtrd 2797 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) 𝑔))
15526symggrp 18595 . . . . . . . . . . 11 (𝐷 ∈ Fin → 𝑆 ∈ Grp)
1568, 155syl 17 . . . . . . . . . 10 (𝜑𝑆 ∈ Grp)
157156ad8antr 739 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑆 ∈ Grp)
15827, 113grpcl 18177 . . . . . . . . 9 ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
159157, 118, 69, 158syl3anc 1368 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
16026, 27, 150symgsubg 30882 . . . . . . . 8 ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
161159, 118, 160syl2anc 587 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
162 simp-7r 789 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑄 = ((𝑔 + 𝑇) 𝑔))
163154, 161, 1623eqtr4rd 2804 . . . . . 6 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
16434, 38, 163rspcedvd 3544 . . . . 5 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
165 difexg 5197 . . . . . . . 8 (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ V)
1668, 165syl 17 . . . . . . 7 (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
167166ad5antr 733 . . . . . 6 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
168 3p2e5 11825 . . . . . . . . . . 11 (3 + 2) = 5
169168, 59eqbrtrid 5067 . . . . . . . . . 10 (𝜑 → (3 + 2) ≤ 𝑁)
170 2re 11748 . . . . . . . . . . . 12 2 ∈ ℝ
171170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
17249, 171, 55leaddsub2d 11280 . . . . . . . . . 10 (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3)))
173169, 172mpbid 235 . . . . . . . . 9 (𝜑 → 2 ≤ (𝑁 − 3))
174173ad5antr 733 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ (𝑁 − 3))
17541a1i 11 . . . . . . . . 9 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑁 = (♯‘𝐷))
17676elin2d 4104 . . . . . . . . . . 11 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ (♯ “ {3}))
177 hashf 13748 . . . . . . . . . . . . 13 ♯:V⟶(ℕ0 ∪ {+∞})
178 ffn 6498 . . . . . . . . . . . . 13 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
179 fniniseg 6821 . . . . . . . . . . . . 13 (♯ Fn V → (𝑢 ∈ (♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3)))
180177, 178, 179mp2b 10 . . . . . . . . . . . 12 (𝑢 ∈ (♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3))
181180simprbi 500 . . . . . . . . . . 11 (𝑢 ∈ (♯ “ {3}) → (♯‘𝑢) = 3)
182176, 181syl 17 . . . . . . . . . 10 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘𝑢) = 3)
183 vex 3413 . . . . . . . . . . . 12 𝑢 ∈ V
184183dmex 7621 . . . . . . . . . . 11 dom 𝑢 ∈ V
185 hashf1rn 13763 . . . . . . . . . . 11 ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢1-1𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
186184, 84, 185sylancr 590 . . . . . . . . . 10 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢))
187182, 186eqtr3d 2795 . . . . . . . . 9 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
188175, 187oveq12d 7168 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
189174, 188breqtrd 5058 . . . . . . 7 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
190 hashssdif 13823 . . . . . . . 8 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
1919, 87, 190syl2anc 587 . . . . . . 7 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
192189, 191breqtrrd 5060 . . . . . 6 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
193 hashge2el2dif 13890 . . . . . 6 (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥𝑦)
194167, 192, 193syl2anc 587 . . . . 5 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥𝑦)
195164, 194r19.29vva 3257 . . . 4 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
196 nfcv 2919 . . . . . 6 𝑢𝑀
19764, 26, 27tocycf 30910 . . . . . . 7 (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
198 ffn 6498 . . . . . . 7 (𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆) → 𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
1998, 197, 1983syl 18 . . . . . 6 (𝜑𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
20067, 63eleqtrdi 2862 . . . . . 6 (𝜑𝑇 ∈ (𝑀 “ (♯ “ {3})))
201196, 199, 200fvelimad 6720 . . . . 5 (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))(𝑀𝑢) = 𝑇)
202201ad3antrrr 729 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))(𝑀𝑢) = 𝑇)
203195, 202r19.29a 3213 . . 3 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
2047, 203pm2.61dan 812 . 2 (((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
205 cyc3conja.q . . 3 (𝜑𝑄𝐶)
20663, 26, 41, 64, 27, 113, 150, 62, 8, 205, 67cycpmconjs 30949 . 2 (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) 𝑔))
207204, 206r19.29a 3213 1 (𝜑 → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071  {crab 3074  Vcvv 3409   ∖ cdif 3855   ∪ cun 3856   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  {csn 4522  {cpr 4524   class class class wbr 5032   I cid 5429  ◡ccnv 5523  dom cdm 5524  ran crn 5525   ↾ cres 5526   “ cima 5527   ∘ ccom 5528   Fn wfn 6330  ⟶wf 6331  –1-1→wf1 6332  –1-1-onto→wf1o 6334  ‘cfv 6335  (class class class)co 7150  2oc2o 8106   ≈ cen 8524  Fincfn 8527  ℝcr 10574  0cc0 10575   + caddc 10578  +∞cpnf 10710   < clt 10713   ≤ cle 10714   − cmin 10908  2c2 11729  3c3 11730  5c5 11732  ℕ0cn0 11934  ℤcz 12020  ...cfz 12939  ♯chash 13740  Word cword 13913  ⟨“cs2 14250  Basecbs 16541  +gcplusg 16623  Grpcgrp 18169  -gcsg 18171  SymGrpcsymg 18562  pmTrspcpmtr 18636  pmEvencevpm 18685  toCycctocyc 30899 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-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654  ax-mulf 10655 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-xor 1503  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-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-ot 4531  df-uni 4799  df-int 4839  df-iun 4885  df-iin 4886  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-tpos 7902  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-oadd 8116  df-er 8299  df-map 8418  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-inf 8940  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-xnn0 12007  df-z 12021  df-dec 12138  df-uz 12283  df-rp 12431  df-fz 12940  df-fzo 13083  df-fl 13211  df-mod 13287  df-seq 13419  df-exp 13480  df-hash 13741  df-word 13914  df-lsw 13962  df-concat 13970  df-s1 13997  df-substr 14050  df-pfx 14080  df-splice 14159  df-reverse 14168  df-csh 14198  df-s2 14257  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-mulr 16637  df-starv 16638  df-tset 16642  df-ple 16643  df-ds 16645  df-unif 16646  df-0g 16773  df-gsum 16774  df-mre 16915  df-mrc 16916  df-acs 16918  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-mhm 18022  df-submnd 18023  df-efmnd 18100  df-grp 18172  df-minusg 18173  df-sbg 18174  df-subg 18343  df-ghm 18423  df-gim 18466  df-oppg 18541  df-symg 18563  df-pmtr 18637  df-psgn 18686  df-evpm 18687  df-cmn 18975  df-abl 18976  df-mgp 19308  df-ur 19320  df-ring 19367  df-cring 19368  df-oppr 19444  df-dvdsr 19462  df-unit 19463  df-invr 19493  df-dvr 19504  df-drng 19572  df-cnfld 20167  df-tocyc 30900 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator