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

Theorem cyc3conja 30713
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 485 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → 𝑔𝐴)
2 simpr 485 . . . . . . 7 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → 𝑝 = 𝑔)
32oveq1d 7166 . . . . . 6 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
43, 2oveq12d 7169 . . . . 5 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) 𝑝) = ((𝑔 + 𝑇) 𝑔))
54eqeq2d 2836 . . . 4 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) 𝑔)))
6 simplr 765 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → 𝑄 = ((𝑔 + 𝑇) 𝑔))
71, 5, 6rspcedvd 3629 . . 3 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
8 cyc3conja.d . . . . . . . . 9 (𝜑𝐷 ∈ Fin)
98ad5antr 730 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝐷 ∈ Fin)
109ad3antrrr 726 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝐷 ∈ Fin)
11 simp-8r 788 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑔 ∈ (Base‘𝑆))
12 simp-6r 784 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ¬ 𝑔𝐴)
1311, 12eldifd 3950 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴))
14 simpllr 772 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥 ∈ (𝐷 ∖ ran 𝑢))
1514eldifad 3951 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥𝐷)
16 simplr 765 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑦 ∈ (𝐷 ∖ ran 𝑢))
1716eldifad 3951 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑦𝐷)
1815, 17prssd 4753 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19 simpr 485 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥𝑦)
20 pr2nelem 9422 . . . . . . . . . . 11 ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥𝑦) → {𝑥, 𝑦} ≈ 2o)
2114, 16, 19, 20syl3anc 1365 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ≈ 2o)
22 eqid 2825 . . . . . . . . . . 11 (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23 eqid 2825 . . . . . . . . . . 11 ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
2422, 23pmtrrn 18507 . . . . . . . . . 10 ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
2510, 18, 21, 24syl3anc 1365 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26 cyc3conja.s . . . . . . . . . 10 𝑆 = (SymGrp‘𝐷)
27 eqid 2825 . . . . . . . . . 10 (Base‘𝑆) = (Base‘𝑆)
2826, 27, 23pmtrodpm 20657 . . . . . . . . 9 ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
2910, 25, 28syl2anc 584 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
30 cyc3conja.a . . . . . . . . 9 𝐴 = (pmEven‘𝐷)
3130difeq2i 4099 . . . . . . . 8 ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
3229, 31syl6eleqr 2928 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
3326, 27, 30odpmco 30644 . . . . . . 7 ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
3410, 13, 32, 33syl3anc 1365 . . . . . 6 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
35 simpr 485 . . . . . . . . 9 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
3635oveq1d 7166 . . . . . . . 8 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
3736, 35oveq12d 7169 . . . . . . 7 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
3837eqeq2d 2836 . . . . . 6 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
3929eldifad 3951 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40 0zd 11985 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
41 cyc3conja.n . . . . . . . . . . . . . . . . . 18 𝑁 = (♯‘𝐷)
42 hashcl 13710 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0)
438, 42syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘𝐷) ∈ ℕ0)
4441, 43eqeltrid 2921 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ0)
4544nn0zd 12077 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
46 3z 12007 . . . . . . . . . . . . . . . . 17 3 ∈ ℤ
4746a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ∈ ℤ)
48 0red 10636 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
4947zred 12079 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ∈ ℝ)
50 3pos 11734 . . . . . . . . . . . . . . . . . 18 0 < 3
5150a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 3)
5248, 49, 51ltled 10780 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 3)
53 5re 11716 . . . . . . . . . . . . . . . . . 18 5 ∈ ℝ
5453a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℝ)
5544nn0red 11948 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℝ)
56 3lt5 11807 . . . . . . . . . . . . . . . . . . 19 3 < 5
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 3 < 5)
5849, 54, 57ltled 10780 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≤ 5)
59 cyc3conja.1 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ≤ 𝑁)
6049, 54, 55, 58, 59letrd 10789 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ≤ 𝑁)
61 elfz4 12894 . . . . . . . . . . . . . . . 16 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (0 ≤ 3 ∧ 3 ≤ 𝑁)) → 3 ∈ (0...𝑁))
6240, 45, 47, 52, 60, 61syl32anc 1372 . . . . . . . . . . . . . . 15 (𝜑 → 3 ∈ (0...𝑁))
63 cyc3conja.c . . . . . . . . . . . . . . . 16 𝐶 = (𝑀 “ (♯ “ {3}))
64 cyc3conja.m . . . . . . . . . . . . . . . 16 𝑀 = (toCyc‘𝐷)
6563, 26, 41, 64, 27cycpmgcl 30709 . . . . . . . . . . . . . . 15 ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
668, 62, 65syl2anc 584 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ (Base‘𝑆))
67 cyc3conja.t . . . . . . . . . . . . . 14 (𝜑𝑇𝐶)
6866, 67sseldd 3971 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (Base‘𝑆))
6968ad8antr 736 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑇 ∈ (Base‘𝑆))
7064, 10, 15, 17, 19, 22cycpm2tr 30675 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
7170reseq1d 5850 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
7215, 17s2cld 14226 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
7315, 17, 19s2f1 30535 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1𝐷)
7464, 10, 72, 73tocycfvres2 30667 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
7574reseq1d 5850 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢))
76 simplr 765 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3})))
7776elin1d 4178 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
78 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢𝑤 = 𝑢)
79 dmeq 5770 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
80 eqidd 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢𝐷 = 𝐷)
8178, 79, 80f1eq123d 6604 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
8281elrab 3683 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
8377, 82sylib 219 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
8483simprd 496 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢:dom 𝑢1-1𝐷)
85 f1f 6571 . . . . . . . . . . . . . . . . . . 19 (𝑢:dom 𝑢1-1𝐷𝑢:dom 𝑢𝐷)
86 frn 6516 . . . . . . . . . . . . . . . . . . 19 (𝑢:dom 𝑢𝐷 → ran 𝑢𝐷)
8784, 85, 863syl 18 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ran 𝑢𝐷)
8887ad3antrrr 726 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢𝐷)
8914, 16prssd 4753 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
90 ssconb 4117 . . . . . . . . . . . . . . . . . 18 (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})))
9190biimpa 477 . . . . . . . . . . . . . . . . 17 ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
9218, 88, 89, 91syl21anc 835 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
9314, 16s2rn 30534 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
9493difeq2d 4102 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
9592, 94sseqtrrd 4011 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
9695resabs1d 5882 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
9795resabs1d 5882 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
9875, 96, 973eqtr3d 2868 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
9971, 98eqtr3d 2862 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
100 simp-4r 780 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑀𝑢) = 𝑇)
101100reseq1d 5850 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑇 ↾ (𝐷 ∖ ran 𝑢)))
10283simpld 495 . . . . . . . . . . . . . . 15 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ Word 𝐷)
103102ad3antrrr 726 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑢 ∈ Word 𝐷)
10484ad3antrrr 726 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑢:dom 𝑢1-1𝐷)
10564, 10, 103, 104tocycfvres2 30667 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106101, 105eqtr3d 2862 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
107 disjdif 4423 . . . . . . . . . . . . 13 (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
108107a1i 11 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
109 undif 4432 . . . . . . . . . . . . 13 (ran 𝑢𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
11088, 109sylib 219 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
11126, 27, 39, 69, 99, 106, 108, 110symgcom 30641 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
112111coeq2d 5731 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
113 cyc3conja.p . . . . . . . . . . . . . . 15 + = (+g𝑆)
11426, 27, 113symgov 18440 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
11511, 39, 114syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
11626, 27, 113symgcl 18441 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
11711, 39, 116syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
118115, 117eqeltrrd 2918 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
11926, 27, 113symgov 18440 . . . . . . . . . . . 12 (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
120118, 69, 119syl2anc 584 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
121 coass 6115 . . . . . . . . . . 11 ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
122120, 121syl6eq 2876 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
123 coass 6115 . . . . . . . . . . 11 ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
124123a1i 11 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
125112, 122, 1243eqtr4d 2870 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
126 cnvco 5754 . . . . . . . . . 10 (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)
127126a1i 11 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔))
128125, 127coeq12d 5733 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)))
129 coass 6115 . . . . . . . . . 10 ((((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑔) = (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔))
130 coass 6115 . . . . . . . . . . 11 (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
131130coeq1i 5728 . . . . . . . . . 10 ((((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑔) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔)
132129, 131eqtr3i 2850 . . . . . . . . 9 (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔)
133132a1i 11 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔))
13426, 27, 113symgov 18440 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔𝑇))
13511, 69, 134syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + 𝑇) = (𝑔𝑇))
13626, 27, 113symgcl 18441 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
13711, 69, 136syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
138135, 137eqeltrrd 2918 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔𝑇) ∈ (Base‘𝑆))
13926, 27symgbasf 18434 . . . . . . . . . . . 12 ((𝑔𝑇) ∈ (Base‘𝑆) → (𝑔𝑇):𝐷𝐷)
140 fcoi1 6548 . . . . . . . . . . . 12 ((𝑔𝑇):𝐷𝐷 → ((𝑔𝑇) ∘ ( I ↾ 𝐷)) = (𝑔𝑇))
141138, 139, 1403syl 18 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ ( I ↾ 𝐷)) = (𝑔𝑇))
14226, 27elsymgbas 18432 . . . . . . . . . . . . . . 15 (𝐷 ∈ Fin → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆) ↔ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷))
143142biimpa 477 . . . . . . . . . . . . . 14 ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷)
14410, 39, 143syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷)
145 f1ococnv2 6637 . . . . . . . . . . . . 13 (((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷 → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
146144, 145syl 17 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
147146coeq2d 5731 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔𝑇) ∘ ( I ↾ 𝐷)))
148141, 147, 1353eqtr4d 2870 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
149148coeq1d 5730 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
150 cyc3conja.l . . . . . . . . . . 11 = (-g𝑆)
15126, 27, 150symgsubg 30645 . . . . . . . . . 10 (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
152137, 11, 151syl2anc 584 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 + 𝑇) 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
153149, 152eqtr4d 2863 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔) = ((𝑔 + 𝑇) 𝑔))
154128, 133, 1533eqtrd 2864 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) 𝑔))
15526symggrp 18450 . . . . . . . . . . 11 (𝐷 ∈ Fin → 𝑆 ∈ Grp)
1568, 155syl 17 . . . . . . . . . 10 (𝜑𝑆 ∈ Grp)
157156ad8antr 736 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑆 ∈ Grp)
15827, 113grpcl 18043 . . . . . . . . 9 ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
159157, 118, 69, 158syl3anc 1365 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
16026, 27, 150symgsubg 30645 . . . . . . . 8 ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
161159, 118, 160syl2anc 584 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
162 simp-7r 786 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑄 = ((𝑔 + 𝑇) 𝑔))
163154, 161, 1623eqtr4rd 2871 . . . . . 6 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
16434, 38, 163rspcedvd 3629 . . . . 5 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
165 difexg 5227 . . . . . . . 8 (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ V)
1668, 165syl 17 . . . . . . 7 (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
167166ad5antr 730 . . . . . 6 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
168 3p2e5 11780 . . . . . . . . . . 11 (3 + 2) = 5
169168, 59eqbrtrid 5097 . . . . . . . . . 10 (𝜑 → (3 + 2) ≤ 𝑁)
170 2re 11703 . . . . . . . . . . . 12 2 ∈ ℝ
171170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
17249, 171, 55leaddsub2d 11234 . . . . . . . . . 10 (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3)))
173169, 172mpbid 233 . . . . . . . . 9 (𝜑 → 2 ≤ (𝑁 − 3))
174173ad5antr 730 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ (𝑁 − 3))
17541a1i 11 . . . . . . . . 9 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑁 = (♯‘𝐷))
17676elin2d 4179 . . . . . . . . . . 11 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ (♯ “ {3}))
177 hashf 13691 . . . . . . . . . . . . 13 ♯:V⟶(ℕ0 ∪ {+∞})
178 ffn 6510 . . . . . . . . . . . . 13 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
179 fniniseg 6825 . . . . . . . . . . . . 13 (♯ Fn V → (𝑢 ∈ (♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3)))
180177, 178, 179mp2b 10 . . . . . . . . . . . 12 (𝑢 ∈ (♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3))
181180simprbi 497 . . . . . . . . . . 11 (𝑢 ∈ (♯ “ {3}) → (♯‘𝑢) = 3)
182176, 181syl 17 . . . . . . . . . 10 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘𝑢) = 3)
183 vex 3502 . . . . . . . . . . . 12 𝑢 ∈ V
184183dmex 7607 . . . . . . . . . . 11 dom 𝑢 ∈ V
185 hashf1rn 13706 . . . . . . . . . . 11 ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢1-1𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
186184, 84, 185sylancr 587 . . . . . . . . . 10 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢))
187182, 186eqtr3d 2862 . . . . . . . . 9 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
188175, 187oveq12d 7169 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
189174, 188breqtrd 5088 . . . . . . 7 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
190 hashssdif 13766 . . . . . . . 8 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
1919, 87, 190syl2anc 584 . . . . . . 7 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
192189, 191breqtrrd 5090 . . . . . 6 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
193 hashge2el2dif 13831 . . . . . 6 (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥𝑦)
194167, 192, 193syl2anc 584 . . . . 5 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥𝑦)
195164, 194r19.29vva 3340 . . . 4 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
196 nfcv 2981 . . . . . 6 𝑢𝑀
19764, 26, 27tocycf 30673 . . . . . . 7 (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
198 ffn 6510 . . . . . . 7 (𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆) → 𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
1998, 197, 1983syl 18 . . . . . 6 (𝜑𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
20067, 63syl6eleq 2927 . . . . . 6 (𝜑𝑇 ∈ (𝑀 “ (♯ “ {3})))
201196, 199, 200fvelimad 6728 . . . . 5 (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))(𝑀𝑢) = 𝑇)
202201ad3antrrr 726 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))(𝑀𝑢) = 𝑇)
203195, 202r19.29a 3293 . . 3 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
2047, 203pm2.61dan 809 . 2 (((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
205 cyc3conja.q . . 3 (𝜑𝑄𝐶)
20663, 26, 41, 64, 27, 113, 150, 62, 8, 205, 67cycpmconjs 30712 . 2 (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) 𝑔))
207204, 206r19.29a 3293 1 (𝜑 → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1530  wcel 2107  wne 3020  wrex 3143  {crab 3146  Vcvv 3499  cdif 3936  cun 3937  cin 3938  wss 3939  c0 4294  {csn 4563  {cpr 4565   class class class wbr 5062   I cid 5457  ccnv 5552  dom cdm 5553  ran crn 5554  cres 5555  cima 5556  ccom 5557   Fn wfn 6346  wf 6347  1-1wf1 6348  1-1-ontowf1o 6350  cfv 6351  (class class class)co 7151  2oc2o 8090  cen 8498  Fincfn 8501  cr 10528  0cc0 10529   + caddc 10532  +∞cpnf 10664   < clt 10667  cle 10668  cmin 10862  2c2 11684  3c3 11685  5c5 11687  0cn0 11889  cz 11973  ...cfz 12885  chash 13683  Word cword 13854  ⟨“cs2 14196  Basecbs 16475  +gcplusg 16557  Grpcgrp 18035  -gcsg 18037  SymGrpcsymg 18427  pmTrspcpmtr 18491  pmEvencevpm 18540  toCycctocyc 30662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-xor 1498  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-ot 4572  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-tpos 7886  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12383  df-fz 12886  df-fzo 13027  df-fl 13155  df-mod 13231  df-seq 13363  df-exp 13423  df-hash 13684  df-word 13855  df-lsw 13908  df-concat 13916  df-s1 13943  df-substr 13996  df-pfx 14026  df-splice 14105  df-reverse 14114  df-csh 14144  df-s2 14203  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-gsum 16708  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-mhm 17946  df-submnd 17947  df-grp 18038  df-minusg 18039  df-sbg 18040  df-subg 18208  df-ghm 18288  df-gim 18331  df-oppg 18406  df-symg 18428  df-pmtr 18492  df-psgn 18541  df-evpm 18542  df-cmn 18830  df-abl 18831  df-mgp 19162  df-ur 19174  df-ring 19221  df-cring 19222  df-oppr 19295  df-dvdsr 19313  df-unit 19314  df-invr 19344  df-dvr 19355  df-drng 19426  df-cnfld 20462  df-tocyc 30663
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator