Step |
Hyp |
Ref |
Expression |
1 |
|
gsmtrcl.s |
⊢ 𝑆 = ( SymGrp ‘ 𝑁 ) |
2 |
|
gsmtrcl.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
3 |
|
gsmtrcl.t |
⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 ) |
4 |
|
eqid |
⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 ) |
5 |
1 3 4
|
psgneldm2i |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ dom ( pmSgn ‘ 𝑁 ) ) |
6 |
1 4 2
|
psgneldm |
⊢ ( ( 𝑆 Σg 𝑊 ) ∈ dom ( pmSgn ‘ 𝑁 ) ↔ ( ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ∧ dom ( ( 𝑆 Σg 𝑊 ) ∖ I ) ∈ Fin ) ) |
7 |
|
ax-1 |
⊢ ( ( 𝑆 Σg 𝑊 ) ∈ 𝐵 → ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) ) |
8 |
7
|
adantr |
⊢ ( ( ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ∧ dom ( ( 𝑆 Σg 𝑊 ) ∖ I ) ∈ Fin ) → ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) ) |
9 |
6 8
|
sylbi |
⊢ ( ( 𝑆 Σg 𝑊 ) ∈ dom ( pmSgn ‘ 𝑁 ) → ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) ) |
10 |
5 9
|
mpcom |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇 ) → ( 𝑆 Σg 𝑊 ) ∈ 𝐵 ) |