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

Metamath Proof Explorer

Theorem isnmnd

Description: A condition for a structure not to be a monoid: every element of the base set is not a left identity for at least one element of the base set. (Contributed by AV, 4-Feb-2020)

Ref Expression
Hypotheses isnmnd.b 
|- B = ( Base ` M )
isnmnd.o 
|- .o. = ( +g ` M )
Assertion isnmnd 
|- ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd )

Proof

Step Hyp Ref Expression
1 isnmnd.b 
 |-  B = ( Base ` M )
2 isnmnd.o 
 |-  .o. = ( +g ` M )
3 neneq 
 |-  ( ( z .o. x ) =/= x -> -. ( z .o. x ) = x )
4 3 intnanrd 
 |-  ( ( z .o. x ) =/= x -> -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
5 4 reximi 
 |-  ( E. x e. B ( z .o. x ) =/= x -> E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
6 5 ralimi 
 |-  ( A. z e. B E. x e. B ( z .o. x ) =/= x -> A. z e. B E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
7 rexnal 
 |-  ( E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
8 7 ralbii 
 |-  ( A. z e. B E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> A. z e. B -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
9 ralnex 
 |-  ( A. z e. B -. A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
10 8 9 bitri 
 |-  ( A. z e. B E. x e. B -. ( ( z .o. x ) = x /\ ( x .o. z ) = x ) <-> -. E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
11 6 10 sylib 
 |-  ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) )
12 11 intnand 
 |-  ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. ( M e. Smgrp /\ E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) )
13 1 2 ismnddef 
 |-  ( M e. Mnd <-> ( M e. Smgrp /\ E. z e. B A. x e. B ( ( z .o. x ) = x /\ ( x .o. z ) = x ) ) )
14 12 13 sylnibr 
 |-  ( A. z e. B E. x e. B ( z .o. x ) =/= x -> -. M e. Mnd )
15 df-nel 
 |-  ( M e/ Mnd <-> -. M e. Mnd )
16 14 15 sylibr 
 |-  ( A. z e. B E. x e. B ( z .o. x ) =/= x -> M e/ Mnd )