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