cyc3conja

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)

	Ref	Expression
Hypotheses	cyc3conja.c	$⊢ C = M [{\|.\|}^{-1} [\{3\}]]$
	cyc3conja.a	$⊢ A = pmEven (D)$
	cyc3conja.s	$⊢ S = SymGrp (D)$
	cyc3conja.n	$⊢ N = \|D\|$
	cyc3conja.m	$⊢ M = toCyc (D)$
	cyc3conja.p	$⊢ \underset{˙}{+} = +_{S}$
	cyc3conja.l	$⊢ \underset{˙}{-} = -_{S}$
	cyc3conja.1	$⊢ φ \to 5 \leq N$
	cyc3conja.d	$⊢ φ \to D \in Fin$
	cyc3conja.q	$⊢ φ \to Q \in C$
	cyc3conja.t	$⊢ φ \to T \in C$
Assertion	cyc3conja	$⊢ φ \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$

Proof

Step	Hyp	Ref	Expression
1		cyc3conja.c	$⊢ C = M [{\|.\|}^{-1} [\{3\}]]$
2		cyc3conja.a	$⊢ A = pmEven (D)$
3		cyc3conja.s	$⊢ S = SymGrp (D)$
4		cyc3conja.n	$⊢ N = \|D\|$
5		cyc3conja.m	$⊢ M = toCyc (D)$
6		cyc3conja.p	$⊢ \underset{˙}{+} = +_{S}$
7		cyc3conja.l	$⊢ \underset{˙}{-} = -_{S}$
8		cyc3conja.1	$⊢ φ \to 5 \leq N$
9		cyc3conja.d	$⊢ φ \to D \in Fin$
10		cyc3conja.q	$⊢ φ \to Q \in C$
11		cyc3conja.t	$⊢ φ \to T \in C$
12		simpr	$⊢ (((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \to g \in A$
13		simpr	$⊢ ((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \land p = g) \to p = g$
14	13	oveq1d	$⊢ ((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \land p = g) \to p \underset{˙}{+} T = g \underset{˙}{+} T$
15	14 13	oveq12d	$⊢ ((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \land p = g) \to (p \underset{˙}{+} T) \underset{˙}{-} p = (g \underset{˙}{+} T) \underset{˙}{-} g$
16	15	eqeq2d	$⊢ ((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \land p = g) \to (Q = (p \underset{˙}{+} T) \underset{˙}{-} p \leftrightarrow Q = (g \underset{˙}{+} T) \underset{˙}{-} g)$
17		simplr	$⊢ (((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \to Q = (g \underset{˙}{+} T) \underset{˙}{-} g$
18	12 16 17	rspcedvd	$⊢ (((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land g \in A) \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
19	9	ad5antr	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to D \in Fin$
20	19	ad3antrrr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to D \in Fin$
21		simp-8r	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \in {Base}_{S}$
22		simp-6r	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to \neg g \in A$
23	21 22	eldifd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \in ({Base}_{S} ∖ A)$
24		simpllr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to x \in (D ∖ ran u)$
25	24	eldifad	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to x \in D$
26		simplr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to y \in (D ∖ ran u)$
27	26	eldifad	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to y \in D$
28	25 27	prssd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to \{x, y\} \subseteq D$
29		simpr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to x \neq y$
30		pr2nelem	$⊢ (x \in (D ∖ ran u) \land y \in (D ∖ ran u) \land x \neq y) \to \{x, y\} \approx 2_{𝑜}$
31	24 26 29 30	syl3anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to \{x, y\} \approx 2_{𝑜}$
32		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
33		eqid	$⊢ ran pmTrsp (D) = ran pmTrsp (D)$
34	32 33	pmtrrn	$⊢ (D \in Fin \land \{x, y\} \subseteq D \land \{x, y\} \approx 2_{𝑜}) \to pmTrsp (D) (\{x, y\}) \in ran pmTrsp (D)$
35	20 28 31 34	syl3anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) \in ran pmTrsp (D)$
36		eqid	$⊢ {Base}_{S} = {Base}_{S}$
37	3 36 33	pmtrodpm	$⊢ (D \in Fin \land pmTrsp (D) (\{x, y\}) \in ran pmTrsp (D)) \to pmTrsp (D) (\{x, y\}) \in ({Base}_{S} ∖ pmEven (D))$
38	20 35 37	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) \in ({Base}_{S} ∖ pmEven (D))$
39	2	difeq2i	$⊢ {Base}_{S} ∖ A = {Base}_{S} ∖ pmEven (D)$
40	38 39	eleqtrrdi	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) \in ({Base}_{S} ∖ A)$
41	3 36 2	odpmco	$⊢ (D \in Fin \land g \in ({Base}_{S} ∖ A) \land pmTrsp (D) (\{x, y\}) \in ({Base}_{S} ∖ A)) \to g \circ pmTrsp (D) (\{x, y\}) \in A$
42	20 23 40 41	syl3anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \circ pmTrsp (D) (\{x, y\}) \in A$
43		simpr	$⊢ (((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \land p = g \circ pmTrsp (D) (\{x, y\})) \to p = g \circ pmTrsp (D) (\{x, y\})$
44	43	oveq1d	$⊢ (((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \land p = g \circ pmTrsp (D) (\{x, y\})) \to p \underset{˙}{+} T = (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T$
45	44 43	oveq12d	$⊢ (((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \land p = g \circ pmTrsp (D) (\{x, y\})) \to (p \underset{˙}{+} T) \underset{˙}{-} p = ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \underset{˙}{-} (g \circ pmTrsp (D) (\{x, y\}))$
46	45	eqeq2d	$⊢ (((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \land p = g \circ pmTrsp (D) (\{x, y\})) \to (Q = (p \underset{˙}{+} T) \underset{˙}{-} p \leftrightarrow Q = ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \underset{˙}{-} (g \circ pmTrsp (D) (\{x, y\})))$
47	38	eldifad	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) \in {Base}_{S}$
48		0zd	$⊢ φ \to 0 \in ℤ$
49		hashcl	$⊢ D \in Fin \to \|D\| \in ℕ_{0}$
50	9 49	syl	$⊢ φ \to \|D\| \in ℕ_{0}$
51	4 50	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
52	51	nn0zd	$⊢ φ \to N \in ℤ$
53		3z	$⊢ 3 \in ℤ$
54	53	a1i	$⊢ φ \to 3 \in ℤ$
55		0red	$⊢ φ \to 0 \in ℝ$
56	54	zred	$⊢ φ \to 3 \in ℝ$
57		3pos	$⊢ 0 < 3$
58	57	a1i	$⊢ φ \to 0 < 3$
59	55 56 58	ltled	$⊢ φ \to 0 \leq 3$
60		5re	$⊢ 5 \in ℝ$
61	60	a1i	$⊢ φ \to 5 \in ℝ$
62	51	nn0red	$⊢ φ \to N \in ℝ$
63		3lt5	$⊢ 3 < 5$
64	63	a1i	$⊢ φ \to 3 < 5$
65	56 61 64	ltled	$⊢ φ \to 3 \leq 5$
66	56 61 62 65 8	letrd	$⊢ φ \to 3 \leq N$
67		elfz4	$⊢ ((0 \in ℤ \land N \in ℤ \land 3 \in ℤ) \land (0 \leq 3 \land 3 \leq N)) \to 3 \in (0 \dots N)$
68	48 52 54 59 66 67	syl32anc	$⊢ φ \to 3 \in (0 \dots N)$
69	1 3 4 5 36	cycpmgcl	$⊢ (D \in Fin \land 3 \in (0 \dots N)) \to C \subseteq {Base}_{S}$
70	9 68 69	syl2anc	$⊢ φ \to C \subseteq {Base}_{S}$
71	70 11	sseldd	$⊢ φ \to T \in {Base}_{S}$
72	71	ad8antr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to T \in {Base}_{S}$
73	5 20 25 27 29 32	cycpm2tr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to M (⟨“ x y ”⟩) = pmTrsp (D) (\{x, y\})$
74	73	reseq1d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {M (⟨“ x y ”⟩) ↾}_{ran u} = {pmTrsp (D) (\{x, y\}) ↾}_{ran u}$
75	25 27	s2cld	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ⟨“ x y ”⟩ \in Word D$
76	25 27 29	s2f1	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ⟨“ x y ”⟩ : dom ⟨“ x y ”⟩ \underset{1-1}{⟶} D$
77	5 20 75 76	tocycfvres2	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {M (⟨“ x y ”⟩) ↾}_{(D ∖ ran ⟨“ x y ”⟩)} = {I ↾}_{(D ∖ ran ⟨“ x y ”⟩)}$
78	77	reseq1d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {({M (⟨“ x y ”⟩) ↾}_{(D ∖ ran ⟨“ x y ”⟩)}) ↾}_{ran u} = {({I ↾}_{(D ∖ ran ⟨“ x y ”⟩)}) ↾}_{ran u}$
79		simplr	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])$
80	79	elin1d	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
81		id	$⊢ w = u \to w = u$
82		dmeq	$⊢ w = u \to dom w = dom u$
83		eqidd	$⊢ w = u \to D = D$
84	81 82 83	f1eq123d	$⊢ w = u \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow u : dom u \underset{1-1}{⟶} D)$
85	84	elrab	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow (u \in Word D \land u : dom u \underset{1-1}{⟶} D)$
86	80 85	sylib	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to (u \in Word D \land u : dom u \underset{1-1}{⟶} D)$
87	86	simprd	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to u : dom u \underset{1-1}{⟶} D$
88		f1f	$⊢ u : dom u \underset{1-1}{⟶} D \to u : dom u ⟶ D$
89		frn	$⊢ u : dom u ⟶ D \to ran u \subseteq D$
90	87 88 89	3syl	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to ran u \subseteq D$
91	90	ad3antrrr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ran u \subseteq D$
92	24 26	prssd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to \{x, y\} \subseteq D ∖ ran u$
93		ssconb	$⊢ (\{x, y\} \subseteq D \land ran u \subseteq D) \to (\{x, y\} \subseteq D ∖ ran u \leftrightarrow ran u \subseteq D ∖ \{x, y\})$
94	93	biimpa	$⊢ ((\{x, y\} \subseteq D \land ran u \subseteq D) \land \{x, y\} \subseteq D ∖ ran u) \to ran u \subseteq D ∖ \{x, y\}$
95	28 91 92 94	syl21anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ran u \subseteq D ∖ \{x, y\}$
96	24 26	s2rn	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ran ⟨“ x y ”⟩ = \{x, y\}$
97	96	difeq2d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to D ∖ ran ⟨“ x y ”⟩ = D ∖ \{x, y\}$
98	95 97	sseqtrrd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ran u \subseteq D ∖ ran ⟨“ x y ”⟩$
99	98	resabs1d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {({M (⟨“ x y ”⟩) ↾}_{(D ∖ ran ⟨“ x y ”⟩)}) ↾}_{ran u} = {M (⟨“ x y ”⟩) ↾}_{ran u}$
100	98	resabs1d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {({I ↾}_{(D ∖ ran ⟨“ x y ”⟩)}) ↾}_{ran u} = {I ↾}_{ran u}$
101	78 99 100	3eqtr3d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {M (⟨“ x y ”⟩) ↾}_{ran u} = {I ↾}_{ran u}$
102	74 101	eqtr3d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {pmTrsp (D) (\{x, y\}) ↾}_{ran u} = {I ↾}_{ran u}$
103		simp-4r	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to M (u) = T$
104	103	reseq1d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {M (u) ↾}_{(D ∖ ran u)} = {T ↾}_{(D ∖ ran u)}$
105	86	simpld	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to u \in Word D$
106	105	ad3antrrr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to u \in Word D$
107	87	ad3antrrr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to u : dom u \underset{1-1}{⟶} D$
108	5 20 106 107	tocycfvres2	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {M (u) ↾}_{(D ∖ ran u)} = {I ↾}_{(D ∖ ran u)}$
109	104 108	eqtr3d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {T ↾}_{(D ∖ ran u)} = {I ↾}_{(D ∖ ran u)}$
110		disjdif	$⊢ ran u \cap (D ∖ ran u) = \emptyset$
111	110	a1i	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ran u \cap (D ∖ ran u) = \emptyset$
112		undif	$⊢ ran u \subseteq D \leftrightarrow ran u \cup (D ∖ ran u) = D$
113	91 112	sylib	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ran u \cup (D ∖ ran u) = D$
114	3 36 47 72 102 109 111 113	symgcom	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) \circ T = T \circ pmTrsp (D) (\{x, y\})$
115	114	coeq2d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \circ (pmTrsp (D) (\{x, y\}) \circ T) = g \circ (T \circ pmTrsp (D) (\{x, y\}))$
116	3 36 6	symgov	$⊢ (g \in {Base}_{S} \land pmTrsp (D) (\{x, y\}) \in {Base}_{S}) \to g \underset{˙}{+} pmTrsp (D) (\{x, y\}) = g \circ pmTrsp (D) (\{x, y\})$
117	21 47 116	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \underset{˙}{+} pmTrsp (D) (\{x, y\}) = g \circ pmTrsp (D) (\{x, y\})$
118	3 36 6	symgcl	$⊢ (g \in {Base}_{S} \land pmTrsp (D) (\{x, y\}) \in {Base}_{S}) \to g \underset{˙}{+} pmTrsp (D) (\{x, y\}) \in {Base}_{S}$
119	21 47 118	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \underset{˙}{+} pmTrsp (D) (\{x, y\}) \in {Base}_{S}$
120	117 119	eqeltrrd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \circ pmTrsp (D) (\{x, y\}) \in {Base}_{S}$
121	3 36 6	symgov	$⊢ (g \circ pmTrsp (D) (\{x, y\}) \in {Base}_{S} \land T \in {Base}_{S}) \to (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T = (g \circ pmTrsp (D) (\{x, y\})) \circ T$
122	120 72 121	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T = (g \circ pmTrsp (D) (\{x, y\})) \circ T$
123		coass	$⊢ (g \circ pmTrsp (D) (\{x, y\})) \circ T = g \circ (pmTrsp (D) (\{x, y\}) \circ T)$
124	122 123	syl6eq	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T = g \circ (pmTrsp (D) (\{x, y\}) \circ T)$
125		coass	$⊢ (g \circ T) \circ pmTrsp (D) (\{x, y\}) = g \circ (T \circ pmTrsp (D) (\{x, y\}))$
126	125	a1i	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ T) \circ pmTrsp (D) (\{x, y\}) = g \circ (T \circ pmTrsp (D) (\{x, y\}))$
127	115 124 126	3eqtr4d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T = (g \circ T) \circ pmTrsp (D) (\{x, y\})$
128		cnvco	$⊢ {(g \circ pmTrsp (D) (\{x, y\}))}^{-1} = {pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1}$
129	128	a1i	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to {(g \circ pmTrsp (D) (\{x, y\}))}^{-1} = {pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1}$
130	127 129	coeq12d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \circ {(g \circ pmTrsp (D) (\{x, y\}))}^{-1} = ((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ ({pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1})$
131		coass	$⊢ (((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ {pmTrsp (D) (\{x, y\})}^{-1}) \circ g^{-1} = ((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ ({pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1})$
132		coass	$⊢ ((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ {pmTrsp (D) (\{x, y\})}^{-1} = (g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1})$
133	132	coeq1i	$⊢ (((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ {pmTrsp (D) (\{x, y\})}^{-1}) \circ g^{-1} = ((g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1})) \circ g^{-1}$
134	131 133	eqtr3i	$⊢ ((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ ({pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1}) = ((g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1})) \circ g^{-1}$
135	134	a1i	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ((g \circ T) \circ pmTrsp (D) (\{x, y\})) \circ ({pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1}) = ((g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1})) \circ g^{-1}$
136	3 36 6	symgov	$⊢ (g \in {Base}_{S} \land T \in {Base}_{S}) \to g \underset{˙}{+} T = g \circ T$
137	21 72 136	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \underset{˙}{+} T = g \circ T$
138	3 36 6	symgcl	$⊢ (g \in {Base}_{S} \land T \in {Base}_{S}) \to g \underset{˙}{+} T \in {Base}_{S}$
139	21 72 138	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \underset{˙}{+} T \in {Base}_{S}$
140	137 139	eqeltrrd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to g \circ T \in {Base}_{S}$
141	3 36	symgbasf	$⊢ g \circ T \in {Base}_{S} \to (g \circ T) : D ⟶ D$
142		fcoi1	$⊢ (g \circ T) : D ⟶ D \to (g \circ T) \circ ({I ↾}_{D}) = g \circ T$
143	140 141 142	3syl	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ T) \circ ({I ↾}_{D}) = g \circ T$
144	3 36	elsymgbas	$⊢ D \in Fin \to (pmTrsp (D) (\{x, y\}) \in {Base}_{S} \leftrightarrow pmTrsp (D) (\{x, y\}) : D \underset{1-1 onto}{⟶} D)$
145	144	biimpa	$⊢ (D \in Fin \land pmTrsp (D) (\{x, y\}) \in {Base}_{S}) \to pmTrsp (D) (\{x, y\}) : D \underset{1-1 onto}{⟶} D$
146	20 47 145	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) : D \underset{1-1 onto}{⟶} D$
147		f1ococnv2	$⊢ pmTrsp (D) (\{x, y\}) : D \underset{1-1 onto}{⟶} D \to pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1} = {I ↾}_{D}$
148	146 147	syl	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1} = {I ↾}_{D}$
149	148	coeq2d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1}) = (g \circ T) \circ ({I ↾}_{D})$
150	143 149 137	3eqtr4d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1}) = g \underset{˙}{+} T$
151	150	coeq1d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ((g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1})) \circ g^{-1} = (g \underset{˙}{+} T) \circ g^{-1}$
152	3 36 7	symgsubg	$⊢ (g \underset{˙}{+} T \in {Base}_{S} \land g \in {Base}_{S}) \to (g \underset{˙}{+} T) \underset{˙}{-} g = (g \underset{˙}{+} T) \circ g^{-1}$
153	139 21 152	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \underset{˙}{+} T) \underset{˙}{-} g = (g \underset{˙}{+} T) \circ g^{-1}$
154	151 153	eqtr4d	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ((g \circ T) \circ (pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1})) \circ g^{-1} = (g \underset{˙}{+} T) \underset{˙}{-} g$
155	130 135 154	3eqtrd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \circ {(g \circ pmTrsp (D) (\{x, y\}))}^{-1} = (g \underset{˙}{+} T) \underset{˙}{-} g$
156	3	symggrp	$⊢ D \in Fin \to S \in Grp$
157	9 156	syl	$⊢ φ \to S \in Grp$
158	157	ad8antr	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to S \in Grp$
159	36 6	grpcl	$⊢ (S \in Grp \land g \circ pmTrsp (D) (\{x, y\}) \in {Base}_{S} \land T \in {Base}_{S}) \to (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T \in {Base}_{S}$
160	158 120 72 159	syl3anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to (g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T \in {Base}_{S}$
161	3 36 7	symgsubg	$⊢ ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T \in {Base}_{S} \land g \circ pmTrsp (D) (\{x, y\}) \in {Base}_{S}) \to ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \underset{˙}{-} (g \circ pmTrsp (D) (\{x, y\})) = ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \circ {(g \circ pmTrsp (D) (\{x, y\}))}^{-1}$
162	160 120 161	syl2anc	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \underset{˙}{-} (g \circ pmTrsp (D) (\{x, y\})) = ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \circ {(g \circ pmTrsp (D) (\{x, y\}))}^{-1}$
163		simp-7r	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to Q = (g \underset{˙}{+} T) \underset{˙}{-} g$
164	155 162 163	3eqtr4rd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to Q = ((g \circ pmTrsp (D) (\{x, y\})) \underset{˙}{+} T) \underset{˙}{-} (g \circ pmTrsp (D) (\{x, y\}))$
165	42 46 164	rspcedvd	$⊢ ((((((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \land x \in (D ∖ ran u)) \land y \in (D ∖ ran u)) \land x \neq y) \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
166		difexg	$⊢ D \in Fin \to D ∖ ran u \in V$
167	9 166	syl	$⊢ φ \to D ∖ ran u \in V$
168	167	ad5antr	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to D ∖ ran u \in V$
169		3p2e5	$⊢ 3 + 2 = 5$
170	169 8	eqbrtrid	$⊢ φ \to 3 + 2 \leq N$
171		2re	$⊢ 2 \in ℝ$
172	171	a1i	$⊢ φ \to 2 \in ℝ$
173	56 172 62	leaddsub2d	$⊢ φ \to (3 + 2 \leq N \leftrightarrow 2 \leq N - 3)$
174	170 173	mpbid	$⊢ φ \to 2 \leq N - 3$
175	174	ad5antr	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to 2 \leq N - 3$
176	4	a1i	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to N = \|D\|$
177	79	elin2d	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to u \in {\|.\|}^{-1} [\{3\}]$
178		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
179		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
180		fniniseg	$⊢ \|.\| Fn V \to (u \in {\|.\|}^{-1} [\{3\}] \leftrightarrow (u \in V \land \|u\| = 3))$
181	178 179 180	mp2b	$⊢ u \in {\|.\|}^{-1} [\{3\}] \leftrightarrow (u \in V \land \|u\| = 3)$
182	181	simprbi	$⊢ u \in {\|.\|}^{-1} [\{3\}] \to \|u\| = 3$
183	177 182	syl	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to \|u\| = 3$
184		vex	$⊢ u \in V$
185	184	dmex	$⊢ dom u \in V$
186		hashf1rn	$⊢ (dom u \in V \land u : dom u \underset{1-1}{⟶} D) \to \|u\| = \|ran u\|$
187	185 87 186	sylancr	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to \|u\| = \|ran u\|$
188	183 187	eqtr3d	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to 3 = \|ran u\|$
189	176 188	oveq12d	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to N - 3 = \|D\| - \|ran u\|$
190	175 189	breqtrd	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to 2 \leq \|D\| - \|ran u\|$
191		hashssdif	$⊢ (D \in Fin \land ran u \subseteq D) \to \|D ∖ ran u\| = \|D\| - \|ran u\|$
192	19 90 191	syl2anc	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to \|D ∖ ran u\| = \|D\| - \|ran u\|$
193	190 192	breqtrrd	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to 2 \leq \|D ∖ ran u\|$
194		hashge2el2dif	$⊢ (D ∖ ran u \in V \land 2 \leq \|D ∖ ran u\|) \to \exists x \in (D ∖ ran u) \exists y \in (D ∖ ran u) x \neq y$
195	168 193 194	syl2anc	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to \exists x \in (D ∖ ran u) \exists y \in (D ∖ ran u) x \neq y$
196	165 195	r19.29vva	$⊢ (((((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land M (u) = T) \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
197		nfcv	$⊢ \underline{Ⅎ} u M$
198	5 3 36	tocycf	$⊢ D \in Fin \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
199		ffn	$⊢ M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S} \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
200	9 198 199	3syl	$⊢ φ \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
201	11 1	eleqtrdi	$⊢ φ \to T \in M [{\|.\|}^{-1} [\{3\}]]$
202	197 200 201	fvelimad	$⊢ φ \to \exists u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}]) M (u) = T$
203	202	ad3antrrr	$⊢ (((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \to \exists u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}]) M (u) = T$
204	196 203	r19.29a	$⊢ (((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \land \neg g \in A) \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
205	18 204	pm2.61dan	$⊢ ((φ \land g \in {Base}_{S}) \land Q = (g \underset{˙}{+} T) \underset{˙}{-} g) \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$
206	1 3 4 5 36 6 7 68 9 10 11	cycpmconjs	$⊢ φ \to \exists g \in {Base}_{S} Q = (g \underset{˙}{+} T) \underset{˙}{-} g$
207	205 206	r19.29a	$⊢ φ \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$

Metamath Proof Explorer

Theorem cyc3conja

Proof