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