Metamath Proof Explorer


Theorem evpmid

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 ‘ 𝐷 ) )

Proof

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 ‘ 𝐷 ) )