Metamath Proof Explorer

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

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 mvdco ⊢ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ⊆ ( dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( 𝐹 ∖ I ) )
9 difss ⊢ ( 𝐹 ∖ I ) ⊆ 𝐹
10 dmss ⊢ ( ( 𝐹 ∖ I ) ⊆ 𝐹 → dom ( 𝐹 ∖ I ) ⊆ dom 𝐹 )
11 9 10 ax-mp ⊢ dom ( 𝐹 ∖ I ) ⊆ dom 𝐹
12 11 7 sselid ⊢ ( 𝜑 → 𝐼 ∈ dom 𝐹 )
13 1 3 symgbasf1o ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
14 f1of ⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 → 𝐹 : 𝐷 ⟶ 𝐷 )
15 6 13 14 3syl ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ 𝐷 )
16 15 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
17 12 16 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
18 15 17 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ 𝐷 )
19 4 18 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
20 17 19 prssd ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ 𝐷 )
21 15 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
22 fnelnfp ⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) → ( 𝐼 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 ) )
23 22 biimpa ⊢ ( ( ( 𝐹 Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) ∧ 𝐼 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 )
24 21 17 7 23 syl21anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ≠ 𝐼 )
25 24 necomd ⊢ ( 𝜑 → 𝐼 ≠ ( 𝐹 ‘ 𝐼 ) )
26 4 a1i ⊢ ( 𝜑 → 𝐽 = ( 𝐹 ‘ 𝐼 ) )
27 25 26 neeqtrrd ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
28 enpr2 ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽 ) → { 𝐼 , 𝐽 } ≈ 2o )
29 17 19 27 28 syl3anc ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ≈ 2o )
30 2 pmtrmvd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
31 5 20 29 30 syl3anc ⊢ ( 𝜑 → dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) = { 𝐼 , 𝐽 } )
32 6 13 syl ⊢ ( 𝜑 → 𝐹 : 𝐷 –1-1-onto→ 𝐷 )
33 f1omvdmvd ⊢ ( ( 𝐹 : 𝐷 –1-1-onto→ 𝐷 ∧ 𝐼 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
34 32 7 33 syl2anc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
35 4 34 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
36 35 eldifad ⊢ ( 𝜑 → 𝐽 ∈ dom ( 𝐹 ∖ I ) )
37 7 36 prssd ⊢ ( 𝜑 → { 𝐼 , 𝐽 } ⊆ dom ( 𝐹 ∖ I ) )
38 31 37 eqsstrd ⊢ ( 𝜑 → dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ⊆ dom ( 𝐹 ∖ I ) )
39 ssequn1 ⊢ ( dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ⊆ dom ( 𝐹 ∖ I ) ↔ ( dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( 𝐹 ∖ I ) ) = dom ( 𝐹 ∖ I ) )
40 38 39 sylib ⊢ ( 𝜑 → ( dom ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∖ I ) ∪ dom ( 𝐹 ∖ I ) ) = dom ( 𝐹 ∖ I ) )
41 8 40 sseqtrid ⊢ ( 𝜑 → dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ⊆ dom ( 𝐹 ∖ I ) )
42 41 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) → 𝑥 ∈ dom ( 𝐹 ∖ I ) )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐼 ) → 𝑥 = 𝐼 )
44 eqid ⊢ ran 𝑇 = ran 𝑇
45 2 44 pmtrrn ⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 )
46 5 20 29 45 syl3anc ⊢ ( 𝜑 → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 )
47 2 44 pmtrff1o ⊢ ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∈ ran 𝑇 → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) : 𝐷 –1-1-onto→ 𝐷 )
48 46 47 syl ⊢ ( 𝜑 → ( 𝑇 ‘ { 𝐼 , 𝐽 } ) : 𝐷 –1-1-onto→ 𝐷 )
49 f1oco ⊢ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) : 𝐷 –1-1-onto→ 𝐷 ∧ 𝐹 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) : 𝐷 –1-1-onto→ 𝐷 )
50 48 32 49 syl2anc ⊢ ( 𝜑 → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) : 𝐷 –1-1-onto→ 𝐷 )
51 f1ofn ⊢ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) : 𝐷 –1-1-onto→ 𝐷 → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) Fn 𝐷 )
52 50 51 syl ⊢ ( 𝜑 → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) Fn 𝐷 )
53 15 17 fvco3d ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) = ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝐹 ‘ 𝐼 ) ) )
54 26 eqcomd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) = 𝐽 )
55 54 fveq2d ⊢ ( 𝜑 → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ‘ ( 𝐹 ‘ 𝐼 ) ) = ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) )
56 2 pmtrprfv2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽 ) ) → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) = 𝐼 )
57 5 17 19 27 56 syl13anc ⊢ ( 𝜑 → ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ‘ 𝐽 ) = 𝐼 )
58 53 55 57 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) = 𝐼 )
59 nne ⊢ ( ¬ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) ≠ 𝐼 ↔ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) = 𝐼 )
60 58 59 sylibr ⊢ ( 𝜑 → ¬ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) ≠ 𝐼 )
61 fnelnfp ⊢ ( ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) → ( 𝐼 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ↔ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) ≠ 𝐼 ) )
62 61 notbid ⊢ ( ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) → ( ¬ 𝐼 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ↔ ¬ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) ≠ 𝐼 ) )
63 62 biimpar ⊢ ( ( ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) Fn 𝐷 ∧ 𝐼 ∈ 𝐷 ) ∧ ¬ ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ‘ 𝐼 ) ≠ 𝐼 ) → ¬ 𝐼 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )
64 52 17 60 63 syl21anc ⊢ ( 𝜑 → ¬ 𝐼 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐼 ) → ¬ 𝐼 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )
66 43 65 eqneltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐼 ) → ¬ 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) )
67 66 ex ⊢ ( 𝜑 → ( 𝑥 = 𝐼 → ¬ 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) )
68 67 necon2ad ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) → 𝑥 ≠ 𝐼 ) )
69 68 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) → 𝑥 ≠ 𝐼 )
70 eldifsn ⊢ ( 𝑥 ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) ↔ ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ∧ 𝑥 ≠ 𝐼 ) )
71 42 69 70 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ) → 𝑥 ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )
72 71 ex ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) → 𝑥 ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) ) )
73 72 ssrdv ⊢ ( 𝜑 → dom ( ( ( 𝑇 ‘ { 𝐼 , 𝐽 } ) ∘ 𝐹 ) ∖ I ) ⊆ ( dom ( 𝐹 ∖ I ) ∖ { 𝐼 } ) )