Theorem evpmss

Description: Even permutations are permutations. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	evpmss.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	evpmss.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
Assertion	evpmss	⊢ ( pmEven ‘ 𝐷 ) ⊆ 𝑃

Proof

Step	Hyp	Ref	Expression
1		evpmss.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2		evpmss.p	⊢ 𝑃 = ( Base ‘ 𝑆 )
3		fveq2	⊢ ( 𝑑 = 𝐷 → ( pmSgn ‘ 𝑑 ) = ( pmSgn ‘ 𝐷 ) )
4	3	cnveqd	⊢ ( 𝑑 = 𝐷 → ◡ ( pmSgn ‘ 𝑑 ) = ◡ ( pmSgn ‘ 𝐷 ) )
5	4	imaeq1d	⊢ ( 𝑑 = 𝐷 → ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
6		df-evpm	⊢ pmEven = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )
7		fvex	⊢ ( pmSgn ‘ 𝐷 ) ∈ V
8	7	cnvex	⊢ ◡ ( pmSgn ‘ 𝐷 ) ∈ V
9	8	imaex	⊢ ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ V
10	5 6 9	fvmpt	⊢ ( 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
11		cnvimass	⊢ ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ⊆ dom ( pmSgn ‘ 𝐷 )
12		eqid	⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 )
13		eqid	⊢ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) = ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) )
14		eqid	⊢ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
15	1 12 13 14	psgnghm	⊢ ( 𝐷 ∈ V → ( pmSgn ‘ 𝐷 ) ∈ ( ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
16		eqid	⊢ ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) ) = ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) )
17		eqid	⊢ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) )
18	16 17	ghmf	⊢ ( ( pmSgn ‘ 𝐷 ) ∈ ( ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → ( pmSgn ‘ 𝐷 ) : ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) ) ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) )
19		fdm	⊢ ( ( pmSgn ‘ 𝐷 ) : ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) ) ⟶ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } ) ) → dom ( pmSgn ‘ 𝐷 ) = ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) ) )
20	15 18 19	3syl	⊢ ( 𝐷 ∈ V → dom ( pmSgn ‘ 𝐷 ) = ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) ) )
21	13 2	ressbasss	⊢ ( Base ‘ ( 𝑆 ↾s dom ( pmSgn ‘ 𝐷 ) ) ) ⊆ 𝑃
22	20 21	eqsstrdi	⊢ ( 𝐷 ∈ V → dom ( pmSgn ‘ 𝐷 ) ⊆ 𝑃 )
23	11 22	sstrid	⊢ ( 𝐷 ∈ V → ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ⊆ 𝑃 )
24	10 23	eqsstrd	⊢ ( 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) ⊆ 𝑃 )
25		fvprc	⊢ ( ¬ 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) = ∅ )
26		0ss	⊢ ∅ ⊆ 𝑃
27	25 26	eqsstrdi	⊢ ( ¬ 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) ⊆ 𝑃 )
28	24 27	pm2.61i	⊢ ( pmEven ‘ 𝐷 ) ⊆ 𝑃