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

Metamath Proof Explorer

Theorem ismnd

Description: The predicate "is a monoid". This is the defining theorem of a monoid by showing that a set is a monoid if and only if it is a set equipped with a closed, everywhere defined internal operation (so, a magma, see mndcl ), whose operation is associative (so, a semigroup, see also mndass ) and has a two-sided neutral element (see mndid ). (Contributed by Mario Carneiro, 6-Jan-2015) (Revised by AV, 1-Feb-2020)

Ref Expression
Hypotheses ismnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ismnd.p ⊢ + = ( +g ‘ 𝐺 )
Assertion ismnd ( 𝐺 ∈ Mnd ↔ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) ∈ 𝐵 ∧ ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) ) ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )

Proof

Step Hyp Ref Expression
1 ismnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ismnd.p ⊢ + = ( +g ‘ 𝐺 )
3 1 2 ismnddef ⊢ ( 𝐺 ∈ Mnd ↔ ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
4 rexn0 ⊢ ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) → 𝐵 ≠ ∅ )
5 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
6 1 5 eqtrid ⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
7 6 necon1ai ⊢ ( 𝐵 ≠ ∅ → 𝐺 ∈ V )
8 1 2 issgrpv ⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) ∈ 𝐵 ∧ ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) ) ) )
9 4 7 8 3syl ⊢ ( ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) → ( 𝐺 ∈ Smgrp ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) ∈ 𝐵 ∧ ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) ) ) )
10 9 pm5.32ri ⊢ ( ( 𝐺 ∈ Smgrp ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) ↔ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) ∈ 𝐵 ∧ ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) ) ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )
11 3 10 bitri ⊢ ( 𝐺 ∈ Mnd ↔ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) ∈ 𝐵 ∧ ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 + 𝑏 ) + 𝑐 ) = ( 𝑎 + ( 𝑏 + 𝑐 ) ) ) ∧ ∃ 𝑒 ∈ 𝐵 ∀ 𝑎 ∈ 𝐵 ( ( 𝑒 + 𝑎 ) = 𝑎 ∧ ( 𝑎 + 𝑒 ) = 𝑎 ) ) )