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 = {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 = {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 {Base}_{g} \in V$
4		fveq2	$⊢ g = M \to {Base}_{g} = {Base}_{M}$
5	4 1	eqtr4di	$⊢ g = M \to {Base}_{g} = B$
6		fvexd	$⊢ (g = M \land b = B) \to +_{g} \in V$
7		fveq2	$⊢ g = M \to +_{g} = +_{M}$
8	7	adantr	$⊢ (g = M \land b = B) \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	$⊢ Smgrp = \{g \in Mgm \| \underset{˙}{[} {Base}_{g} / b \underset{˙}{]} \underset{˙}{[} +_{g} / o \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x o y) o z = x o (y o z)\}$
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 \|-

Metamath Proof Explorer

Theorem issgrp

Proof