Step |
Hyp |
Ref |
Expression |
1 |
|
psgnfitr.g |
⊢ 𝐺 = ( SymGrp ‘ 𝑁 ) |
2 |
|
psgnfitr.p |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
psgnfitr.t |
⊢ 𝑇 = ran ( pmTrsp ‘ 𝑁 ) |
4 |
|
eqid |
⊢ ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) = ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) |
5 |
3 1 2 4
|
symggen2 |
⊢ ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = 𝐵 ) |
6 |
1
|
symggrp |
⊢ ( 𝑁 ∈ Fin → 𝐺 ∈ Grp ) |
7 |
6
|
grpmndd |
⊢ ( 𝑁 ∈ Fin → 𝐺 ∈ Mnd ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
9 |
3 1 8
|
symgtrf |
⊢ 𝑇 ⊆ ( Base ‘ 𝐺 ) |
10 |
8 4
|
gsumwspan |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) |
11 |
7 9 10
|
sylancl |
⊢ ( 𝑁 ∈ Fin → ( ( mrCls ‘ ( SubMnd ‘ 𝐺 ) ) ‘ 𝑇 ) = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) |
12 |
5 11
|
eqtr3d |
⊢ ( 𝑁 ∈ Fin → 𝐵 = ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) |
13 |
12
|
eleq2d |
⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝐵 ↔ 𝑄 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ) ) |
14 |
|
eqid |
⊢ ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) = ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) |
15 |
|
ovex |
⊢ ( 𝐺 Σg 𝑤 ) ∈ V |
16 |
14 15
|
elrnmpti |
⊢ ( 𝑄 ∈ ran ( 𝑤 ∈ Word 𝑇 ↦ ( 𝐺 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) ) |
17 |
13 16
|
bitrdi |
⊢ ( 𝑁 ∈ Fin → ( 𝑄 ∈ 𝐵 ↔ ∃ 𝑤 ∈ Word 𝑇 𝑄 = ( 𝐺 Σg 𝑤 ) ) ) |