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 30950

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 488	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝐴)
2		simpr 488	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → 𝑝 = 𝑔)
3	2	oveq1d 7165	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇))
4	3, 2	oveq12d 7168	. . . . 5 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) − 𝑝) = ((𝑔 + 𝑇) − 𝑔))
5	4	eqeq2d 2769	. . . 4 ⊢ (((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) − 𝑔)))
6		simplr 768	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
7	1, 5, 6	rspcedvd 3544	. . 3 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
8		cyc3conja.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ Fin)
9	8	ad5antr 733	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝐷 ∈ Fin)
10	9	ad3antrrr 729	. . . . . . 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 3869	. . . . . . 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 3870	. . . . . . . . . . 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 3870	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ 𝐷)
18	15, 17	prssd 4712	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ 𝐷)
19		simpr 488	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
20		pr2nelem 9464	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
21	14, 16, 19, 20	syl3anc 1368	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2_o)
22		eqid 2758	. . . . . . . . . . 11 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
23		eqid 2758	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
24	22, 23	pmtrrn 18652	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2_o) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
25	10, 18, 21, 24	syl3anc 1368	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷))
26		cyc3conja.s	. . . . . . . . . 10 ⊢ 𝑆 = (SymGrp‘𝐷)
27		eqid 2758	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
28	26, 27, 23	pmtrodpm 20362	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
29	10, 25, 28	syl2anc 587	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷)))
30		cyc3conja.a	. . . . . . . . 9 ⊢ 𝐴 = (pmEven‘𝐷)
31	30	difeq2i 4025	. . . . . . . 8 ⊢ ((Base‘𝑆) ∖ 𝐴) = ((Base‘𝑆) ∖ (pmEven‘𝐷))
32	29, 31	eleqtrrdi 2863	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴))
33	26, 27, 30	odpmco 30881	. . . . . . 7 ⊢ ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
34	10, 13, 32, 33	syl3anc 1368	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴)
35		simpr 488	. . . . . . . . 9 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
36	35	oveq1d 7165	. . . . . . . 8 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇))
37	36, 35	oveq12d 7168	. . . . . . 7 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) − 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
38	37	eqeq2d 2769	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))))
39	29	eldifad 3870	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆))
40		0zd 12032	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℤ)
41		cyc3conja.n	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = (♯‘𝐷)
42		hashcl 13767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ₀)
43	8, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐷) ∈ ℕ₀)
44	41, 43	eqeltrid 2856	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
45	44	nn0zd 12124	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℤ)
46		3z 12054	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℤ
47	46	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ∈ ℤ)
48		0red 10682	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
49	47	zred 12126	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ∈ ℝ)
50		3pos 11779	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 3
51	50	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 3)
52	48, 49, 51	ltled 10826	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ 3)
53		5re 11761	. . . . . . . . . . . . . . . . . 18 ⊢ 5 ∈ ℝ
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℝ)
55	44	nn0red 11995	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ)
56		3lt5 11852	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 5
57	56	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 3 < 5)
58	49, 54, 57	ltled 10826	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ≤ 5)
59		cyc3conja.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ≤ 𝑁)
60	49, 54, 55, 58, 59	letrd 10835	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ≤ 𝑁)
61		elfz4 12949	. . . . . . . . . . . . . . . 16 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (0 ≤ 3 ∧ 3 ≤ 𝑁)) → 3 ∈ (0...𝑁))
62	40, 45, 47, 52, 60, 61	syl32anc 1375	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 3 ∈ (0...𝑁))
63		cyc3conja.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝑀 “ (^◡♯ “ {3}))
64		cyc3conja.m	. . . . . . . . . . . . . . . 16 ⊢ 𝑀 = (toCyc‘𝐷)
65	63, 26, 41, 64, 27	cycpmgcl 30946	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 3 ∈ (0...𝑁)) → 𝐶 ⊆ (Base‘𝑆))
66	8, 62, 65	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ⊆ (Base‘𝑆))
67		cyc3conja.t	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ 𝐶)
68	66, 67	sseldd 3893	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ (Base‘𝑆))
69	68	ad8antr 739	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑇 ∈ (Base‘𝑆))
70	64, 10, 15, 17, 19, 22	cycpm2tr 30912	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘⟨“𝑥𝑦”⟩) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))
71	70	reseq1d 5822	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢))
72	15, 17	s2cld 14280	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩ ∈ Word 𝐷)
73	15, 17, 19	s2f1 30743	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ⟨“𝑥𝑦”⟩:dom ⟨“𝑥𝑦”⟩–1-1→𝐷)
74	64, 10, 72, 73	tocycfvres2 30904	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) = ( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)))
75	74	reseq1d 5822	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢))
76		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3})))
77	76	elin1d 4103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
78		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
79		dmeq 5743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
80		eqidd 2759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
81	78, 79, 80	f1eq123d 6594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷))
82	81	elrab 3602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
83	77, 82	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷))
84	83	simprd 499	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢:dom 𝑢–1-1→𝐷)
85		f1f 6560	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢⟶𝐷)
86		frn 6504	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢:dom 𝑢⟶𝐷 → ran 𝑢 ⊆ 𝐷)
87	84, 85, 86	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ran 𝑢 ⊆ 𝐷)
88	87	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ 𝐷)
89	14, 16	prssd 4712	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢))
90		ssconb 4043	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})))
91	90	biimpa 480	. . . . . . . . . . . . . . . . 17 ⊢ ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
92	18, 88, 89, 91	syl21anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))
93	14, 16	s2rn 30742	. . . . . . . . . . . . . . . . 17 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran ⟨“𝑥𝑦”⟩ = {𝑥, 𝑦})
94	93	difeq2d 4028	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝐷 ∖ ran ⟨“𝑥𝑦”⟩) = (𝐷 ∖ {𝑥, 𝑦}))
95	92, 94	sseqtrrd 3933	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩))
96	95	resabs1d 5854	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘⟨“𝑥𝑦”⟩) ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢))
97	95	resabs1d 5854	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (( I ↾ (𝐷 ∖ ran ⟨“𝑥𝑦”⟩)) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
98	75, 96, 97	3eqtr3d 2801	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘⟨“𝑥𝑦”⟩) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
99	71, 98	eqtr3d 2795	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢))
100		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘𝑢) = 𝑇)
101	100	reseq1d 5822	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑇 ↾ (𝐷 ∖ ran 𝑢)))
102	83	simpld 498	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ Word 𝐷)
103	102	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢 ∈ Word 𝐷)
104	84	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢:dom 𝑢–1-1→𝐷)
105	64, 10, 103, 104	tocycfvres2 30904	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
106	101, 105	eqtr3d 2795	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢)))
107		disjdif 4368	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅
108	107	a1i 11	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅)
109		undif 4378	. . . . . . . . . . . . 13 ⊢ (ran 𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
110	88, 109	sylib 221	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷)
111	26, 27, 39, 69, 99, 106, 108, 110	symgcom 30878	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
112	111	coeq2d 5702	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
113		cyc3conja.p	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑆)
114	26, 27, 113	symgov 18579	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
115	11, 39, 114	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
116	26, 27, 113	symgcl 18580	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
117	11, 39, 116	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
118	115, 117	eqeltrrd 2853	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆))
119	26, 27, 113	symgov 18579	. . . . . . . . . . . 12 ⊢ (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
120	118, 69, 119	syl2anc 587	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇))
121		coass 6095	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))
122	120, 121	eqtrdi 2809	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)))
123		coass 6095	. . . . . . . . . . 11 ⊢ ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
124	123	a1i 11	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
125	112, 122, 124	3eqtr4d 2803	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
126		cnvco 5725	. . . . . . . . . 10 ⊢ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)
127	126	a1i 11	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
128	125, 127	coeq12d 5704	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)))
129		coass 6095	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔))
130		coass 6095	. . . . . . . . . . 11 ⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})))
131	130	coeq1i 5699	. . . . . . . . . 10 ⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ^◡𝑔) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔)
132	129, 131	eqtr3i 2783	. . . . . . . . 9 ⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔)
133	132	a1i 11	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡𝑔)) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔))
134	26, 27, 113	symgov 18579	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
135	11, 69, 134	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇))
136	26, 27, 113	symgcl 18580	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
137	11, 69, 136	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆))
138	135, 137	eqeltrrd 2853	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ 𝑇) ∈ (Base‘𝑆))
139	26, 27	symgbasf 18571	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇) ∈ (Base‘𝑆) → (𝑔 ∘ 𝑇):𝐷⟶𝐷)
140		fcoi1 6537	. . . . . . . . . . . 12 ⊢ ((𝑔 ∘ 𝑇):𝐷⟶𝐷 → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
141	138, 139, 140	3syl 18	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇))
142	26, 27	elsymgbas 18569	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ Fin → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆) ↔ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷))
143	142	biimpa 480	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷)
144	10, 39, 143	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷)
145		f1ococnv2 6628	. . . . . . . . . . . . 13 ⊢ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷 → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
146	144, 145	syl 17	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷))
147	146	coeq2d 5702	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)))
148	141, 147, 135	3eqtr4d 2803	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇))
149	148	coeq1d 5701	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
150		cyc3conja.l	. . . . . . . . . . 11 ⊢ − = (-_g‘𝑆)
151	26, 27, 150	symgsubg 30882	. . . . . . . . . 10 ⊢ (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
152	137, 11, 151	syl2anc 587	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ^◡𝑔))
153	149, 152	eqtr4d 2796	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ^◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ^◡𝑔) = ((𝑔 + 𝑇) − 𝑔))
154	128, 133, 153	3eqtrd 2797	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) − 𝑔))
155	26	symggrp 18595	. . . . . . . . . . 11 ⊢ (𝐷 ∈ Fin → 𝑆 ∈ Grp)
156	8, 155	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Grp)
157	156	ad8antr 739	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑆 ∈ Grp)
158	27, 113	grpcl 18177	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
159	157, 118, 69, 158	syl3anc 1368	. . . . . . . 8 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆))
160	26, 27, 150	symgsubg 30882	. . . . . . . 8 ⊢ ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
161	159, 118, 160	syl2anc 587	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ^◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
162		simp-7r 789	. . . . . . 7 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = ((𝑔 + 𝑇) − 𝑔))
163	154, 161, 162	3eqtr4rd 2804	. . . . . 6 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))
164	34, 38, 163	rspcedvd 3544	. . . . 5 ⊢ (((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
165		difexg 5197	. . . . . . . 8 ⊢ (𝐷 ∈ Fin → (𝐷 ∖ ran 𝑢) ∈ V)
166	8, 165	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V)
167	166	ad5antr 733	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V)
168		3p2e5 11825	. . . . . . . . . . 11 ⊢ (3 + 2) = 5
169	168, 59	eqbrtrid 5067	. . . . . . . . . 10 ⊢ (𝜑 → (3 + 2) ≤ 𝑁)
170		2re 11748	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
171	170	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
172	49, 171, 55	leaddsub2d 11280	. . . . . . . . . 10 ⊢ (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3)))
173	169, 172	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → 2 ≤ (𝑁 − 3))
174	173	ad5antr 733	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (𝑁 − 3))
175	41	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑁 = (♯‘𝐷))
176	76	elin2d 4104	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ (^◡♯ “ {3}))
177		hashf 13748	. . . . . . . . . . . . 13 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
178		ffn 6498	. . . . . . . . . . . . 13 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
179		fniniseg 6821	. . . . . . . . . . . . 13 ⊢ (♯ Fn V → (𝑢 ∈ (^◡♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3)))
180	177, 178, 179	mp2b 10	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (^◡♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) = 3))
181	180	simprbi 500	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (^◡♯ “ {3}) → (♯‘𝑢) = 3)
182	176, 181	syl 17	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = 3)
183		vex 3413	. . . . . . . . . . . 12 ⊢ 𝑢 ∈ V
184	183	dmex 7621	. . . . . . . . . . 11 ⊢ dom 𝑢 ∈ V
185		hashf1rn 13763	. . . . . . . . . . 11 ⊢ ((dom 𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢))
186	184, 84, 185	sylancr 590	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢))
187	182, 186	eqtr3d 2795	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 3 = (♯‘ran 𝑢))
188	175, 187	oveq12d 7168	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran 𝑢)))
189	174, 188	breqtrd 5058	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran 𝑢)))
190		hashssdif 13823	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
191	9, 87, 190	syl2anc 587	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢)))
192	189, 191	breqtrrd 5060	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢)))
193		hashge2el2dif 13890	. . . . . 6 ⊢ (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦)
194	167, 192, 193	syl2anc 587	. . . . 5 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦)
195	164, 194	r19.29vva 3257	. . . 4 ⊢ ((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
196		nfcv 2919	. . . . . 6 ⊢ Ⅎ𝑢𝑀
197	64, 26, 27	tocycf 30910	. . . . . . 7 ⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆))
198		ffn 6498	. . . . . . 7 ⊢ (𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆) → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
199	8, 197, 198	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷})
200	67, 63	eleqtrdi 2862	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ (𝑀 “ (^◡♯ “ {3})))
201	196, 199, 200	fvelimad 6720	. . . . 5 ⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
202	201	ad3antrrr 729	. . . 4 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (^◡♯ “ {3}))(𝑀‘𝑢) = 𝑇)
203	195, 202	r19.29a 3213	. . 3 ⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
204	7, 203	pm2.61dan 812	. 2 ⊢ (((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
205		cyc3conja.q	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝐶)
206	63, 26, 41, 64, 27, 113, 150, 62, 8, 205, 67	cycpmconjs 30949	. 2 ⊢ (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) − 𝑔))
207	204, 206	r19.29a 3213	1 ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ∃wrex 3071 {crab 3074 Vcvv 3409 ∖ cdif 3855 ∪ cun 3856 ∩ cin 3857 ⊆ wss 3858 ∅c0 4225 {csn 4522 {cpr 4524 class class class wbr 5032 I cid 5429 ^◡ccnv 5523 dom cdm 5524 ran crn 5525 ↾ cres 5526 “ cima 5527 ∘ ccom 5528 Fn wfn 6330 ⟶wf 6331 –1-1→wf1 6332 –1-1-onto→wf1o 6334 ‘cfv 6335 (class class class)co 7150 2_oc2o 8106 ≈ cen 8524 Fincfn 8527 ℝcr 10574 0cc0 10575 + caddc 10578 +∞cpnf 10710 < clt 10713 ≤ cle 10714 − cmin 10908 2c2 11729 3c3 11730 5c5 11732 ℕ₀cn0 11934 ℤcz 12020 ...cfz 12939 ♯chash 13740 Word cword 13913 ⟨“cs2 14250 Basecbs 16541 +_gcplusg 16623 Grpcgrp 18169 -_gcsg 18171 SymGrpcsymg 18562 pmTrspcpmtr 18636 pmEvencevpm 18685 toCycctocyc 30899

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653 ax-addf 10654 ax-mulf 10655

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-xor 1503 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-ot 4531 df-uni 4799 df-int 4839 df-iun 4885 df-iin 4886 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-se 5484 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-isom 6344 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-1st 7693 df-2nd 7694 df-tpos 7902 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-2o 8113 df-oadd 8116 df-er 8299 df-map 8418 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-sup 8939 df-inf 8940 df-dju 9363 df-card 9401 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-div 11336 df-nn 11675 df-2 11737 df-3 11738 df-4 11739 df-5 11740 df-6 11741 df-7 11742 df-8 11743 df-9 11744 df-n0 11935 df-xnn0 12007 df-z 12021 df-dec 12138 df-uz 12283 df-rp 12431 df-fz 12940 df-fzo 13083 df-fl 13211 df-mod 13287 df-seq 13419 df-exp 13480 df-hash 13741 df-word 13914 df-lsw 13962 df-concat 13970 df-s1 13997 df-substr 14050 df-pfx 14080 df-splice 14159 df-reverse 14168 df-csh 14198 df-s2 14257 df-struct 16543 df-ndx 16544 df-slot 16545 df-base 16547 df-sets 16548 df-ress 16549 df-plusg 16636 df-mulr 16637 df-starv 16638 df-tset 16642 df-ple 16643 df-ds 16645 df-unif 16646 df-0g 16773 df-gsum 16774 df-mre 16915 df-mrc 16916 df-acs 16918 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-mhm 18022 df-submnd 18023 df-efmnd 18100 df-grp 18172 df-minusg 18173 df-sbg 18174 df-subg 18343 df-ghm 18423 df-gim 18466 df-oppg 18541 df-symg 18563 df-pmtr 18637 df-psgn 18686 df-evpm 18687 df-cmn 18975 df-abl 18976 df-mgp 19308 df-ur 19320 df-ring 19367 df-cring 19368 df-oppr 19444 df-dvdsr 19462 df-unit 19463 df-invr 19493 df-dvr 19504 df-drng 19572 df-cnfld 20167 df-tocyc 30900

This theorem is referenced by: (None)

W3C validator