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