Metamath Proof Explorer


Theorem symgga

Description: The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Hypotheses symgga.g 𝐺 = ( SymGrp ‘ 𝑋 )
symgga.b 𝐵 = ( Base ‘ 𝐺 )
symgga.f 𝐹 = ( 𝑓𝐵 , 𝑥𝑋 ↦ ( 𝑓𝑥 ) )
Assertion symgga ( 𝑋𝑉𝐹 ∈ ( 𝐺 GrpAct 𝑋 ) )

Proof

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 𝑋 ) )