pmtrcnel

Description: Composing a permutation F with a transposition which results in moving at least one less point. Here the set of points moved by a permutation F is expressed as dom ( F \ _I ) . (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)$
Assertion	pmtrcnel	$⊢ φ \to dom ((T (\{I, J\}) \circ F) ∖ I) \subseteq dom (F ∖ I) ∖ \{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		mvdco	$⊢ dom ((T (\{I, J\}) \circ F) ∖ I) \subseteq dom (T (\{I, J\}) ∖ I) \cup dom (F ∖ I)$
9		difss	$⊢ F ∖ I \subseteq F$
10		dmss	$⊢ F ∖ I \subseteq F \to dom (F ∖ I) \subseteq dom F$
11	9 10	ax-mp	$⊢ dom (F ∖ I) \subseteq dom F$
12	11 7	sselid	$⊢ φ \to I \in dom F$
13	1 3	symgbasf1o	$⊢ F \in B \to F : D \underset{1-1 onto}{⟶} D$
14		f1of	$⊢ F : D \underset{1-1 onto}{⟶} D \to F : D ⟶ D$
15	6 13 14	3syl	$⊢ φ \to F : D ⟶ D$
16	15	fdmd	$⊢ φ \to dom F = D$
17	12 16	eleqtrd	$⊢ φ \to I \in D$
18	15 17	ffvelcdmd	$⊢ φ \to F (I) \in D$
19	4 18	eqeltrid	$⊢ φ \to J \in D$
20	17 19	prssd	$⊢ φ \to \{I, J\} \subseteq D$
21	15	ffnd	$⊢ φ \to F Fn D$
22		fnelnfp	$⊢ (F Fn D \land I \in D) \to (I \in dom (F ∖ I) \leftrightarrow F (I) \neq I)$
23	22	biimpa	$⊢ ((F Fn D \land I \in D) \land I \in dom (F ∖ I)) \to F (I) \neq I$
24	21 17 7 23	syl21anc	$⊢ φ \to F (I) \neq I$
25	24	necomd	$⊢ φ \to I \neq F (I)$
26	4	a1i	$⊢ φ \to J = F (I)$
27	25 26	neeqtrrd	$⊢ φ \to I \neq J$
28		enpr2	$⊢ (I \in D \land J \in D \land I \neq J) \to \{I, J\} \approx 2_{𝑜}$
29	17 19 27 28	syl3anc	$⊢ φ \to \{I, J\} \approx 2_{𝑜}$
30	2	pmtrmvd	$⊢ (D \in V \land \{I, J\} \subseteq D \land \{I, J\} \approx 2_{𝑜}) \to dom (T (\{I, J\}) ∖ I) = \{I, J\}$
31	5 20 29 30	syl3anc	$⊢ φ \to dom (T (\{I, J\}) ∖ I) = \{I, J\}$
32	6 13	syl	$⊢ φ \to F : D \underset{1-1 onto}{⟶} D$
33		f1omvdmvd	$⊢ (F : D \underset{1-1 onto}{⟶} D \land I \in dom (F ∖ I)) \to F (I) \in (dom (F ∖ I) ∖ \{I\})$
34	32 7 33	syl2anc	$⊢ φ \to F (I) \in (dom (F ∖ I) ∖ \{I\})$
35	4 34	eqeltrid	$⊢ φ \to J \in (dom (F ∖ I) ∖ \{I\})$
36	35	eldifad	$⊢ φ \to J \in dom (F ∖ I)$
37	7 36	prssd	$⊢ φ \to \{I, J\} \subseteq dom (F ∖ I)$
38	31 37	eqsstrd	$⊢ φ \to dom (T (\{I, J\}) ∖ I) \subseteq dom (F ∖ I)$
39		ssequn1	$⊢ dom (T (\{I, J\}) ∖ I) \subseteq dom (F ∖ I) \leftrightarrow dom (T (\{I, J\}) ∖ I) \cup dom (F ∖ I) = dom (F ∖ I)$
40	38 39	sylib	$⊢ φ \to dom (T (\{I, J\}) ∖ I) \cup dom (F ∖ I) = dom (F ∖ I)$
41	8 40	sseqtrid	$⊢ φ \to dom ((T (\{I, J\}) \circ F) ∖ I) \subseteq dom (F ∖ I)$
42	41	sselda	$⊢ (φ \land x \in dom ((T (\{I, J\}) \circ F) ∖ I)) \to x \in dom (F ∖ I)$
43		simpr	$⊢ (φ \land x = I) \to x = I$
44		eqid	$⊢ ran T = ran T$
45	2 44	pmtrrn	$⊢ (D \in V \land \{I, J\} \subseteq D \land \{I, J\} \approx 2_{𝑜}) \to T (\{I, J\}) \in ran T$
46	5 20 29 45	syl3anc	$⊢ φ \to T (\{I, J\}) \in ran T$
47	2 44	pmtrff1o	$⊢ T (\{I, J\}) \in ran T \to T (\{I, J\}) : D \underset{1-1 onto}{⟶} D$
48	46 47	syl	$⊢ φ \to T (\{I, J\}) : D \underset{1-1 onto}{⟶} D$
49		f1oco	$⊢ (T (\{I, J\}) : D \underset{1-1 onto}{⟶} D \land F : D \underset{1-1 onto}{⟶} D) \to (T (\{I, J\}) \circ F) : D \underset{1-1 onto}{⟶} D$
50	48 32 49	syl2anc	$⊢ φ \to (T (\{I, J\}) \circ F) : D \underset{1-1 onto}{⟶} D$
51		f1ofn	$⊢ (T (\{I, J\}) \circ F) : D \underset{1-1 onto}{⟶} D \to (T (\{I, J\}) \circ F) Fn D$
52	50 51	syl	$⊢ φ \to (T (\{I, J\}) \circ F) Fn D$
53	15 17	fvco3d	$⊢ φ \to (T (\{I, J\}) \circ F) (I) = T (\{I, J\}) (F (I))$
54	26	eqcomd	$⊢ φ \to F (I) = J$
55	54	fveq2d	$⊢ φ \to T (\{I, J\}) (F (I)) = T (\{I, J\}) (J)$
56	2	pmtrprfv2	$⊢ (D \in V \land (I \in D \land J \in D \land I \neq J)) \to T (\{I, J\}) (J) = I$
57	5 17 19 27 56	syl13anc	$⊢ φ \to T (\{I, J\}) (J) = I$
58	53 55 57	3eqtrd	$⊢ φ \to (T (\{I, J\}) \circ F) (I) = I$
59		nne	$⊢ \neg (T (\{I, J\}) \circ F) (I) \neq I \leftrightarrow (T (\{I, J\}) \circ F) (I) = I$
60	58 59	sylibr	$⊢ φ \to \neg (T (\{I, J\}) \circ F) (I) \neq I$
61		fnelnfp	$⊢ ((T (\{I, J\}) \circ F) Fn D \land I \in D) \to (I \in dom ((T (\{I, J\}) \circ F) ∖ I) \leftrightarrow (T (\{I, J\}) \circ F) (I) \neq I)$
62	61	notbid	$⊢ ((T (\{I, J\}) \circ F) Fn D \land I \in D) \to (\neg I \in dom ((T (\{I, J\}) \circ F) ∖ I) \leftrightarrow \neg (T (\{I, J\}) \circ F) (I) \neq I)$
63	62	biimpar	$⊢ (((T (\{I, J\}) \circ F) Fn D \land I \in D) \land \neg (T (\{I, J\}) \circ F) (I) \neq I) \to \neg I \in dom ((T (\{I, J\}) \circ F) ∖ I)$
64	52 17 60 63	syl21anc	$⊢ φ \to \neg I \in dom ((T (\{I, J\}) \circ F) ∖ I)$
65	64	adantr	$⊢ (φ \land x = I) \to \neg I \in dom ((T (\{I, J\}) \circ F) ∖ I)$
66	43 65	eqneltrd	$⊢ (φ \land x = I) \to \neg x \in dom ((T (\{I, J\}) \circ F) ∖ I)$
67	66	ex	$⊢ φ \to (x = I \to \neg x \in dom ((T (\{I, J\}) \circ F) ∖ I))$
68	67	necon2ad	$⊢ φ \to (x \in dom ((T (\{I, J\}) \circ F) ∖ I) \to x \neq I)$
69	68	imp	$⊢ (φ \land x \in dom ((T (\{I, J\}) \circ F) ∖ I)) \to x \neq I$
70		eldifsn	$⊢ x \in (dom (F ∖ I) ∖ \{I\}) \leftrightarrow (x \in dom (F ∖ I) \land x \neq I)$
71	42 69 70	sylanbrc	$⊢ (φ \land x \in dom ((T (\{I, J\}) \circ F) ∖ I)) \to x \in (dom (F ∖ I) ∖ \{I\})$
72	71	ex	$⊢ φ \to (x \in dom ((T (\{I, J\}) \circ F) ∖ I) \to x \in (dom (F ∖ I) ∖ \{I\}))$
73	72	ssrdv	$⊢ φ \to dom ((T (\{I, J\}) \circ F) ∖ I) \subseteq dom (F ∖ I) ∖ \{I\}$

Metamath Proof Explorer

Theorem pmtrcnel

Proof