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 33087

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 7384	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
4	3, 2	oveq12d 7387	. . . . 5 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) − 𝑝) = ((𝑔 + 𝑇) − 𝑔))
5	4	eqeq2d 2740	. . . 4 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) − 𝑔)))
6		simplr 768	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
7	1, 5, 6	rspcedvd 3587	. . 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 3922	. . . . . . 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 3923	. . . . . . . . . . 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 3923	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ 𝐷)
18	15, 17	prssd 4782	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19		simpr 484	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
20		enpr2 9931	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
21	14, 16, 19, 20	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
22		eqid 2729	. . . . . . . . . . 11 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23		eqid 2729	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
24	22, 23	pmtrrn 19363	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2_o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
25	10, 18, 21, 24	syl3anc 1373	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26		cyc3conja.s	. . . . . . . . . 10 ⊢ 𝑆 = (SymGrp‘𝐷)
27		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
28	26, 27, 23	pmtrodpm 21482	. . . . . . . . 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 4082	. . . . . . . 8 ⊢ ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
32	29, 31	eleqtrrdi 2839	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
33	26, 27, 30	odpmco 33016	. . . . . . 7 ⊢ ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
34	10, 13, 32, 33	syl3anc 1373	. . . . . 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 7384	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
37	36, 35	oveq12d 7387	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) − 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
38	37	eqeq2d 2740	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
39	29	eldifad 3923	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40		0zd 12517	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℤ)
41		cyc3conja.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐷)
42		hashcl 14297	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
43	8, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
44	41, 43	eqeltrid 2832	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
45	44	nn0zd 12531	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46		3z 12542	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℤ
47	46	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ∈ ℤ)
48		0red 11153	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
49	47	zred 12614	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ∈ ℝ)
50		3pos 12267	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 3
51	50	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 3)
52	48, 49, 51	ltled 11298	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ 3)
53		5re 12249	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℝ
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℝ)
55	44	nn0red 12480	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
56		3lt5 12335	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 5
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 3 < 5)
58	49, 54, 57	ltled 11298	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≤ 5)
59		cyc3conja.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ≤ 𝑁)
60	49, 54, 55, 58, 59	letrd 11307	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ≤ 𝑁)
61	40, 45, 47, 52, 60	elfzd 13452	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ (0...𝑁))
62		cyc3conja.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝑀 “ (^◡♯ “ {3}))
63		cyc3conja.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (toCyc‘𝐷)
64	62, 26, 41, 63, 27	cycpmgcl 33083	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
65	8, 61, 64	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝑆))
66		cyc3conja.t	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ 𝐶)
67	65, 66	sseldd 3944	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (Base‘𝑆))
68	67	ad8antr 740	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑇 ∈ (Base‘𝑆))
69	63, 10, 15, 17, 19, 22	cycpm2tr 33049	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
70	69	reseq1d 5938	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
71	15, 17	s2cld 14813	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
72	15, 17, 19	s2f1 32839	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1→𝐷)
73	63, 10, 71, 72	tocycfvres2 33041	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
74	73	reseq1d 5938	. . . . . . . . . . . . . 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 4163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
77		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
78		dmeq 5857	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
79		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
80	77, 78, 79	f1eq123d 6774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
81	80	elrab 3656	. . . . . . . . . . . . . . . . . . . . 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 6738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢⟶𝐷)
85		frn 6677	. . . . . . . . . . . . . . . . . . 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 4782	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
89		ssconb 4101	. . . . . . . . . . . . . . . . . 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 14905	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
93	92	difeq2d 4085	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
94	91, 93	sseqtrrd 3981	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
95	94	resabs1d 5968	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
96	94	resabs1d 5968	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
97	74, 95, 96	3eqtr3d 2772	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
98	70, 97	eqtr3d 2766	. . . . . . . . . . . 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 5938	. . . . . . . . . . . . 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 33041	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
105	100, 104	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106		disjdif 4431	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
107	106	a1i 11	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
108		undif 4441	. . . . . . . . . . . . 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 33013	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
111	110	coeq2d 5816	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
112		cyc3conja.p	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑆)
113	26, 27, 112	symgov 19290	. . . . . . . . . . . . . 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 19291	. . . . . . . . . . . . . 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 2829	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
118	26, 27, 112	symgov 19290	. . . . . . . . . . . 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 6226	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
121	119, 120	eqtrdi 2780	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
122		coass 6226	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
124	111, 121, 123	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
125		cnvco 5839	. . . . . . . . . 10 ⊢ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)
126	125	a1i 11	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
127	124, 126	coeq12d 5818	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)))
128		coass 6226	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
129		coass 6226	. . . . . . . . . . 11 ⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
130	129	coeq1i 5813	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔)
131	128, 130	eqtr3i 2754	. . . . . . . . 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 19290	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
134	11, 68, 133	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
135	26, 27, 112	symgcl 19291	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
136	11, 68, 135	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
137	134, 136	eqeltrrd 2829	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ 𝑇) ∈ (Base‘𝑆))
138	26, 27	symgbasf 19282	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇) ∈ (Base‘𝑆) → (𝑔 ∘ 𝑇):𝐷⟶𝐷)
139		fcoi1 6716	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇):𝐷⟶𝐷 → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
140	137, 138, 139	3syl 18	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
141	26, 27	elsymgbas 19280	. . . . . . . . . . . . . . 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 6809	. . . . . . . . . . . . 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 5816	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)))
147	140, 146, 134	3eqtr4d 2774	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
148	147	coeq1d 5815	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
149		cyc3conja.l	. . . . . . . . . . 11 ⊢ − = (-_g‘𝑆)
150	26, 27, 149	symgsubg 33017	. . . . . . . . . 10 ⊢ (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
151	136, 11, 150	syl2anc 584	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
152	148, 151	eqtr4d 2767	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) − 𝑔))
153	127, 132, 152	3eqtrd 2768	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) − 𝑔))
154	26	symggrp 19306	. . . . . . . . . . 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 18849	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
158	156, 117, 68, 157	syl3anc 1373	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
159	26, 27, 149	symgsubg 33017	. . . . . . . 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 2775	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
163	34, 38, 162	rspcedvd 3587	. . . . 5 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
164	8	difexd 5281	. . . . . . 7 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
165	164	ad5antr 734	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
166		3p2e5 12308	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
167	166, 59	eqbrtrid 5137	. . . . . . . . . 10 ⊢ (𝜑 → (3 + 2) ≤ 𝑁)
168		2re 12236	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
169	168	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
170	49, 169, 55	leaddsub2d 11756	. . . . . . . . . 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 4164	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ (^◡♯ “ {3}))
175		hashf 14279	. . . . . . . . . . . . 13 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
176		ffn 6670	. . . . . . . . . . . . 13 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
177		fniniseg 7014	. . . . . . . . . . . . 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 3448	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
182	181	dmex 7865	. . . . . . . . . . 11 ⊢ dom 𝑢 ∈ V
183		hashf1rn 14293	. . . . . . . . . . 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 2766	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
186	173, 185	oveq12d 7387	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
187	172, 186	breqtrd 5128	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
188		hashssdif 14353	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
189	9, 86, 188	syl2anc 584	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
190	187, 189	breqtrrd 5130	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
191		hashge2el2dif 14421	. . . . . 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 3195	. . . 4 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
194		nfcv 2891	. . . . . 6 ⊢ Ⅎ𝑢𝑀
195	63, 26, 27	tocycf 33047	. . . . . . 7 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆))
196		ffn 6670	. . . . . . 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 2838	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (𝑀 “ (^◡♯ “ {3})))
199	194, 197, 198	fvelimad 6910	. . . . 5 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
200	199	ad3antrrr 730	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
201	193, 200	r19.29a 3141	. . 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 33086	. 2 ⊢ (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) − 𝑔))
205	202, 204	r19.29a 3141	1 ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 {crab 3402 Vcvv 3444 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 {csn 4585 {cpr 4587 class class class wbr 5102 I cid 5525 ^◡ccnv 5630 dom cdm 5631 ran crn 5632 ↾ cres 5633 “ cima 5634 ∘ ccom 5635 Fn wfn 6494 ⟶wf 6495 –1-1→wf1 6496 –1-1-onto→wf1o 6498 ‘cfv 6499 (class class class)co 7369 2_oc2o 8405 ≈ cen 8892 Fincfn 8895 ℝcr 11043 0cc0 11044 + caddc 11047 +∞cpnf 11181 < clt 11184 ≤ cle 11185 − cmin 11381 2c2 12217 3c3 12218 5c5 12220 ℕ₀cn0 12418 ℤcz 12505 ...cfz 13444 ♯chash 14271 Word cword 14454 ⟨“cs2 14783 Basecbs 17155 +_gcplusg 17196 Grpcgrp 18841 -_gcsg 18843 SymGrpcsymg 19275 pmTrspcpmtr 19347 pmEvencevpm 19396 toCycctocyc 33036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122 ax-addf 11123 ax-mulf 11124

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-xor 1512 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-ot 4594 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-tpos 8182 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-oadd 8415 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-inf 9370 df-dju 9830 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-6 12229 df-7 12230 df-8 12231 df-9 12232 df-n0 12419 df-xnn0 12492 df-z 12506 df-dec 12626 df-uz 12770 df-rp 12928 df-fz 13445 df-fzo 13592 df-fl 13730 df-mod 13808 df-seq 13943 df-exp 14003 df-hash 14272 df-word 14455 df-lsw 14504 df-concat 14512 df-s1 14537 df-substr 14582 df-pfx 14612 df-splice 14691 df-reverse 14700 df-csh 14730 df-s2 14790 df-struct 17093 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-starv 17211 df-tset 17215 df-ple 17216 df-ds 17218 df-unif 17219 df-0g 17380 df-gsum 17381 df-mre 17523 df-mrc 17524 df-acs 17526 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-mhm 18686 df-submnd 18687 df-efmnd 18772 df-grp 18844 df-minusg 18845 df-sbg 18846 df-subg 19031 df-ghm 19121 df-gim 19167 df-oppg 19254 df-symg 19276 df-pmtr 19348 df-psgn 19397 df-evpm 19398 df-cmn 19688 df-abl 19689 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-dvr 20286 df-drng 20616 df-cnfld 21241 df-tocyc 33037

This theorem is referenced by: (None)

W3C validator