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

Metamath Proof Explorer

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 ) )