Theorem 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	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	pmtrcnel.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
	pmtrcnel.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	pmtrcnel.j	⊢ 𝐽 = ( 𝐹 ‘ 𝐼 )
	pmtrcnel.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	pmtrcnel.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	pmtrcnel.i	⊢ ( 𝜑 → 𝐼 ∈ dom ( 𝐹 ∖ I ) )
	pmtrcnel.e	⊢ 𝐸 = dom ( 𝐹 ∖ I )
	pmtrcnel.a	⊢ 𝐴 = dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I )
Assertion	pmtrcnelor	⊢ ( 𝜑 → ( 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∨ 𝐴 = ( 𝐸 ∖ { 𝐼 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmtrcnel.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		pmtrcnel.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
3		pmtrcnel.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		pmtrcnel.j	⊢ 𝐽 = ( 𝐹 ‘ 𝐼 )
5		pmtrcnel.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
6		pmtrcnel.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		pmtrcnel.i	⊢ ( 𝜑 → 𝐼 ∈ dom ( 𝐹 ∖ I ) )
8		pmtrcnel.e	⊢ 𝐸 = dom ( 𝐹 ∖ I )
9		pmtrcnel.a	⊢ 𝐴 = dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I )
10	1 2 3 4 5 6 7	pmtrcnel	⊢ ( 𝜑 → dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ⊆ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
11	8	difeq1i	⊢ ( 𝐸 ∖ { 𝐼 } ) = ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } )
12	10 9 11	3sstr4g	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐸 ∖ { 𝐼 } ) )
13	12	ssdifd	⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) ⊆ ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) )
14		difpr	⊢ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) = ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } )
15	14	difeq2i	⊢ ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } ) )
16	1 3	symgbasf1o	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
17	6 16	syl	⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
18		f1omvdmvd	⊢ ( ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 ∧ 𝐼 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
19	17 7 18	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
20	4 19	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
21	20	eldifad	⊢ ( 𝜑 → 𝐽 ∈ dom ( 𝐹 ∖ I ) )
22	21 8	eleqtrrdi	⊢ ( 𝜑 → 𝐽 ∈ 𝐸 )
23	4	a1i	⊢ ( 𝜑 → 𝐽 = ( 𝐹 ‘ 𝐼 ) )
24		f1of	⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → 𝐹 : 𝐷 ⟶ 𝐷 )
25	17 24	syl	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐷 )
26	25	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
27		difss	⊢ ( 𝐹 ∖ I ) ⊆ 𝐹
28		dmss	⊢ ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
29	27 28	ax-mp	⊢ dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
30	29 7	sselid	⊢ ( 𝜑 → 𝐼 ∈ dom 𝐹 )
31	25	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
32	30 31	eleqtrd	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
33		fnelnfp	⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) → ( 𝐼 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 ) )
34	33	biimpa	⊢ ( ( ( 𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) ∧ 𝐼 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 )
35	26 32 7 34	syl21anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 )
36	23 35	eqnetrd	⊢ ( 𝜑 → 𝐽 ≠ 𝐼 )
37		eldifsn	⊢ ( 𝐽 ∈ ( 𝐸 ∖ { 𝐼 } ) ↔ ( 𝐽 ∈ 𝐸 ∧ 𝐽 ≠ 𝐼 ) )
38	22 36 37	sylanbrc	⊢ ( 𝜑 → 𝐽 ∈ ( 𝐸 ∖ { 𝐼 } ) )
39	38	snssd	⊢ ( 𝜑 → { 𝐽 } ⊆ ( 𝐸 ∖ { 𝐼 } ) )
40		dfss4	⊢ ( { 𝐽 } ⊆ ( 𝐸 ∖ { 𝐼 } ) ↔ ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } ) ) = { 𝐽 } )
41	39 40	sylib	⊢ ( 𝜑 → ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } ) ) = { 𝐽 } )
42	15 41	syl5eq	⊢ ( 𝜑 → ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } )
43	13 42	sseqtrd	⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) ⊆ { 𝐽 } )
44		sssn	⊢ ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) ⊆ { 𝐽 } ↔ ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ∨ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) )
45	43 44	sylib	⊢ ( 𝜑 → ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ∨ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) )
46		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ) → ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ )
47	1 2 3 4 5 6 7	pmtrcnel2	⊢ ( 𝜑 → ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 , 𝐽 } ) ⊆ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )
48	8	difeq1i	⊢ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) = ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 , 𝐽 } )
49	47 48 9	3sstr4g	⊢ ( 𝜑 → ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ⊆ 𝐴 )
50		ssdif0	⊢ ( ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ⊆ 𝐴 ↔ ( ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∖ 𝐴 ) = ∅ )
51	49 50	sylib	⊢ ( 𝜑 → ( ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∖ 𝐴 ) = ∅ )
52	51	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ) → ( ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∖ 𝐴 ) = ∅ )
53		eqdif	⊢ ( ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ∧ ( ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∖ 𝐴 ) = ∅ ) → 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) )
54	46 52 53	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ) → 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) )
55	54	ex	⊢ ( 𝜑 → ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ → 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) )
56	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → 𝐴 ⊆ ( 𝐸 ∖ { 𝐼 } ) )
57	14 49	eqsstrrid	⊢ ( 𝜑 → ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } ) ⊆ 𝐴 )
58	57	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } ) ⊆ 𝐴 )
59		ssundif	⊢ ( ( 𝐸 ∖ { 𝐼 } ) ⊆ ( { 𝐽 } ∪ 𝐴 ) ↔ ( ( 𝐸 ∖ { 𝐼 } ) ∖ { 𝐽 } ) ⊆ 𝐴 )
60	58 59	sylibr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → ( 𝐸 ∖ { 𝐼 } ) ⊆ ( { 𝐽 } ∪ 𝐴 ) )
61		ssidd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → { 𝐽 } ⊆ { 𝐽 } )
62		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } )
63	61 62	sseqtrrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → { 𝐽 } ⊆ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) )
64	63	difss2d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → { 𝐽 } ⊆ 𝐴 )
65		ssequn1	⊢ ( { 𝐽 } ⊆ 𝐴 ↔ ( { 𝐽 } ∪ 𝐴 ) = 𝐴 )
66	64 65	sylib	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → ( { 𝐽 } ∪ 𝐴 ) = 𝐴 )
67	60 66	sseqtrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → ( 𝐸 ∖ { 𝐼 } ) ⊆ 𝐴 )
68	56 67	eqssd	⊢ ( ( 𝜑 ∧ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → 𝐴 = ( 𝐸 ∖ { 𝐼 } ) )
69	68	ex	⊢ ( 𝜑 → ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } → 𝐴 = ( 𝐸 ∖ { 𝐼 } ) ) )
70	55 69	orim12d	⊢ ( 𝜑 → ( ( ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = ∅ ∨ ( 𝐴 ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } ) → ( 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∨ 𝐴 = ( 𝐸 ∖ { 𝐼 } ) ) ) )
71	45 70	mpd	⊢ ( 𝜑 → ( 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∨ 𝐴 = ( 𝐸 ∖ { 𝐼 } ) ) )