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 33160
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 484 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → 𝑔𝐴)
2 simpr 484 . . . . . . 7 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → 𝑝 = 𝑔)
32oveq1d 7446 . . . . . 6 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
43, 2oveq12d 7449 . . . . 5 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) 𝑝) = ((𝑔 + 𝑇) 𝑔))
54eqeq2d 2746 . . . 4 (((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) 𝑔)))
6 simplr 769 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → 𝑄 = ((𝑔 + 𝑇) 𝑔))
71, 5, 6rspcedvd 3624 . . 3 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ 𝑔𝐴) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
8 cyc3conja.d . . . . . . . . 9 (𝜑𝐷 ∈ Fin)
98ad5antr 734 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝐷 ∈ Fin)
109ad3antrrr 730 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝐷 ∈ Fin)
11 simp-8r 792 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑔 ∈ (Base‘𝑆))
12 simp-6r 788 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ¬ 𝑔𝐴)
1311, 12eldifd 3974 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴))
14 simpllr 776 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥 ∈ (𝐷 ∖ ran 𝑢))
1514eldifad 3975 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥𝐷)
16 simplr 769 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑦 ∈ (𝐷 ∖ ran 𝑢))
1716eldifad 3975 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑦𝐷)
1815, 17prssd 4827 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19 simpr 484 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑥𝑦)
20 enpr2 10040 . . . . . . . . . . 11 ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥𝑦) → {𝑥, 𝑦} ≈ 2o)
2114, 16, 19, 20syl3anc 1370 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ≈ 2o)
22 eqid 2735 . . . . . . . . . . 11 (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23 eqid 2735 . . . . . . . . . . 11 ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
2422, 23pmtrrn 19490 . . . . . . . . . 10 ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
2510, 18, 21, 24syl3anc 1370 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26 cyc3conja.s . . . . . . . . . 10 𝑆 = (SymGrp‘𝐷)
27 eqid 2735 . . . . . . . . . 10 (Base‘𝑆) = (Base‘𝑆)
2826, 27, 23pmtrodpm 21633 . . . . . . . . 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 4133 . . . . . . . 8 ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
3229, 31eleqtrrdi 2850 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
3326, 27, 30odpmco 33089 . . . . . . 7 ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
3410, 13, 32, 33syl3anc 1370 . . . . . 6 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
35 simpr 484 . . . . . . . . 9 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
3635oveq1d 7446 . . . . . . . 8 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
3736, 35oveq12d 7449 . . . . . . 7 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
3837eqeq2d 2746 . . . . . 6 ((((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
3929eldifad 3975 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40 0zd 12623 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
41 cyc3conja.n . . . . . . . . . . . . . . . . . 18 𝑁 = (♯‘𝐷)
42 hashcl 14392 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0)
438, 42syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘𝐷) ∈ ℕ0)
4441, 43eqeltrid 2843 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ0)
4544nn0zd 12637 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
46 3z 12648 . . . . . . . . . . . . . . . . 17 3 ∈ ℤ
4746a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ∈ ℤ)
48 0red 11262 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
4947zred 12720 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ∈ ℝ)
50 3pos 12369 . . . . . . . . . . . . . . . . . 18 0 < 3
5150a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 3)
5248, 49, 51ltled 11407 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 3)
53 5re 12351 . . . . . . . . . . . . . . . . . 18 5 ∈ ℝ
5453a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℝ)
5544nn0red 12586 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℝ)
56 3lt5 12442 . . . . . . . . . . . . . . . . . . 19 3 < 5
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 3 < 5)
5849, 54, 57ltled 11407 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ≤ 5)
59 cyc3conja.1 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ≤ 𝑁)
6049, 54, 55, 58, 59letrd 11416 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ≤ 𝑁)
6140, 45, 47, 52, 60elfzd 13552 . . . . . . . . . . . . . . 15 (𝜑 → 3 ∈ (0...𝑁))
62 cyc3conja.c . . . . . . . . . . . . . . . 16 𝐶 = (𝑀 “ (♯ “ {3}))
63 cyc3conja.m . . . . . . . . . . . . . . . 16 𝑀 = (toCyc‘𝐷)
6462, 26, 41, 63, 27cycpmgcl 33156 . . . . . . . . . . . . . . 15 ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
658, 61, 64syl2anc 584 . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ (Base‘𝑆))
66 cyc3conja.t . . . . . . . . . . . . . 14 (𝜑𝑇𝐶)
6765, 66sseldd 3996 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (Base‘𝑆))
6867ad8antr 740 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑇 ∈ (Base‘𝑆))
6963, 10, 15, 17, 19, 22cycpm2tr 33122 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
7069reseq1d 5999 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
7115, 17s2cld 14907 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
7215, 17, 19s2f1 32914 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1𝐷)
7363, 10, 71, 72tocycfvres2 33114 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
7473reseq1d 5999 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢))
75 simplr 769 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3})))
7675elin1d 4214 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
77 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢𝑤 = 𝑢)
78 dmeq 5917 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
79 eqidd 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑢𝐷 = 𝐷)
8077, 78, 79f1eq123d 6841 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑢 → (𝑤:dom 𝑤1-1𝐷𝑢:dom 𝑢1-1𝐷))
8180elrab 3695 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ↔ (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
8276, 81sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝑢 ∈ Word 𝐷𝑢:dom 𝑢1-1𝐷))
8382simprd 495 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢:dom 𝑢1-1𝐷)
84 f1f 6805 . . . . . . . . . . . . . . . . . . 19 (𝑢:dom 𝑢1-1𝐷𝑢:dom 𝑢𝐷)
85 frn 6744 . . . . . . . . . . . . . . . . . . 19 (𝑢:dom 𝑢𝐷 → ran 𝑢𝐷)
8683, 84, 853syl 18 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ran 𝑢𝐷)
8786ad3antrrr 730 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢𝐷)
8814, 16prssd 4827 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
89 ssconb 4152 . . . . . . . . . . . . . . . . . 18 (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})))
9089biimpa 476 . . . . . . . . . . . . . . . . 17 ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
9118, 87, 88, 90syl21anc 838 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
9214, 16s2rn 14999 . . . . . . . . . . . . . . . . 17 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
9392difeq2d 4136 . . . . . . . . . . . . . . . 16 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
9491, 93sseqtrrd 4037 . . . . . . . . . . . . . . 15 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
9594resabs1d 6028 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
9694resabs1d 6028 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
9774, 95, 963eqtr3d 2783 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
9870, 97eqtr3d 2777 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
99 simp-4r 784 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑀𝑢) = 𝑇)
10099reseq1d 5999 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑇 ↾ (𝐷 ∖ ran 𝑢)))
10182simpld 494 . . . . . . . . . . . . . . 15 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ Word 𝐷)
102101ad3antrrr 730 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑢 ∈ Word 𝐷)
10383ad3antrrr 730 . . . . . . . . . . . . . 14 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑢:dom 𝑢1-1𝐷)
10463, 10, 102, 103tocycfvres2 33114 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑀𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
105100, 104eqtr3d 2777 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106 disjdif 4478 . . . . . . . . . . . . 13 (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
107106a1i 11 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
108 undif 4488 . . . . . . . . . . . . 13 (ran 𝑢𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
10987, 108sylib 218 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
11026, 27, 39, 68, 98, 105, 107, 109symgcom 33086 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
111110coeq2d 5876 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
112 cyc3conja.p . . . . . . . . . . . . . . 15 + = (+g𝑆)
11326, 27, 112symgov 19416 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
11411, 39, 113syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
11526, 27, 112symgcl 19417 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
11611, 39, 115syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
117114, 116eqeltrrd 2840 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
11826, 27, 112symgov 19416 . . . . . . . . . . . 12 (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
119117, 68, 118syl2anc 584 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
120 coass 6287 . . . . . . . . . . 11 ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
121119, 120eqtrdi 2791 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
122 coass 6287 . . . . . . . . . . 11 ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
123122a1i 11 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
124111, 121, 1233eqtr4d 2785 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
125 cnvco 5899 . . . . . . . . . 10 (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)
126125a1i 11 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔))
127124, 126coeq12d 5878 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)))
128 coass 6287 . . . . . . . . . 10 ((((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑔) = (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔))
129 coass 6287 . . . . . . . . . . 11 (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
130129coeq1i 5873 . . . . . . . . . 10 ((((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑔) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔)
131128, 130eqtr3i 2765 . . . . . . . . 9 (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔)
132131a1i 11 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑔)) = (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔))
13326, 27, 112symgov 19416 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔𝑇))
13411, 68, 133syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + 𝑇) = (𝑔𝑇))
13526, 27, 112symgcl 19417 . . . . . . . . . . . . . 14 ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
13611, 68, 135syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
137134, 136eqeltrrd 2840 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (𝑔𝑇) ∈ (Base‘𝑆))
13826, 27symgbasf 19408 . . . . . . . . . . . 12 ((𝑔𝑇) ∈ (Base‘𝑆) → (𝑔𝑇):𝐷𝐷)
139 fcoi1 6783 . . . . . . . . . . . 12 ((𝑔𝑇):𝐷𝐷 → ((𝑔𝑇) ∘ ( I ↾ 𝐷)) = (𝑔𝑇))
140137, 138, 1393syl 18 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ ( I ↾ 𝐷)) = (𝑔𝑇))
14126, 27elsymgbas 19406 . . . . . . . . . . . . . . 15 (𝐷 ∈ Fin → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆) ↔ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷))
142141biimpa 476 . . . . . . . . . . . . . 14 ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷)
14310, 39, 142syl2anc 584 . . . . . . . . . . . . 13 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷)
144 f1ococnv2 6876 . . . . . . . . . . . . 13 (((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷1-1-onto𝐷 → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
145143, 144syl 17 . . . . . . . . . . . 12 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
146145coeq2d 5876 . . . . . . . . . . 11 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔𝑇) ∘ ( I ↾ 𝐷)))
147140, 146, 1343eqtr4d 2785 . . . . . . . . . 10 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
148147coeq1d 5875 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
149 cyc3conja.l . . . . . . . . . . 11 = (-g𝑆)
15026, 27, 149symgsubg 33090 . . . . . . . . . 10 (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
151136, 11, 150syl2anc 584 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 + 𝑇) 𝑔) = ((𝑔 + 𝑇) ∘ 𝑔))
152148, 151eqtr4d 2778 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ 𝑔) = ((𝑔 + 𝑇) 𝑔))
153127, 132, 1523eqtrd 2779 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) 𝑔))
15426symggrp 19433 . . . . . . . . . . 11 (𝐷 ∈ Fin → 𝑆 ∈ Grp)
1558, 154syl 17 . . . . . . . . . 10 (𝜑𝑆 ∈ Grp)
156155ad8antr 740 . . . . . . . . 9 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑆 ∈ Grp)
15727, 112grpcl 18972 . . . . . . . . 9 ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
158156, 117, 68, 157syl3anc 1370 . . . . . . . 8 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
15926, 27, 149symgsubg 33090 . . . . . . . 8 ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
160158, 117, 159syl2anc 584 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
161 simp-7r 790 . . . . . . 7 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑄 = ((𝑔 + 𝑇) 𝑔))
162153, 160, 1613eqtr4rd 2786 . . . . . 6 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
16334, 38, 162rspcedvd 3624 . . . . 5 (((((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥𝑦) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
1648difexd 5337 . . . . . . 7 (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
165164ad5antr 734 . . . . . 6 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
166 3p2e5 12415 . . . . . . . . . . 11 (3 + 2) = 5
167166, 59eqbrtrid 5183 . . . . . . . . . 10 (𝜑 → (3 + 2) ≤ 𝑁)
168 2re 12338 . . . . . . . . . . . 12 2 ∈ ℝ
169168a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℝ)
17049, 169, 55leaddsub2d 11863 . . . . . . . . . 10 (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3)))
171167, 170mpbid 232 . . . . . . . . 9 (𝜑 → 2 ≤ (𝑁 − 3))
172171ad5antr 734 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ (𝑁 − 3))
17341a1i 11 . . . . . . . . 9 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑁 = (♯‘𝐷))
17475elin2d 4215 . . . . . . . . . . 11 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 𝑢 ∈ (♯ “ {3}))
175 hashf 14374 . . . . . . . . . . . . 13 ♯:V⟶(ℕ0 ∪ {+∞})
176 ffn 6737 . . . . . . . . . . . . 13 (♯:V⟶(ℕ0 ∪ {+∞}) → ♯ Fn V)
177 fniniseg 7080 . . . . . . . . . . . . 13 (♯ Fn V → (𝑢 ∈ (♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3)))
178175, 176, 177mp2b 10 . . . . . . . . . . . 12 (𝑢 ∈ (♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3))
179178simprbi 496 . . . . . . . . . . 11 (𝑢 ∈ (♯ “ {3}) → (♯‘𝑢) = 3)
180174, 179syl 17 . . . . . . . . . 10 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘𝑢) = 3)
181 vex 3482 . . . . . . . . . . . 12 𝑢 ∈ V
182181dmex 7932 . . . . . . . . . . 11 dom 𝑢 ∈ V
183 hashf1rn 14388 . . . . . . . . . . 11 ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢1-1𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
184182, 83, 183sylancr 587 . . . . . . . . . 10 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢))
185180, 184eqtr3d 2777 . . . . . . . . 9 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
186173, 185oveq12d 7449 . . . . . . . 8 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
187172, 186breqtrd 5174 . . . . . . 7 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
188 hashssdif 14448 . . . . . . . 8 ((𝐷 ∈ Fin ∧ ran 𝑢𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
1899, 86, 188syl2anc 584 . . . . . . 7 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
190187, 189breqtrrd 5176 . . . . . 6 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
191 hashge2el2dif 14516 . . . . . 6 (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥𝑦)
192165, 190, 191syl2anc 584 . . . . 5 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥𝑦)
193163, 192r19.29vva 3214 . . . 4 ((((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))) ∧ (𝑀𝑢) = 𝑇) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
194 nfcv 2903 . . . . . 6 𝑢𝑀
19563, 26, 27tocycf 33120 . . . . . . 7 (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆))
196 ffn 6737 . . . . . . 7 (𝑀:{𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷}⟶(Base‘𝑆) → 𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
1978, 195, 1963syl 18 . . . . . 6 (𝜑𝑀 Fn {𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷})
19866, 62eleqtrdi 2849 . . . . . 6 (𝜑𝑇 ∈ (𝑀 “ (♯ “ {3})))
199194, 197, 198fvelimad 6976 . . . . 5 (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))(𝑀𝑢) = 𝑇)
200199ad3antrrr 730 . . . 4 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷𝑤:dom 𝑤1-1𝐷} ∩ (♯ “ {3}))(𝑀𝑢) = 𝑇)
201193, 200r19.29a 3160 . . 3 ((((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) ∧ ¬ 𝑔𝐴) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
2027, 201pm2.61dan 813 . 2 (((𝜑𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) 𝑔)) → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
203 cyc3conja.q . . 3 (𝜑𝑄𝐶)
20462, 26, 41, 63, 27, 112, 149, 61, 8, 203, 66cycpmconjs 33159 . 2 (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) 𝑔))
205202, 204r19.29a 3160 1 (𝜑 → ∃𝑝𝐴 𝑄 = ((𝑝 + 𝑇) 𝑝))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wne 2938  wrex 3068  {crab 3433  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  {csn 4631  {cpr 4633   class class class wbr 5148   I cid 5582  ccnv 5688  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  ccom 5693   Fn wfn 6558  wf 6559  1-1wf1 6560  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  2oc2o 8499  cen 8981  Fincfn 8984  cr 11152  0cc0 11153   + caddc 11156  +∞cpnf 11290   < clt 11293  cle 11294  cmin 11490  2c2 12319  3c3 12320  5c5 12322  0cn0 12524  cz 12611  ...cfz 13544  chash 14366  Word cword 14549  ⟨“cs2 14877  Basecbs 17245  +gcplusg 17298  Grpcgrp 18964  -gcsg 18966  SymGrpcsymg 19401  pmTrspcpmtr 19474  pmEvencevpm 19523  toCycctocyc 33109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232  ax-mulf 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-xor 1509  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-dju 9939  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-xnn0 12598  df-z 12612  df-dec 12732  df-uz 12877  df-rp 13033  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-hash 14367  df-word 14550  df-lsw 14598  df-concat 14606  df-s1 14631  df-substr 14676  df-pfx 14706  df-splice 14785  df-reverse 14794  df-csh 14824  df-s2 14884  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-0g 17488  df-gsum 17489  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-mhm 18809  df-submnd 18810  df-efmnd 18895  df-grp 18967  df-minusg 18968  df-sbg 18969  df-subg 19154  df-ghm 19244  df-gim 19290  df-oppg 19377  df-symg 19402  df-pmtr 19475  df-psgn 19524  df-evpm 19525  df-cmn 19815  df-abl 19816  df-mgp 20153  df-rng 20171  df-ur 20200  df-ring 20253  df-cring 20254  df-oppr 20351  df-dvdsr 20374  df-unit 20375  df-invr 20405  df-dvr 20418  df-drng 20748  df-cnfld 21383  df-tocyc 33110
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator