This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → ( ( 𝐸 ∖ { 𝐼 } ) ∖ ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ) = { 𝐽 } )
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 ⊢ ( 𝜑 → ( 𝐴 = ( 𝐸 ∖ { 𝐼 , 𝐽 } ) ∨ 𝐴 = ( 𝐸 ∖ { 𝐼 } ) ) )