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 33178

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 7447	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
4	3, 2	oveq12d 7450	. . . . 5 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) − 𝑝) = ((𝑔 + 𝑇) − 𝑔))
5	4	eqeq2d 2747	. . . 4 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) − 𝑔)))
6		simplr 768	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
7	1, 5, 6	rspcedvd 3623	. . 3 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
8		cyc3conja.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ Fin)
9	8	ad5antr 734	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝐷 ∈ Fin)
10	9	ad3antrrr 730	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝐷 ∈ Fin)
11		simp-8r 791	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑔 ∈ (Base‘𝑆))
12		simp-6r 787	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑔 ∈ 𝐴)
13	11, 12	eldifd 3961	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴))
14		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ (𝐷 ∖ ran 𝑢))
15	14	eldifad 3962	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ 𝐷)
16		simplr 768	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ (𝐷 ∖ ran 𝑢))
17	16	eldifad 3962	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ 𝐷)
18	15, 17	prssd 4821	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19		simpr 484	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
20		enpr2 10043	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
21	14, 16, 19, 20	syl3anc 1372	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
22		eqid 2736	. . . . . . . . . . 11 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23		eqid 2736	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
24	22, 23	pmtrrn 19476	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2_o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
25	10, 18, 21, 24	syl3anc 1372	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26		cyc3conja.s	. . . . . . . . . 10 ⊢ 𝑆 = (SymGrp‘𝐷)
27		eqid 2736	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
28	26, 27, 23	pmtrodpm 21616	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
29	10, 25, 28	syl2anc 584	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
30		cyc3conja.a	. . . . . . . . 9 ⊢ 𝐴 = (pmEven‘𝐷)
31	30	difeq2i 4122	. . . . . . . 8 ⊢ ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
32	29, 31	eleqtrrdi 2851	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
33	26, 27, 30	odpmco 33107	. . . . . . 7 ⊢ ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
34	10, 13, 32, 33	syl3anc 1372	. . . . . 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 7447	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
37	36, 35	oveq12d 7450	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) − 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
38	37	eqeq2d 2747	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
39	29	eldifad 3962	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40		0zd 12627	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℤ)
41		cyc3conja.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐷)
42		hashcl 14396	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
43	8, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
44	41, 43	eqeltrid 2844	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
45	44	nn0zd 12641	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46		3z 12652	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℤ
47	46	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ∈ ℤ)
48		0red 11265	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
49	47	zred 12724	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ∈ ℝ)
50		3pos 12372	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 3
51	50	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 3)
52	48, 49, 51	ltled 11410	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ 3)
53		5re 12354	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℝ
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℝ)
55	44	nn0red 12590	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
56		3lt5 12445	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 5
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 3 < 5)
58	49, 54, 57	ltled 11410	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≤ 5)
59		cyc3conja.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ≤ 𝑁)
60	49, 54, 55, 58, 59	letrd 11419	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ≤ 𝑁)
61	40, 45, 47, 52, 60	elfzd 13556	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ (0...𝑁))
62		cyc3conja.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝑀 “ (^◡♯ “ {3}))
63		cyc3conja.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (toCyc‘𝐷)
64	62, 26, 41, 63, 27	cycpmgcl 33174	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
65	8, 61, 64	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝑆))
66		cyc3conja.t	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ 𝐶)
67	65, 66	sseldd 3983	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (Base‘𝑆))
68	67	ad8antr 740	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑇 ∈ (Base‘𝑆))
69	63, 10, 15, 17, 19, 22	cycpm2tr 33140	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
70	69	reseq1d 5995	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
71	15, 17	s2cld 14911	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
72	15, 17, 19	s2f1 32930	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1→𝐷)
73	63, 10, 71, 72	tocycfvres2 33132	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
74	73	reseq1d 5995	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢))
75		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3})))
76	75	elin1d 4203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
77		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
78		dmeq 5913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
79		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
80	77, 78, 79	f1eq123d 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
81	80	elrab 3691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
82	76, 81	sylib 218	. . . . . . . . . . . . . . . . . . . 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 6803	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢⟶𝐷)
85		frn 6742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢⟶𝐷 → ran 𝑢 ⊆ 𝐷)
86	83, 84, 85	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ran 𝑢 ⊆ 𝐷)
87	86	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ 𝐷)
88	14, 16	prssd 4821	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
89		ssconb 4141	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})))
90	89	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
91	18, 87, 88, 90	syl21anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
92	14, 16	s2rn 15003	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
93	92	difeq2d 4125	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
94	91, 93	sseqtrrd 4020	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
95	94	resabs1d 6025	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
96	94	resabs1d 6025	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
97	74, 95, 96	3eqtr3d 2784	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
98	70, 97	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
99		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘𝑢) = 𝑇)
100	99	reseq1d 5995	. . . . . . . . . . . . 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 730	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢 ∈ Word 𝐷)
103	83	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢:dom 𝑢–1-1→𝐷)
104	63, 10, 102, 103	tocycfvres2 33132	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
105	100, 104	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106		disjdif 4471	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
107	106	a1i 11	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
108		undif 4481	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
109	87, 108	sylib 218	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
110	26, 27, 39, 68, 98, 105, 107, 109	symgcom 33104	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
111	110	coeq2d 5872	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
112		cyc3conja.p	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑆)
113	26, 27, 112	symgov 19402	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
114	11, 39, 113	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
115	26, 27, 112	symgcl 19403	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
116	11, 39, 115	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
117	114, 116	eqeltrrd 2841	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
118	26, 27, 112	symgov 19402	. . . . . . . . . . . 12 ⊢ (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
119	117, 68, 118	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
120		coass 6284	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
121	119, 120	eqtrdi 2792	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
122		coass 6284	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
124	111, 121, 123	3eqtr4d 2786	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
125		cnvco 5895	. . . . . . . . . 10 ⊢ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)
126	125	a1i 11	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
127	124, 126	coeq12d 5874	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)))
128		coass 6284	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
129		coass 6284	. . . . . . . . . . 11 ⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
130	129	coeq1i 5869	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔)
131	128, 130	eqtr3i 2766	. . . . . . . . 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 19402	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
134	11, 68, 133	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
135	26, 27, 112	symgcl 19403	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
136	11, 68, 135	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
137	134, 136	eqeltrrd 2841	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ 𝑇) ∈ (Base‘𝑆))
138	26, 27	symgbasf 19394	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇) ∈ (Base‘𝑆) → (𝑔 ∘ 𝑇):𝐷⟶𝐷)
139		fcoi1 6781	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇):𝐷⟶𝐷 → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
140	137, 138, 139	3syl 18	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
141	26, 27	elsymgbas 19392	. . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷)
144		f1ococnv2 6874	. . . . . . . . . . . . 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 5872	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)))
147	140, 146, 134	3eqtr4d 2786	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
148	147	coeq1d 5871	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
149		cyc3conja.l	. . . . . . . . . . 11 ⊢ − = (-_g‘𝑆)
150	26, 27, 149	symgsubg 33108	. . . . . . . . . 10 ⊢ (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
151	136, 11, 150	syl2anc 584	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
152	148, 151	eqtr4d 2779	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) − 𝑔))
153	127, 132, 152	3eqtrd 2780	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) − 𝑔))
154	26	symggrp 19419	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → 𝑆 ∈ Grp)
155	8, 154	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Grp)
156	155	ad8antr 740	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑆 ∈ Grp)
157	27, 112	grpcl 18960	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
158	156, 117, 68, 157	syl3anc 1372	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
159	26, 27, 149	symgsubg 33108	. . . . . . . 8 ⊢ ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
160	158, 117, 159	syl2anc 584	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
161		simp-7r 789	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
162	153, 160, 161	3eqtr4rd 2787	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
163	34, 38, 162	rspcedvd 3623	. . . . 5 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
164	8	difexd 5330	. . . . . . 7 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
165	164	ad5antr 734	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
166		3p2e5 12418	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
167	166, 59	eqbrtrid 5177	. . . . . . . . . 10 ⊢ (𝜑 → (3 + 2) ≤ 𝑁)
168		2re 12341	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
170	49, 169, 55	leaddsub2d 11866	. . . . . . . . . 10 ⊢ (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3)))
171	167, 170	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 2 ≤ (𝑁 − 3))
172	171	ad5antr 734	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (𝑁 − 3))
173	41	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑁 = (♯‘𝐷))
174	75	elin2d 4204	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ (^◡♯ “ {3}))
175		hashf 14378	. . . . . . . . . . . . 13 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
176		ffn 6735	. . . . . . . . . . . . 13 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
177		fniniseg 7079	. . . . . . . . . . . . 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 3483	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
182	181	dmex 7932	. . . . . . . . . . 11 ⊢ dom 𝑢 ∈ V
183		hashf1rn 14392	. . . . . . . . . . 11 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
184	182, 83, 183	sylancr 587	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢))
185	180, 184	eqtr3d 2778	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
186	173, 185	oveq12d 7450	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
187	172, 186	breqtrd 5168	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
188		hashssdif 14452	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
189	9, 86, 188	syl2anc 584	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
190	187, 189	breqtrrd 5170	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
191		hashge2el2dif 14520	. . . . . 6 ⊢ (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦)
192	165, 190, 191	syl2anc 584	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦)
193	163, 192	r19.29vva 3215	. . . 4 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
194		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑢𝑀
195	63, 26, 27	tocycf 33138	. . . . . . 7 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆))
196		ffn 6735	. . . . . . 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 2850	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (𝑀 “ (^◡♯ “ {3})))
199	194, 197, 198	fvelimad 6975	. . . . 5 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
200	199	ad3antrrr 730	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
201	193, 200	r19.29a 3161	. . 3 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
202	7, 201	pm2.61dan 812	. 2 ⊢ (((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
203		cyc3conja.q	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
204	62, 26, 41, 63, 27, 112, 149, 61, 8, 203, 66	cycpmconjs 33177	. 2 ⊢ (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) − 𝑔))
205	202, 204	r19.29a 3161	1 ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∃wrex 3069 {crab 3435 Vcvv 3479 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 ⊆ wss 3950 ∅c0 4332 {csn 4625 {cpr 4627 class class class wbr 5142 I cid 5576 ^◡ccnv 5683 dom cdm 5684 ran crn 5685 ↾ cres 5686 “ cima 5687 ∘ ccom 5688 Fn wfn 6555 ⟶wf 6556 –1-1→wf1 6557 –1-1-onto→wf1o 6559 ‘cfv 6560 (class class class)co 7432 2_oc2o 8501 ≈ cen 8983 Fincfn 8986 ℝcr 11155 0cc0 11156 + caddc 11159 +∞cpnf 11293 < clt 11296 ≤ cle 11297 − cmin 11493 2c2 12322 3c3 12323 5c5 12325 ℕ₀cn0 12528 ℤcz 12615 ...cfz 13548 ♯chash 14370 Word cword 14553 ⟨“cs2 14881 Basecbs 17248 +_gcplusg 17298 Grpcgrp 18952 -_gcsg 18954 SymGrpcsymg 19387 pmTrspcpmtr 19460 pmEvencevpm 19509 toCycctocyc 33127

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234 ax-addf 11235 ax-mulf 11236

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-xor 1511 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-ot 4634 df-uni 4907 df-int 4946 df-iun 4992 df-iin 4993 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-tpos 8252 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-oadd 8511 df-er 8746 df-map 8869 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-sup 9483 df-inf 9484 df-dju 9942 df-card 9980 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12529 df-xnn0 12602 df-z 12616 df-dec 12736 df-uz 12880 df-rp 13036 df-fz 13549 df-fzo 13696 df-fl 13833 df-mod 13911 df-seq 14044 df-exp 14104 df-hash 14371 df-word 14554 df-lsw 14602 df-concat 14610 df-s1 14635 df-substr 14680 df-pfx 14710 df-splice 14789 df-reverse 14798 df-csh 14828 df-s2 14888 df-struct 17185 df-sets 17202 df-slot 17220 df-ndx 17232 df-base 17249 df-ress 17276 df-plusg 17311 df-mulr 17312 df-starv 17313 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-0g 17487 df-gsum 17488 df-mre 17630 df-mrc 17631 df-acs 17633 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-mhm 18797 df-submnd 18798 df-efmnd 18883 df-grp 18955 df-minusg 18956 df-sbg 18957 df-subg 19142 df-ghm 19232 df-gim 19278 df-oppg 19365 df-symg 19388 df-pmtr 19461 df-psgn 19510 df-evpm 19511 df-cmn 19801 df-abl 19802 df-mgp 20139 df-rng 20151 df-ur 20180 df-ring 20233 df-cring 20234 df-oppr 20335 df-dvdsr 20358 df-unit 20359 df-invr 20389 df-dvr 20402 df-drng 20732 df-cnfld 21366 df-tocyc 33128

This theorem is referenced by: (None)

W3C validator