Step |
Hyp |
Ref |
Expression |
1 |
|
symgga.g |
⊢ 𝐺 = ( SymGrp ‘ 𝑋 ) |
2 |
|
symgga.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
symgga.f |
⊢ 𝐹 = ( 𝑓 ∈ 𝐵 , 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) |
4 |
1
|
symggrp |
⊢ ( 𝑋 ∈ 𝑉 → 𝐺 ∈ Grp ) |
5 |
2
|
idghm |
⊢ ( 𝐺 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) ) |
6 |
|
fvresi |
⊢ ( 𝑓 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑓 ) = 𝑓 ) |
7 |
6
|
adantr |
⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑥 ∈ 𝑋 ) → ( ( I ↾ 𝐵 ) ‘ 𝑓 ) = 𝑓 ) |
8 |
7
|
fveq1d |
⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑓 ) ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) ) |
9 |
8
|
mpoeq3ia |
⊢ ( 𝑓 ∈ 𝐵 , 𝑥 ∈ 𝑋 ↦ ( ( ( I ↾ 𝐵 ) ‘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝑓 ∈ 𝐵 , 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑥 ) ) |
10 |
3 9
|
eqtr4i |
⊢ 𝐹 = ( 𝑓 ∈ 𝐵 , 𝑥 ∈ 𝑋 ↦ ( ( ( I ↾ 𝐵 ) ‘ 𝑓 ) ‘ 𝑥 ) ) |
11 |
2 1 10
|
lactghmga |
⊢ ( ( I ↾ 𝐵 ) ∈ ( 𝐺 GrpHom 𝐺 ) → 𝐹 ∈ ( 𝐺 GrpAct 𝑋 ) ) |
12 |
4 5 11
|
3syl |
⊢ ( 𝑋 ∈ 𝑉 → 𝐹 ∈ ( 𝐺 GrpAct 𝑋 ) ) |