Theorem isnsgrp

Description: A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020)

	Ref	Expression
Hypotheses	issgrpn0.b	|- B = ( Base ` M )
	issgrpn0.o	|- .o. = ( +g ` M )
Assertion	isnsgrp	|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) )

Proof

Step	Hyp	Ref	Expression
1		issgrpn0.b	|- B = ( Base ` M )
2		issgrpn0.o	|- .o. = ( +g ` M )
3		simpl1	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> X e. B )
4		oveq1	|- ( x = X -> ( x .o. y ) = ( X .o. y ) )
5	4	oveq1d	|- ( x = X -> ( ( x .o. y ) .o. z ) = ( ( X .o. y ) .o. z ) )
6		oveq1	|- ( x = X -> ( x .o. ( y .o. z ) ) = ( X .o. ( y .o. z ) ) )
7	5 6	eqeq12d	|- ( x = X -> ( ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) )
8	7	notbid	|- ( x = X -> ( -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) )
9	8	rexbidv	|- ( x = X -> ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) )
10	9	rexbidv	|- ( x = X -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) )
11	10	adantl	|- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ x = X ) -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) )
12		simpl2	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Y e. B )
13		oveq2	|- ( y = Y -> ( X .o. y ) = ( X .o. Y ) )
14	13	oveq1d	|- ( y = Y -> ( ( X .o. y ) .o. z ) = ( ( X .o. Y ) .o. z ) )
15		oveq1	|- ( y = Y -> ( y .o. z ) = ( Y .o. z ) )
16	15	oveq2d	|- ( y = Y -> ( X .o. ( y .o. z ) ) = ( X .o. ( Y .o. z ) ) )
17	14 16	eqeq12d	|- ( y = Y -> ( ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) )
18	17	notbid	|- ( y = Y -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) )
19	18	adantl	|- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) )
20	19	rexbidv	|- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) )
21		simpl3	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Z e. B )
22		oveq2	|- ( z = Z -> ( ( X .o. Y ) .o. z ) = ( ( X .o. Y ) .o. Z ) )
23		oveq2	|- ( z = Z -> ( Y .o. z ) = ( Y .o. Z ) )
24	23	oveq2d	|- ( z = Z -> ( X .o. ( Y .o. z ) ) = ( X .o. ( Y .o. Z ) ) )
25	22 24	eqeq12d	|- ( z = Z -> ( ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) )
26	25	notbid	|- ( z = Z -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) )
27	26	adantl	|- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ z = Z ) -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) )
28		neneq	|- ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )
29	28	adantl	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )
30	21 27 29	rspcedvd	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) )
31	12 20 30	rspcedvd	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) )
32	3 11 31	rspcedvd	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
33		rexnal	|- ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
34	33	2rexbii	|- ( E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
35		rexnal2	|- ( E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
36	34 35	bitr2i	|- ( -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
37	32 36	sylibr	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) )
38	37	intnand	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
39	1 2	issgrp	|- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
40	38 39	sylnibr	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. M e. Smgrp )
41		df-nel	|- ( M e/ Smgrp <-> -. M e. Smgrp )
42	40 41	sylibr	|- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> M e/ Smgrp )
43	42	ex	|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) )