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

Metamath Proof Explorer

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