Step |
Hyp |
Ref |
Expression |
1 |
|
psgnfitr.g |
⊢ 𝐺 = ( SymGrp ‘ 𝑁 ) |
2 |
|
psgnfitr.p |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
psgnfitr.t |
⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 ) |
4 |
|
simpr |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → 𝑄 ∈ 𝐵 ) |
5 |
1 2
|
sygbasnfpfi |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → dom ( 𝑄 ∖ I ) ∈ Fin ) |
6 |
|
eqid |
⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 ) |
7 |
1 6 2
|
psgneldm |
⊢ ( 𝑄 ∈ dom ( pmSgn ‘ 𝑁 ) ↔ ( 𝑄 ∈ 𝐵 ∧ dom ( 𝑄 ∖ I ) ∈ Fin ) ) |
8 |
4 5 7
|
sylanbrc |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → 𝑄 ∈ dom ( pmSgn ‘ 𝑁 ) ) |
9 |
1 3 6
|
psgneu |
⊢ ( 𝑄 ∈ dom ( pmSgn ‘ 𝑁 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |
10 |
8 9
|
syl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵 ) → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑄 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |