Theorem issgrp

Description: The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

	Ref	Expression
Hypotheses	issgrp.b	$$⊢B={\mathrm{Base}}_M$$
	issgrp.o	No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion	issgrp	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		issgrp.b	$$⊢B={\mathrm{Base}}_M$$
2		issgrp.o	Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3		fvexd	$$⊢g=M\to {\mathrm{Base}}_g\in \mathrm{V}$$
4		fveq2	$$⊢g=M\to {\mathrm{Base}}_g={\mathrm{Base}}_M$$
5	4 1	eqtr4di	$$⊢g=M\to {\mathrm{Base}}_g=B$$
6		fvexd	$$⊢\left(g=M\wedge b=B\right)\to {+}_g\in \mathrm{V}$$
7		fveq2	$$⊢g=M\to {+}_g={+}_M$$
8	7	adantr	$$⊢\left(g=M\wedge b=B\right)\to {+}_g={+}_M$$
9	8 2	eqtr4di	Could not format ( ( g = M /\ b = B ) -> ( +g ` g ) = .o. ) : No typesetting found for |- ( ( g = M /\ b = B ) -> ( +g ` g ) = .o. ) with typecode |-
10		simplr	Could not format ( ( ( g = M /\ b = B ) /\ o = .o. ) -> b = B ) : No typesetting found for |- ( ( ( g = M /\ b = B ) /\ o = .o. ) -> b = B ) with typecode |-
11		id	Could not format ( o = .o. -> o = .o. ) : No typesetting found for |- ( o = .o. -> o = .o. ) with typecode |-
12		oveq	Could not format ( o = .o. -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( o = .o. -> ( x o y ) = ( x .o. y ) ) with typecode |-
13		eqidd	Could not format ( o = .o. -> z = z ) : No typesetting found for |- ( o = .o. -> z = z ) with typecode |-
14	11 12 13	oveq123d	Could not format ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) ) : No typesetting found for |- ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) ) with typecode |-
15		eqidd	Could not format ( o = .o. -> x = x ) : No typesetting found for |- ( o = .o. -> x = x ) with typecode |-
16		oveq	Could not format ( o = .o. -> ( y o z ) = ( y .o. z ) ) : No typesetting found for |- ( o = .o. -> ( y o z ) = ( y .o. z ) ) with typecode |-
17	11 15 16	oveq123d	Could not format ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) ) with typecode |-
18	14 17	eqeq12d	Could not format ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( o = .o. -> ( ( ( 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 ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
20	10 19	raleqbidv	Could not format ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. 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 |- ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. 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 |-
21	10 20	raleqbidv	Could not format ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
22	10 21	raleqbidv	Could not format ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. 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 |- ( ( ( g = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. 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 |-
23	6 9 22	sbcied2	Could not format ( ( g = M /\ b = B ) -> ( [. ( +g ` g ) / o ]. A. x e. b A. 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 |- ( ( g = M /\ b = B ) -> ( [. ( +g ` g ) / o ]. A. x e. b A. 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 |-
24	3 5 23	sbcied2	Could not format ( g = M -> ( [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. 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 |- ( g = M -> ( [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. 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 |-
25		df-sgrp	$$⊢\mathrm{Smgrp}=\left\{g\in \mathrm{Mgm}|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)\right\}$$
26	24 25	elrab2	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 |-