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		enpr2	$⊢ (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	48 52 54 59 66	elfzd	$⊢ φ \to 3 \in (0 \dots N)$
68	1 3 4 5 36	cycpmgcl	$⊢ (D \in Fin \land 3 \in (0 \dots N)) \to C \subseteq {Base}_{S}$
69	9 67 68	syl2anc	$⊢ φ \to C \subseteq {Base}_{S}$
70	69 11	sseldd	$⊢ φ \to T \in {Base}_{S}$
71	70	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}$
72	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\})$
73	72	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}$
74	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$
75	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$
76	5 20 74 75	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 ”⟩)}$
77	76	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}$
78		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\}])$
79	78	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\}$
80		id	$⊢ w = u \to w = u$
81		dmeq	$⊢ w = u \to dom w = dom u$
82		eqidd	$⊢ w = u \to D = D$
83	80 81 82	f1eq123d	$⊢ w = u \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow u : dom u \underset{1-1}{⟶} D)$
84	83	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)$
85	79 84	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)$
86	85	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$
87		f1f	$⊢ u : dom u \underset{1-1}{⟶} D \to u : dom u ⟶ D$
88		frn	$⊢ u : dom u ⟶ D \to ran u \subseteq D$
89	86 87 88	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$
90	89	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$
91	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$
92		ssconb	$⊢ (\{x, y\} \subseteq D \land ran u \subseteq D) \to (\{x, y\} \subseteq D ∖ ran u \leftrightarrow ran u \subseteq D ∖ \{x, y\})$
93	92	biimpa	$⊢ ((\{x, y\} \subseteq D \land ran u \subseteq D) \land \{x, y\} \subseteq D ∖ ran u) \to ran u \subseteq D ∖ \{x, y\}$
94	28 90 91 93	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\}$
95	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\}$
96	95	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\}$
97	94 96	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 ”⟩$
98	97	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}$
99	97	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}$
100	77 98 99	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}$
101	73 100	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}$
102		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$
103	102	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)}$
104	85	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$
105	104	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$
106	86	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$
107	5 20 105 106	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)}$
108	103 107	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)}$
109		disjdif	$⊢ ran u \cap (D ∖ ran u) = \emptyset$
110	109	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$
111		undif	$⊢ ran u \subseteq D \leftrightarrow ran u \cup (D ∖ ran u) = D$
112	90 111	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$
113	3 36 47 71 101 108 110 112	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\})$
114	113	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\}))$
115	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\})$
116	21 47 115	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\})$
117	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}$
118	21 47 117	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}$
119	116 118	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}$
120	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$
121	119 71 120	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$
122		coass	$⊢ (g \circ pmTrsp (D) (\{x, y\})) \circ T = g \circ (pmTrsp (D) (\{x, y\}) \circ T)$
123	121 122	eqtrdi	$⊢ ((((((((φ \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)$
124		coass	$⊢ (g \circ T) \circ pmTrsp (D) (\{x, y\}) = g \circ (T \circ pmTrsp (D) (\{x, y\}))$
125	124	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\}))$
126	114 123 125	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\})$
127		cnvco	$⊢ {(g \circ pmTrsp (D) (\{x, y\}))}^{-1} = {pmTrsp (D) (\{x, y\})}^{-1} \circ g^{-1}$
128	127	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}$
129	126 128	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})$
130		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})$
131		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})$
132	131	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}$
133	130 132	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}$
134	133	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}$
135	3 36 6	symgov	$⊢ (g \in {Base}_{S} \land T \in {Base}_{S}) \to g \underset{˙}{+} T = g \circ T$
136	21 71 135	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$
137	3 36 6	symgcl	$⊢ (g \in {Base}_{S} \land T \in {Base}_{S}) \to g \underset{˙}{+} T \in {Base}_{S}$
138	21 71 137	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}$
139	136 138	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}$
140	3 36	symgbasf	$⊢ g \circ T \in {Base}_{S} \to (g \circ T) : D ⟶ D$
141		fcoi1	$⊢ (g \circ T) : D ⟶ D \to (g \circ T) \circ ({I ↾}_{D}) = g \circ T$
142	139 140 141	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$
143	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)$
144	143	biimpa	$⊢ (D \in Fin \land pmTrsp (D) (\{x, y\}) \in {Base}_{S}) \to pmTrsp (D) (\{x, y\}) : D \underset{1-1 onto}{⟶} D$
145	20 47 144	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$
146		f1ococnv2	$⊢ pmTrsp (D) (\{x, y\}) : D \underset{1-1 onto}{⟶} D \to pmTrsp (D) (\{x, y\}) \circ {pmTrsp (D) (\{x, y\})}^{-1} = {I ↾}_{D}$
147	145 146	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}$
148	147	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})$
149	142 148 136	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$
150	149	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}$
151	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}$
152	138 21 151	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}$
153	150 152	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$
154	129 134 153	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$
155	3	symggrp	$⊢ D \in Fin \to S \in Grp$
156	9 155	syl	$⊢ φ \to S \in Grp$
157	156	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$
158	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}$
159	157 119 71 158	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}$
160	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}$
161	159 119 160	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}$
162		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$
163	154 161 162	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\}))$
164	42 46 163	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$
165	9	difexd	$⊢ φ \to D ∖ ran u \in V$
166	165	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$
167		3p2e5	$⊢ 3 + 2 = 5$
168	167 8	eqbrtrid	$⊢ φ \to 3 + 2 \leq N$
169		2re	$⊢ 2 \in ℝ$
170	169	a1i	$⊢ φ \to 2 \in ℝ$
171	56 170 62	leaddsub2d	$⊢ φ \to (3 + 2 \leq N \leftrightarrow 2 \leq N - 3)$
172	168 171	mpbid	$⊢ φ \to 2 \leq N - 3$
173	172	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$
174	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\|$
175	78	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\}]$
176		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
177		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
178		fniniseg	$⊢ \|.\| Fn V \to (u \in {\|.\|}^{-1} [\{3\}] \leftrightarrow (u \in V \land \|u\| = 3))$
179	176 177 178	mp2b	$⊢ u \in {\|.\|}^{-1} [\{3\}] \leftrightarrow (u \in V \land \|u\| = 3)$
180	179	simprbi	$⊢ u \in {\|.\|}^{-1} [\{3\}] \to \|u\| = 3$
181	175 180	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$
182		vex	$⊢ u \in V$
183	182	dmex	$⊢ dom u \in V$
184		hashf1rn	$⊢ (dom u \in V \land u : dom u \underset{1-1}{⟶} D) \to \|u\| = \|ran u\|$
185	183 86 184	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\|$
186	181 185	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\|$
187	174 186	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\|$
188	173 187	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\|$
189		hashssdif	$⊢ (D \in Fin \land ran u \subseteq D) \to \|D ∖ ran u\| = \|D\| - \|ran u\|$
190	19 89 189	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\|$
191	188 190	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\|$
192		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$
193	166 191 192	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$
194	164 193	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$
195		nfcv	$⊢ \underline{Ⅎ} u M$
196	5 3 36	tocycf	$⊢ D \in Fin \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
197		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\}$
198	9 196 197	3syl	$⊢ φ \to M Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
199	11 1	eleqtrdi	$⊢ φ \to T \in M [{\|.\|}^{-1} [\{3\}]]$
200	195 198 199	fvelimad	$⊢ φ \to \exists u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}]) M (u) = T$
201	200	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$
202	194 201	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$
203	18 202	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$
204	1 3 4 5 36 6 7 67 9 10 11	cycpmconjs	$⊢ φ \to \exists g \in {Base}_{S} Q = (g \underset{˙}{+} T) \underset{˙}{-} g$
205	203 204	r19.29a	$⊢ φ \to \exists p \in A Q = (p \underset{˙}{+} T) \underset{˙}{-} p$

Metamath Proof Explorer

Theorem cyc3conja

Proof