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

Metamath Proof Explorer

Theorem psgndmsubg

Description: The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgneldm.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgneldm.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion psgndmsubg ( 𝐷 ∈ 𝑉 → dom 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 psgneldm.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgneldm.n ⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 eqid ⊢ { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
5 1 3 4 2 psgnfn ⊢ 𝑁 Fn { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
6 fndm ⊢ ( 𝑁 Fn { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } → dom 𝑁 = { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
7 5 6 ax-mp ⊢ dom 𝑁 = { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
8 1 3 symgfisg ⊢ ( 𝐷 ∈ 𝑉 → { 𝑝 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ∈ ( SubGrp ‘ 𝐺 ) )
9 7 8 eqeltrid ⊢ ( 𝐷 ∈ 𝑉 → dom 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )