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 
|- B = ( Base ` G )
ismnd.p 
|- .+ = ( +g ` G )
Assertion ismnd 
|- ( G e. Mnd <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )

Proof

Step Hyp Ref Expression
1 ismnd.b 
 |-  B = ( Base ` G )
2 ismnd.p 
 |-  .+ = ( +g ` G )
3 1 2 ismnddef 
 |-  ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
4 rexn0 
 |-  ( E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) -> B =/= (/) )
5 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
6 1 5 eqtrid 
 |-  ( -. G e. _V -> B = (/) )
7 6 necon1ai 
 |-  ( B =/= (/) -> G e. _V )
8 1 2 issgrpv 
 |-  ( G e. _V -> ( G e. Smgrp <-> A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) ) )
9 4 7 8 3syl 
 |-  ( E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) -> ( G e. Smgrp <-> A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) ) )
10 9 pm5.32ri 
 |-  ( ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
11 3 10 bitri 
 |-  ( G e. Mnd <-> ( A. a e. B A. b e. B ( ( a .+ b ) e. B /\ A. c e. B ( ( a .+ b ) .+ c ) = ( a .+ ( b .+ c ) ) ) /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )