Description: The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | evpmid.1 | ⊢ 𝑆 = ( SymGrp ‘ 𝐷 ) | |
Assertion | evpmid | ⊢ ( 𝐷 ∈ Fin → ( I ↾ 𝐷 ) ∈ ( pmEven ‘ 𝐷 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evpmid.1 | ⊢ 𝑆 = ( SymGrp ‘ 𝐷 ) | |
2 | 1 | idresperm | ⊢ ( 𝐷 ∈ Fin → ( I ↾ 𝐷 ) ∈ ( Base ‘ 𝑆 ) ) |
3 | eqid | ⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 ) | |
4 | 3 | psgnid | ⊢ ( 𝐷 ∈ Fin → ( ( pmSgn ‘ 𝐷 ) ‘ ( I ↾ 𝐷 ) ) = 1 ) |
5 | eqid | ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) | |
6 | 1 5 3 | psgnevpmb | ⊢ ( 𝐷 ∈ Fin → ( ( I ↾ 𝐷 ) ∈ ( pmEven ‘ 𝐷 ) ↔ ( ( I ↾ 𝐷 ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( pmSgn ‘ 𝐷 ) ‘ ( I ↾ 𝐷 ) ) = 1 ) ) ) |
7 | 2 4 6 | mpbir2and | ⊢ ( 𝐷 ∈ Fin → ( I ↾ 𝐷 ) ∈ ( pmEven ‘ 𝐷 ) ) |