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	\|- ( ph -> D e. V )
	pmtrcnel.f	\|- ( ph -> F e. B )
	pmtrcnel.i	\|- ( ph -> I e. dom ( F \ _I ) )
Assertion	pmtrcnel	\|- ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( 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	\|- ( ph -> D e. V )
6		pmtrcnel.f	\|- ( ph -> F e. B )
7		pmtrcnel.i	\|- ( ph -> I e. dom ( F \ _I ) )
8		mvdco	\|- dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( dom ( ( T ` { I , J } ) \ _I ) u. dom ( F \ _I ) )
9		difss	\|- ( F \ _I ) C_ F
10		dmss	\|- ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
11	9 10	ax-mp	\|- dom ( F \ _I ) C_ dom F
12	11 7	sselid	\|- ( ph -> I e. dom F )
13	1 3	symgbasf1o	\|- ( F e. B -> F : D -1-1-onto-> D )
14		f1of	\|- ( F : D -1-1-onto-> D -> F : D --> D )
15	6 13 14	3syl	\|- ( ph -> F : D --> D )
16	15	fdmd	\|- ( ph -> dom F = D )
17	12 16	eleqtrd	\|- ( ph -> I e. D )
18	15 17	ffvelcdmd	\|- ( ph -> ( F ` I ) e. D )
19	4 18	eqeltrid	\|- ( ph -> J e. D )
20	17 19	prssd	\|- ( ph -> { I , J } C_ D )
21	15	ffnd	\|- ( ph -> F Fn D )
22		fnelnfp	\|- ( ( F Fn D /\ I e. D ) -> ( I e. dom ( F \ _I ) <-> ( F ` I ) =/= I ) )
23	22	biimpa	\|- ( ( ( F Fn D /\ I e. D ) /\ I e. dom ( F \ _I ) ) -> ( F ` I ) =/= I )
24	21 17 7 23	syl21anc	\|- ( ph -> ( F ` I ) =/= I )
25	24	necomd	\|- ( ph -> I =/= ( F ` I ) )
26	4	a1i	\|- ( ph -> J = ( F ` I ) )
27	25 26	neeqtrrd	\|- ( ph -> I =/= J )
28		enpr2	\|- ( ( I e. D /\ J e. D /\ I =/= J ) -> { I , J } ~~ 2o )
29	17 19 27 28	syl3anc	\|- ( ph -> { I , J } ~~ 2o )
30	2	pmtrmvd	\|- ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> dom ( ( T ` { I , J } ) \ _I ) = { I , J } )
31	5 20 29 30	syl3anc	\|- ( ph -> dom ( ( T ` { I , J } ) \ _I ) = { I , J } )
32	6 13	syl	\|- ( ph -> F : D -1-1-onto-> D )
33		f1omvdmvd	\|- ( ( F : D -1-1-onto-> D /\ I e. dom ( F \ _I ) ) -> ( F ` I ) e. ( dom ( F \ _I ) \ { I } ) )
34	32 7 33	syl2anc	\|- ( ph -> ( F ` I ) e. ( dom ( F \ _I ) \ { I } ) )
35	4 34	eqeltrid	\|- ( ph -> J e. ( dom ( F \ _I ) \ { I } ) )
36	35	eldifad	\|- ( ph -> J e. dom ( F \ _I ) )
37	7 36	prssd	\|- ( ph -> { I , J } C_ dom ( F \ _I ) )
38	31 37	eqsstrd	\|- ( ph -> dom ( ( T ` { I , J } ) \ _I ) C_ dom ( F \ _I ) )
39		ssequn1	\|- ( dom ( ( T ` { I , J } ) \ _I ) C_ dom ( F \ _I ) <-> ( dom ( ( T ` { I , J } ) \ _I ) u. dom ( F \ _I ) ) = dom ( F \ _I ) )
40	38 39	sylib	\|- ( ph -> ( dom ( ( T ` { I , J } ) \ _I ) u. dom ( F \ _I ) ) = dom ( F \ _I ) )
41	8 40	sseqtrid	\|- ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ dom ( F \ _I ) )
42	41	sselda	\|- ( ( ph /\ x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) -> x e. dom ( F \ _I ) )
43		simpr	\|- ( ( ph /\ x = I ) -> x = I )
44		eqid	\|- ran T = ran T
45	2 44	pmtrrn	\|- ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> ( T ` { I , J } ) e. ran T )
46	5 20 29 45	syl3anc	\|- ( ph -> ( T ` { I , J } ) e. ran T )
47	2 44	pmtrff1o	\|- ( ( T ` { I , J } ) e. ran T -> ( T ` { I , J } ) : D -1-1-onto-> D )
48	46 47	syl	\|- ( ph -> ( T ` { I , J } ) : D -1-1-onto-> D )
49		f1oco	\|- ( ( ( T ` { I , J } ) : D -1-1-onto-> D /\ F : D -1-1-onto-> D ) -> ( ( T ` { I , J } ) o. F ) : D -1-1-onto-> D )
50	48 32 49	syl2anc	\|- ( ph -> ( ( T ` { I , J } ) o. F ) : D -1-1-onto-> D )
51		f1ofn	\|- ( ( ( T ` { I , J } ) o. F ) : D -1-1-onto-> D -> ( ( T ` { I , J } ) o. F ) Fn D )
52	50 51	syl	\|- ( ph -> ( ( T ` { I , J } ) o. F ) Fn D )
53	15 17	fvco3d	\|- ( ph -> ( ( ( T ` { I , J } ) o. F ) ` I ) = ( ( T ` { I , J } ) ` ( F ` I ) ) )
54	26	eqcomd	\|- ( ph -> ( F ` I ) = J )
55	54	fveq2d	\|- ( ph -> ( ( T ` { I , J } ) ` ( F ` I ) ) = ( ( T ` { I , J } ) ` J ) )
56	2	pmtrprfv2	\|- ( ( D e. V /\ ( I e. D /\ J e. D /\ I =/= J ) ) -> ( ( T ` { I , J } ) ` J ) = I )
57	5 17 19 27 56	syl13anc	\|- ( ph -> ( ( T ` { I , J } ) ` J ) = I )
58	53 55 57	3eqtrd	\|- ( ph -> ( ( ( T ` { I , J } ) o. F ) ` I ) = I )
59		nne	\|- ( -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I <-> ( ( ( T ` { I , J } ) o. F ) ` I ) = I )
60	58 59	sylibr	\|- ( ph -> -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I )
61		fnelnfp	\|- ( ( ( ( T ` { I , J } ) o. F ) Fn D /\ I e. D ) -> ( I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) <-> ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I ) )
62	61	notbid	\|- ( ( ( ( T ` { I , J } ) o. F ) Fn D /\ I e. D ) -> ( -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) <-> -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I ) )
63	62	biimpar	\|- ( ( ( ( ( T ` { I , J } ) o. F ) Fn D /\ I e. D ) /\ -. ( ( ( T ` { I , J } ) o. F ) ` I ) =/= I ) -> -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
64	52 17 60 63	syl21anc	\|- ( ph -> -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
65	64	adantr	\|- ( ( ph /\ x = I ) -> -. I e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
66	43 65	eqneltrd	\|- ( ( ph /\ x = I ) -> -. x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
67	66	ex	\|- ( ph -> ( x = I -> -. x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) )
68	67	necon2ad	\|- ( ph -> ( x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) -> x =/= I ) )
69	68	imp	\|- ( ( ph /\ x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) -> x =/= I )
70		eldifsn	\|- ( x e. ( dom ( F \ _I ) \ { I } ) <-> ( x e. dom ( F \ _I ) /\ x =/= I ) )
71	42 69 70	sylanbrc	\|- ( ( ph /\ x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) -> x e. ( dom ( F \ _I ) \ { I } ) )
72	71	ex	\|- ( ph -> ( x e. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) -> x e. ( dom ( F \ _I ) \ { I } ) ) )
73	72	ssrdv	\|- ( ph -> dom ( ( ( T ` { I , J } ) o. F ) \ _I ) C_ ( dom ( F \ _I ) \ { I } ) )

Metamath Proof Explorer

Theorem pmtrcnel

Proof