cyc3conja - Mathbox for Thierry Arnoux

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

Theorem cyc3conja 31326

Description: All 3-cycles are conjugate in the alternating group A_n 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.

Step	Hyp	Ref	Expression
1		simpr 484	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝐴)
2		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → 𝑝 = 𝑔)
3	2	oveq1d 7270	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
4	3, 2	oveq12d 7273	. . . . 5 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) − 𝑝) = ((𝑔 + 𝑇) − 𝑔))
5	4	eqeq2d 2749	. . . 4 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) − 𝑔)))
6		simplr 765	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
7	1, 5, 6	rspcedvd 3555	. . 3 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
8		cyc3conja.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ Fin)
9	8	ad5antr 730	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝐷 ∈ Fin)
10	9	ad3antrrr 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 𝑢)) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑔 ∈ 𝐴)
13	11, 12	eldifd 3894	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴))
14		simpllr 772	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ (𝐷 ∖ ran 𝑢))
15	14	eldifad 3895	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ 𝐷)
16		simplr 765	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ (𝐷 ∖ ran 𝑢))
17	16	eldifad 3895	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ 𝐷)
18	15, 17	prssd 4752	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19		simpr 484	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
20		pr2nelem 9691	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
21	14, 16, 19, 20	syl3anc 1369	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
22		eqid 2738	. . . . . . . . . . 11 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23		eqid 2738	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
24	22, 23	pmtrrn 18980	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2_o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
25	10, 18, 21, 24	syl3anc 1369	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26		cyc3conja.s	. . . . . . . . . 10 ⊢ 𝑆 = (SymGrp‘𝐷)
27		eqid 2738	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
28	26, 27, 23	pmtrodpm 20714	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
29	10, 25, 28	syl2anc 583	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
30		cyc3conja.a	. . . . . . . . 9 ⊢ 𝐴 = (pmEven‘𝐷)
31	30	difeq2i 4050	. . . . . . . 8 ⊢ ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
32	29, 31	eleqtrrdi 2850	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
33	26, 27, 30	odpmco 31257	. . . . . . 7 ⊢ ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
34	10, 13, 32, 33	syl3anc 1369	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
35		simpr 484	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
36	35	oveq1d 7270	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
37	36, 35	oveq12d 7273	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) − 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
38	37	eqeq2d 2749	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
39	29	eldifad 3895	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40		0zd 12261	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℤ)
41		cyc3conja.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐷)
42		hashcl 13999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
43	8, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
44	41, 43	eqeltrid 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
45	44	nn0zd 12353	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46		3z 12283	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℤ
47	46	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ∈ ℤ)
48		0red 10909	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
49	47	zred 12355	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ∈ ℝ)
50		3pos 12008	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 3
51	50	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 3)
52	48, 49, 51	ltled 11053	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ 3)
53		5re 11990	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℝ
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℝ)
55	44	nn0red 12224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
56		3lt5 12081	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 5
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 3 < 5)
58	49, 54, 57	ltled 11053	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≤ 5)
59		cyc3conja.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ≤ 𝑁)
60	49, 54, 55, 58, 59	letrd 11062	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ≤ 𝑁)
61	40, 45, 47, 52, 60	elfzd 13176	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ (0...𝑁))
62		cyc3conja.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝑀 “ (^◡♯ “ {3}))
63		cyc3conja.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (toCyc‘𝐷)
64	62, 26, 41, 63, 27	cycpmgcl 31322	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
65	8, 61, 64	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝑆))
66		cyc3conja.t	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ 𝐶)
67	65, 66	sseldd 3918	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (Base‘𝑆))
68	67	ad8antr 736	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑇 ∈ (Base‘𝑆))
69	63, 10, 15, 17, 19, 22	cycpm2tr 31288	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
70	69	reseq1d 5879	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
71	15, 17	s2cld 14512	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
72	15, 17, 19	s2f1 31121	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1→𝐷)
73	63, 10, 71, 72	tocycfvres2 31280	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
74	73	reseq1d 5879	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢))
75		simplr 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3})))
76	75	elin1d 4128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
77		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
78		dmeq 5801	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
79		eqidd 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
80	77, 78, 79	f1eq123d 6692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
81	80	elrab 3617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
82	76, 81	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
83	82	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢:dom 𝑢–1-1→𝐷)
84		f1f 6654	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢⟶𝐷)
85		frn 6591	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢⟶𝐷 → ran 𝑢 ⊆ 𝐷)
86	83, 84, 85	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ran 𝑢 ⊆ 𝐷)
87	86	ad3antrrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ 𝐷)
88	14, 16	prssd 4752	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
89		ssconb 4068	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})))
90	89	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
91	18, 87, 88, 90	syl21anc 834	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
92	14, 16	s2rn 31120	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
93	92	difeq2d 4053	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
94	91, 93	sseqtrrd 3958	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
95	94	resabs1d 5911	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
96	94	resabs1d 5911	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
97	74, 95, 96	3eqtr3d 2786	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
98	70, 97	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
99		simp-4r 780	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘𝑢) = 𝑇)
100	99	reseq1d 5879	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑇 ↾ (𝐷 ∖ ran 𝑢)))
101	82	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ Word 𝐷)
102	101	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢 ∈ Word 𝐷)
103	83	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢:dom 𝑢–1-1→𝐷)
104	63, 10, 102, 103	tocycfvres2 31280	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
105	100, 104	eqtr3d 2780	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106		disjdif 4402	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
107	106	a1i 11	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
108		undif 4412	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
109	87, 108	sylib 217	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
110	26, 27, 39, 68, 98, 105, 107, 109	symgcom 31254	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
111	110	coeq2d 5760	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
112		cyc3conja.p	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑆)
113	26, 27, 112	symgov 18906	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
114	11, 39, 113	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
115	26, 27, 112	symgcl 18907	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
116	11, 39, 115	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
117	114, 116	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
118	26, 27, 112	symgov 18906	. . . . . . . . . . . 12 ⊢ (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
119	117, 68, 118	syl2anc 583	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
120		coass 6158	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
121	119, 120	eqtrdi 2795	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
122		coass 6158	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
124	111, 121, 123	3eqtr4d 2788	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
125		cnvco 5783	. . . . . . . . . 10 ⊢ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)
126	125	a1i 11	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
127	124, 126	coeq12d 5762	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)))
128		coass 6158	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
129		coass 6158	. . . . . . . . . . 11 ⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
130	129	coeq1i 5757	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔)
131	128, 130	eqtr3i 2768	. . . . . . . . 9 ⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔)
132	131	a1i 11	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔))
133	26, 27, 112	symgov 18906	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
134	11, 68, 133	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
135	26, 27, 112	symgcl 18907	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
136	11, 68, 135	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
137	134, 136	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ 𝑇) ∈ (Base‘𝑆))
138	26, 27	symgbasf 18898	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇) ∈ (Base‘𝑆) → (𝑔 ∘ 𝑇):𝐷⟶𝐷)
139		fcoi1 6632	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇):𝐷⟶𝐷 → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
140	137, 138, 139	3syl 18	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
141	26, 27	elsymgbas 18896	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ Fin → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆) ↔ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷))
142	141	biimpa 476	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷)
143	10, 39, 142	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷)
144		f1ococnv2 6726	. . . . . . . . . . . . 13 ⊢ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷 → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
145	143, 144	syl 17	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
146	145	coeq2d 5760	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)))
147	140, 146, 134	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
148	147	coeq1d 5759	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
149		cyc3conja.l	. . . . . . . . . . 11 ⊢ − = (-_g‘𝑆)
150	26, 27, 149	symgsubg 31258	. . . . . . . . . 10 ⊢ (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
151	136, 11, 150	syl2anc 583	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
152	148, 151	eqtr4d 2781	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) − 𝑔))
153	127, 132, 152	3eqtrd 2782	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) − 𝑔))
154	26	symggrp 18923	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → 𝑆 ∈ Grp)
155	8, 154	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Grp)
156	155	ad8antr 736	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑆 ∈ Grp)
157	27, 112	grpcl 18500	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
158	156, 117, 68, 157	syl3anc 1369	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
159	26, 27, 149	symgsubg 31258	. . . . . . . 8 ⊢ ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
160	158, 117, 159	syl2anc 583	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
161		simp-7r 786	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
162	153, 160, 161	3eqtr4rd 2789	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
163	34, 38, 162	rspcedvd 3555	. . . . 5 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
164	8	difexd 5248	. . . . . . 7 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
165	164	ad5antr 730	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
166		3p2e5 12054	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
167	166, 59	eqbrtrid 5105	. . . . . . . . . 10 ⊢ (𝜑 → (3 + 2) ≤ 𝑁)
168		2re 11977	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
170	49, 169, 55	leaddsub2d 11507	. . . . . . . . . 10 ⊢ (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3)))
171	167, 170	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → 2 ≤ (𝑁 − 3))
172	171	ad5antr 730	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (𝑁 − 3))
173	41	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑁 = (♯‘𝐷))
174	75	elin2d 4129	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ (^◡♯ “ {3}))
175		hashf 13980	. . . . . . . . . . . . 13 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
176		ffn 6584	. . . . . . . . . . . . 13 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
177		fniniseg 6919	. . . . . . . . . . . . 13 ⊢ (♯ Fn V → (𝑢 ∈ (^◡♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3)))
178	175, 176, 177	mp2b 10	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (^◡♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3))
179	178	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (^◡♯ “ {3}) → (♯‘𝑢) = 3)
180	174, 179	syl 17	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = 3)
181		vex 3426	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
182	181	dmex 7732	. . . . . . . . . . 11 ⊢ dom 𝑢 ∈ V
183		hashf1rn 13995	. . . . . . . . . . 11 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
184	182, 83, 183	sylancr 586	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢))
185	180, 184	eqtr3d 2780	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
186	173, 185	oveq12d 7273	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
187	172, 186	breqtrd 5096	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
188		hashssdif 14055	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
189	9, 86, 188	syl2anc 583	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
190	187, 189	breqtrrd 5098	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
191		hashge2el2dif 14122	. . . . . 6 ⊢ (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦)
192	165, 190, 191	syl2anc 583	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦)
193	163, 192	r19.29vva 3263	. . . 4 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
194		nfcv 2906	. . . . . 6 ⊢ Ⅎ𝑢𝑀
195	63, 26, 27	tocycf 31286	. . . . . . 7 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆))
196		ffn 6584	. . . . . . 7 ⊢ (𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆) → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
197	8, 195, 196	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
198	66, 62	eleqtrdi 2849	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (𝑀 “ (^◡♯ “ {3})))
199	194, 197, 198	fvelimad 6818	. . . . 5 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
200	199	ad3antrrr 726	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
201	193, 200	r19.29a 3217	. . 3 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
202	7, 201	pm2.61dan 809	. 2 ⊢ (((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
203		cyc3conja.q	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
204	62, 26, 41, 63, 27, 112, 149, 61, 8, 203, 66	cycpmconjs 31325	. 2 ⊢ (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) − 𝑔))
205	202, 204	r19.29a 3217	1 ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 {crab 3067 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 {csn 4558 {cpr 4560 class class class wbr 5070 I cid 5479 ^◡ccnv 5579 dom cdm 5580 ran crn 5581 ↾ cres 5582 “ cima 5583 ∘ ccom 5584 Fn wfn 6413 ⟶wf 6414 –1-1→wf1 6415 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 2_oc2o 8261 ≈ cen 8688 Fincfn 8691 ℝcr 10801 0cc0 10802 + caddc 10805 +∞cpnf 10937 < clt 10940 ≤ cle 10941 − cmin 11135 2c2 11958 3c3 11959 5c5 11961 ℕ₀cn0 12163 ℤcz 12249 ...cfz 13168 ♯chash 13972 Word cword 14145 ⟨“cs2 14482 Basecbs 16840 +_gcplusg 16888 Grpcgrp 18492 -_gcsg 18494 SymGrpcsymg 18889 pmTrspcpmtr 18964 pmEvencevpm 19013 toCycctocyc 31275

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-xor 1504 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-ot 4567 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-tpos 8013 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-xnn0 12236 df-z 12250 df-dec 12367 df-uz 12512 df-rp 12660 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-hash 13973 df-word 14146 df-lsw 14194 df-concat 14202 df-s1 14229 df-substr 14282 df-pfx 14312 df-splice 14391 df-reverse 14400 df-csh 14430 df-s2 14489 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-0g 17069 df-gsum 17070 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-mhm 18345 df-submnd 18346 df-efmnd 18423 df-grp 18495 df-minusg 18496 df-sbg 18497 df-subg 18667 df-ghm 18747 df-gim 18790 df-oppg 18865 df-symg 18890 df-pmtr 18965 df-psgn 19014 df-evpm 19015 df-cmn 19303 df-abl 19304 df-mgp 19636 df-ur 19653 df-ring 19700 df-cring 19701 df-oppr 19777 df-dvdsr 19798 df-unit 19799 df-invr 19829 df-dvr 19840 df-drng 19908 df-cnfld 20511 df-tocyc 31276

This theorem is referenced by: (None)

W3C validator