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