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 No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion isnsgrp Could not format assertion : No typesetting found for |- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) ) with typecode |-

Proof

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