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

Metamath Proof Explorer

Theorem mgm0

Description: Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021)

Ref Expression
Assertion mgm0 ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Mgm )

Proof

Step Hyp Ref Expression
1 rzal ⊢ ( ( Base ‘ 𝑀 ) = ∅ → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
2 1 adantl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
3 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
5 3 4 ismgm ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) )
6 5 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) )
7 2 6 mpbird ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Mgm )