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

Metamath Proof Explorer

Theorem psgnevpmb

Description: A class is an even permutation if it is a permutation with sign 1. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses evpmss.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
evpmss.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
psgnevpmb.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgnevpmb ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 evpmss.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 evpmss.p ⊢ 𝑃 = ( Base ‘ 𝑆 )
3 psgnevpmb.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
4 elex ⊢ ( 𝐷 ∈ Fin → 𝐷 ∈ V )
5 fveq2 ⊢ ( 𝑑 = 𝐷 → ( pmSgn ‘ 𝑑 ) = ( pmSgn ‘ 𝐷 ) )
6 5 3 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( pmSgn ‘ 𝑑 ) = 𝑁 )
7 6 cnveqd ⊢ ( 𝑑 = 𝐷 → ◡ ( pmSgn ‘ 𝑑 ) = ◡ 𝑁 )
8 7 imaeq1d ⊢ ( 𝑑 = 𝐷 → ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) = ( ◡ 𝑁 “ { 1 } ) )
9 df-evpm ⊢ pmEven = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )
10 3 fvexi ⊢ 𝑁 ∈ V
11 10 cnvex ⊢ ◡ 𝑁 ∈ V
12 11 imaex ⊢ ( ◡ 𝑁 “ { 1 } ) ∈ V
13 8 9 12 fvmpt ⊢ ( 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) = ( ◡ 𝑁 “ { 1 } ) )
14 4 13 syl ⊢ ( 𝐷 ∈ Fin → ( pmEven ‘ 𝐷 ) = ( ◡ 𝑁 “ { 1 } ) )
15 14 eleq2d ⊢ ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) ↔ 𝐹 ∈ ( ◡ 𝑁 “ { 1 } ) ) )
16 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
17 1 3 16 psgnghm2 ⊢ ( 𝐷 ∈ Fin → 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
18 eqid ⊢ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
19 2 18 ghmf ⊢ ( 𝑁 ∈ ( 𝑆 GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → 𝑁 : 𝑃 ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
20 ffn ⊢ ( 𝑁 : 𝑃 ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → 𝑁 Fn 𝑃 )
21 fniniseg ⊢ ( 𝑁 Fn 𝑃 → ( 𝐹 ∈ ( ◡ 𝑁 “ { 1 } ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )
22 17 19 20 21 4syl ⊢ ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( ◡ 𝑁 “ { 1 } ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )
23 15 22 bitrd ⊢ ( 𝐷 ∈ Fin → ( 𝐹 ∈ ( pmEven ‘ 𝐷 ) ↔ ( 𝐹 ∈ 𝑃 ∧ ( 𝑁 ‘ 𝐹 ) = 1 ) ) )