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

Metamath Proof Explorer

Theorem sgrpidmnd

Description: A semigroup with an identity element which is not the empty set is a monoid. Of course there could be monoids with the empty set as identity element (see, for example, the monoid of the power set of a class under union, pwmnd and pwmndid ), but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024)

Ref Expression
Hypotheses sgrpidmnd.b 
|- B = ( Base ` G )
sgrpidmnd.0 
|- .0. = ( 0g ` G )
Assertion sgrpidmnd 
|- ( ( G e. Smgrp /\ E. e e. B ( e =/= (/) /\ e = .0. ) ) -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 sgrpidmnd.b 
 |-  B = ( Base ` G )
2 sgrpidmnd.0 
 |-  .0. = ( 0g ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 1 3 2 grpidval 
 |-  .0. = ( iota y ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) )
5 4 eqeq2i 
 |-  ( e = .0. <-> e = ( iota y ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) ) )
6 eleq1w 
 |-  ( y = e -> ( y e. B <-> e e. B ) )
7 oveq1 
 |-  ( y = e -> ( y ( +g ` G ) x ) = ( e ( +g ` G ) x ) )
8 7 eqeq1d 
 |-  ( y = e -> ( ( y ( +g ` G ) x ) = x <-> ( e ( +g ` G ) x ) = x ) )
9 8 ovanraleqv 
 |-  ( y = e -> ( A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) <-> A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
10 6 9 anbi12d 
 |-  ( y = e -> ( ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) <-> ( e e. B /\ A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) ) )
11 10 iotan0 
 |-  ( ( e e. B /\ e =/= (/) /\ e = ( iota y ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) ) ) -> ( e e. B /\ A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
12 rsp 
 |-  ( A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) -> ( x e. B -> ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
13 11 12 simpl2im 
 |-  ( ( e e. B /\ e =/= (/) /\ e = ( iota y ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) ) ) -> ( x e. B -> ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
14 13 3expb 
 |-  ( ( e e. B /\ ( e =/= (/) /\ e = ( iota y ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) ) ) ) -> ( x e. B -> ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
15 14 expcom 
 |-  ( ( e =/= (/) /\ e = ( iota y ( y e. B /\ A. x e. B ( ( y ( +g ` G ) x ) = x /\ ( x ( +g ` G ) y ) = x ) ) ) ) -> ( e e. B -> ( x e. B -> ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) ) )
16 5 15 sylan2b 
 |-  ( ( e =/= (/) /\ e = .0. ) -> ( e e. B -> ( x e. B -> ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) ) )
17 16 impcom 
 |-  ( ( e e. B /\ ( e =/= (/) /\ e = .0. ) ) -> ( x e. B -> ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
18 17 ralrimiv 
 |-  ( ( e e. B /\ ( e =/= (/) /\ e = .0. ) ) -> A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) )
19 18 ex 
 |-  ( e e. B -> ( ( e =/= (/) /\ e = .0. ) -> A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
20 19 reximia 
 |-  ( E. e e. B ( e =/= (/) /\ e = .0. ) -> E. e e. B A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) )
21 20 anim2i 
 |-  ( ( G e. Smgrp /\ E. e e. B ( e =/= (/) /\ e = .0. ) ) -> ( G e. Smgrp /\ E. e e. B A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
22 1 3 ismnddef 
 |-  ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. x e. B ( ( e ( +g ` G ) x ) = x /\ ( x ( +g ` G ) e ) = x ) ) )
23 21 22 sylibr 
 |-  ( ( G e. Smgrp /\ E. e e. B ( e =/= (/) /\ e = .0. ) ) -> G e. Mnd )