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

Metamath Proof Explorer

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