Theorem ga0

Description: The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Assertion	ga0	⊢ ( 𝐺 ∈ Grp → ∅ ∈ ( 𝐺 GrpAct ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	jctr	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) )
3		f0	⊢ ∅ : ∅ ⟶ ∅
4		xp0	⊢ ( ( Base ‘ 𝐺 ) × ∅ ) = ∅
5	4	feq2i	⊢ ( ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅ )
6	3 5	mpbir	⊢ ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅
7		ral0	⊢ ∀ 𝑥 ∈ ∅ ( ( ( 0g ‘ 𝐺 ) ∅ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∅ 𝑥 ) = ( 𝑦 ∅ ( 𝑧 ∅ 𝑥 ) ) )
8	6 7	pm3.2i	⊢ ( ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( ( 0g ‘ 𝐺 ) ∅ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∅ 𝑥 ) = ( 𝑦 ∅ ( 𝑧 ∅ 𝑥 ) ) ) )
9		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
12	9 10 11	isga	⊢ ( ∅ ∈ ( 𝐺 GrpAct ∅ ) ↔ ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) ∧ ( ∅ : ( ( Base ‘ 𝐺 ) × ∅ ) ⟶ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( ( 0g ‘ 𝐺 ) ∅ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∅ 𝑥 ) = ( 𝑦 ∅ ( 𝑧 ∅ 𝑥 ) ) ) ) ) )
13	2 8 12	sylanblrc	⊢ ( 𝐺 ∈ Grp → ∅ ∈ ( 𝐺 GrpAct ∅ ) )