Step |
Hyp |
Ref |
Expression |
1 |
|
orbsta2.x |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
2 |
|
orbsta2.h |
⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐴 ) = 𝐴 } |
3 |
|
orbsta2.r |
⊢ ∼ = ( 𝐺 ~QG 𝐻 ) |
4 |
|
orbsta2.o |
⊢ 𝑂 = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) } |
5 |
1 2
|
gastacl |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
6 |
5
|
adantr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
7 |
|
simpr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → 𝑋 ∈ Fin ) |
8 |
1 3 6 7
|
lagsubg2 |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐻 ) ) ) |
9 |
|
pwfi |
⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin ) |
10 |
7 9
|
sylib |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → 𝒫 𝑋 ∈ Fin ) |
11 |
1 3
|
eqger |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 ) |
12 |
6 11
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ∼ Er 𝑋 ) |
13 |
12
|
qsss |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( 𝑋 / ∼ ) ⊆ 𝒫 𝑋 ) |
14 |
10 13
|
ssfid |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( 𝑋 / ∼ ) ∈ Fin ) |
15 |
|
eqid |
⊢ ran ( 𝑘 ∈ 𝑋 ↦ 〈 [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) 〉 ) = ran ( 𝑘 ∈ 𝑋 ↦ 〈 [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) 〉 ) |
16 |
1 2 3 15 4
|
orbsta |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) → ran ( 𝑘 ∈ 𝑋 ↦ 〈 [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) 〉 ) : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 ) |
17 |
16
|
adantr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ran ( 𝑘 ∈ 𝑋 ↦ 〈 [ 𝑘 ] ∼ , ( 𝑘 ⊕ 𝐴 ) 〉 ) : ( 𝑋 / ∼ ) –1-1-onto→ [ 𝐴 ] 𝑂 ) |
18 |
14 17
|
hasheqf1od |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ ( 𝑋 / ∼ ) ) = ( ♯ ‘ [ 𝐴 ] 𝑂 ) ) |
19 |
18
|
oveq1d |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ( ♯ ‘ ( 𝑋 / ∼ ) ) · ( ♯ ‘ 𝐻 ) ) = ( ( ♯ ‘ [ 𝐴 ] 𝑂 ) · ( ♯ ‘ 𝐻 ) ) ) |
20 |
8 19
|
eqtrd |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝐴 ∈ 𝑌 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐴 ] 𝑂 ) · ( ♯ ‘ 𝐻 ) ) ) |