pmtrcnelor

Description: Composing a permutation F with a transposition which results in moving one or two less points. (Contributed by Thierry Arnoux, 16-Nov-2023)

	Ref	Expression
Hypotheses	pmtrcnel.s	$⊢ S = SymGrp (D)$
	pmtrcnel.t	$⊢ T = pmTrsp (D)$
	pmtrcnel.b	$⊢ B = {Base}_{S}$
	pmtrcnel.j	$⊢ J = F (I)$
	pmtrcnel.d	$⊢ φ \to D \in V$
	pmtrcnel.f	$⊢ φ \to F \in B$
	pmtrcnel.i	$⊢ φ \to I \in dom (F ∖ I)$
	pmtrcnel.e	$⊢ E = dom (F ∖ I)$
	pmtrcnel.a	$⊢ A = dom ((T (\{I, J\}) \circ F) ∖ I)$
Assertion	pmtrcnelor	$⊢ φ \to (A = E ∖ \{I, J\} \lor A = E ∖ \{I\})$

Proof

Step	Hyp	Ref	Expression
1		pmtrcnel.s	$⊢ S = SymGrp (D)$
2		pmtrcnel.t	$⊢ T = pmTrsp (D)$
3		pmtrcnel.b	$⊢ B = {Base}_{S}$
4		pmtrcnel.j	$⊢ J = F (I)$
5		pmtrcnel.d	$⊢ φ \to D \in V$
6		pmtrcnel.f	$⊢ φ \to F \in B$
7		pmtrcnel.i	$⊢ φ \to I \in dom (F ∖ I)$
8		pmtrcnel.e	$⊢ E = dom (F ∖ I)$
9		pmtrcnel.a	$⊢ A = dom ((T (\{I, J\}) \circ F) ∖ I)$
10	1 2 3 4 5 6 7	pmtrcnel	$⊢ φ \to dom ((T (\{I, J\}) \circ F) ∖ I) \subseteq dom (F ∖ I) ∖ \{I\}$
11	8	difeq1i	$⊢ E ∖ \{I\} = dom (F ∖ I) ∖ \{I\}$
12	10 9 11	3sstr4g	$⊢ φ \to A \subseteq E ∖ \{I\}$
13	12	ssdifd	$⊢ φ \to A ∖ (E ∖ \{I, J\}) \subseteq (E ∖ \{I\}) ∖ (E ∖ \{I, J\})$
14		difpr	$⊢ E ∖ \{I, J\} = (E ∖ \{I\}) ∖ \{J\}$
15	14	difeq2i	$⊢ (E ∖ \{I\}) ∖ (E ∖ \{I, J\}) = (E ∖ \{I\}) ∖ ((E ∖ \{I\}) ∖ \{J\})$
16	1 3	symgbasf1o	$⊢ F \in B \to F : D \underset{1-1 onto}{⟶} D$
17	6 16	syl	$⊢ φ \to F : D \underset{1-1 onto}{⟶} D$
18		f1omvdmvd	$⊢ (F : D \underset{1-1 onto}{⟶} D \land I \in dom (F ∖ I)) \to F (I) \in (dom (F ∖ I) ∖ \{I\})$
19	17 7 18	syl2anc	$⊢ φ \to F (I) \in (dom (F ∖ I) ∖ \{I\})$
20	4 19	eqeltrid	$⊢ φ \to J \in (dom (F ∖ I) ∖ \{I\})$
21	20	eldifad	$⊢ φ \to J \in dom (F ∖ I)$
22	21 8	eleqtrrdi	$⊢ φ \to J \in E$
23	4	a1i	$⊢ φ \to J = F (I)$
24		f1of	$⊢ F : D \underset{1-1 onto}{⟶} D \to F : D ⟶ D$
25	17 24	syl	$⊢ φ \to F : D ⟶ D$
26	25	ffnd	$⊢ φ \to F Fn D$
27		difss	$⊢ F ∖ I \subseteq F$
28		dmss	$⊢ F ∖ I \subseteq F \to dom (F ∖ I) \subseteq dom F$
29	27 28	ax-mp	$⊢ dom (F ∖ I) \subseteq dom F$
30	29 7	sselid	$⊢ φ \to I \in dom F$
31	25	fdmd	$⊢ φ \to dom F = D$
32	30 31	eleqtrd	$⊢ φ \to I \in D$
33		fnelnfp	$⊢ (F Fn D \land I \in D) \to (I \in dom (F ∖ I) \leftrightarrow F (I) \neq I)$
34	33	biimpa	$⊢ ((F Fn D \land I \in D) \land I \in dom (F ∖ I)) \to F (I) \neq I$
35	26 32 7 34	syl21anc	$⊢ φ \to F (I) \neq I$
36	23 35	eqnetrd	$⊢ φ \to J \neq I$
37		eldifsn	$⊢ J \in (E ∖ \{I\}) \leftrightarrow (J \in E \land J \neq I)$
38	22 36 37	sylanbrc	$⊢ φ \to J \in (E ∖ \{I\})$
39	38	snssd	$⊢ φ \to \{J\} \subseteq E ∖ \{I\}$
40		dfss4	$⊢ \{J\} \subseteq E ∖ \{I\} \leftrightarrow (E ∖ \{I\}) ∖ ((E ∖ \{I\}) ∖ \{J\}) = \{J\}$
41	39 40	sylib	$⊢ φ \to (E ∖ \{I\}) ∖ ((E ∖ \{I\}) ∖ \{J\}) = \{J\}$
42	15 41	eqtrid	$⊢ φ \to (E ∖ \{I\}) ∖ (E ∖ \{I, J\}) = \{J\}$
43	13 42	sseqtrd	$⊢ φ \to A ∖ (E ∖ \{I, J\}) \subseteq \{J\}$
44		sssn	$⊢ A ∖ (E ∖ \{I, J\}) \subseteq \{J\} \leftrightarrow (A ∖ (E ∖ \{I, J\}) = \emptyset \lor A ∖ (E ∖ \{I, J\}) = \{J\})$
45	43 44	sylib	$⊢ φ \to (A ∖ (E ∖ \{I, J\}) = \emptyset \lor A ∖ (E ∖ \{I, J\}) = \{J\})$
46		simpr	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \emptyset) \to A ∖ (E ∖ \{I, J\}) = \emptyset$
47	1 2 3 4 5 6 7	pmtrcnel2	$⊢ φ \to dom (F ∖ I) ∖ \{I, J\} \subseteq dom ((T (\{I, J\}) \circ F) ∖ I)$
48	8	difeq1i	$⊢ E ∖ \{I, J\} = dom (F ∖ I) ∖ \{I, J\}$
49	47 48 9	3sstr4g	$⊢ φ \to E ∖ \{I, J\} \subseteq A$
50		ssdif0	$⊢ E ∖ \{I, J\} \subseteq A \leftrightarrow (E ∖ \{I, J\}) ∖ A = \emptyset$
51	49 50	sylib	$⊢ φ \to (E ∖ \{I, J\}) ∖ A = \emptyset$
52	51	adantr	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \emptyset) \to (E ∖ \{I, J\}) ∖ A = \emptyset$
53		eqdif	$⊢ (A ∖ (E ∖ \{I, J\}) = \emptyset \land (E ∖ \{I, J\}) ∖ A = \emptyset) \to A = E ∖ \{I, J\}$
54	46 52 53	syl2anc	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \emptyset) \to A = E ∖ \{I, J\}$
55	54	ex	$⊢ φ \to (A ∖ (E ∖ \{I, J\}) = \emptyset \to A = E ∖ \{I, J\})$
56	12	adantr	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to A \subseteq E ∖ \{I\}$
57	14 49	eqsstrrid	$⊢ φ \to (E ∖ \{I\}) ∖ \{J\} \subseteq A$
58	57	adantr	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to (E ∖ \{I\}) ∖ \{J\} \subseteq A$
59		ssundif	$⊢ E ∖ \{I\} \subseteq \{J\} \cup A \leftrightarrow (E ∖ \{I\}) ∖ \{J\} \subseteq A$
60	58 59	sylibr	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to E ∖ \{I\} \subseteq \{J\} \cup A$
61		ssidd	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to \{J\} \subseteq \{J\}$
62		simpr	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to A ∖ (E ∖ \{I, J\}) = \{J\}$
63	61 62	sseqtrrd	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to \{J\} \subseteq A ∖ (E ∖ \{I, J\})$
64	63	difss2d	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to \{J\} \subseteq A$
65		ssequn1	$⊢ \{J\} \subseteq A \leftrightarrow \{J\} \cup A = A$
66	64 65	sylib	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to \{J\} \cup A = A$
67	60 66	sseqtrd	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to E ∖ \{I\} \subseteq A$
68	56 67	eqssd	$⊢ (φ \land A ∖ (E ∖ \{I, J\}) = \{J\}) \to A = E ∖ \{I\}$
69	68	ex	$⊢ φ \to (A ∖ (E ∖ \{I, J\}) = \{J\} \to A = E ∖ \{I\})$
70	55 69	orim12d	$⊢ φ \to ((A ∖ (E ∖ \{I, J\}) = \emptyset \lor A ∖ (E ∖ \{I, J\}) = \{J\}) \to (A = E ∖ \{I, J\} \lor A = E ∖ \{I\}))$
71	45 70	mpd	$⊢ φ \to (A = E ∖ \{I, J\} \lor A = E ∖ \{I\})$

Metamath Proof Explorer

Theorem pmtrcnelor

Proof