This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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