sgrpass

Description: A semigroup operation is associative. (Contributed by FL, 2-Nov-2009) (Revised by AV, 30-Jan-2020)

	Ref	Expression
Hypotheses	sgrpass.b	$⊢ B = {Base}_{G}$
	sgrpass.o	No typesetting found for \|- .o. = ( +g ` G ) with typecode \|-
Assertion	sgrpass	Could not format assertion : No typesetting found for \|- ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		sgrpass.b	$⊢ B = {Base}_{G}$
2		sgrpass.o	Could not format .o. = ( +g ` G ) : No typesetting found for \|- .o. = ( +g ` G ) with typecode \|-
3	1 2	issgrp	Could not format ( G e. Smgrp <-> ( G 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 \|- ( G e. Smgrp <-> ( G 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 \|-
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		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 \|-
9	8	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 \|-
10		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 \|-
11	10	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 \|-
12	9 11	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 \|-
13		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 \|-
14		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 \|-
15	14	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 \|-
16	13 15	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 \|-
17	7 12 16	rspc3v	Could not format ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( A. x e. B A. y e. B A. 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 ) -> ( A. x e. B A. y e. B A. 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 \|-
18	17	com12	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 ) ) -> ( ( X e. B /\ Y e. B /\ 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 ) ) -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode \|-
19	3 18	simplbiim	Could not format ( G e. Smgrp -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for \|- ( G e. Smgrp -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode \|-
20	19	imp	Could not format ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for \|- ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem sgrpass

Proof