Theorem 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	|- .o. = ( +g ` G )
Assertion	sgrpass	|- ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		sgrpass.b	|- B = ( Base ` G )
2		sgrpass.o	|- .o. = ( +g ` G )
3	1 2	issgrp	|- ( 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 ) ) ) )
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		oveq2	|- ( y = Y -> ( X .o. y ) = ( X .o. Y ) )
9	8	oveq1d	|- ( y = Y -> ( ( X .o. y ) .o. z ) = ( ( X .o. Y ) .o. z ) )
10		oveq1	|- ( y = Y -> ( y .o. z ) = ( Y .o. z ) )
11	10	oveq2d	|- ( y = Y -> ( X .o. ( y .o. z ) ) = ( X .o. ( Y .o. z ) ) )
12	9 11	eqeq12d	|- ( y = Y -> ( ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) )
13		oveq2	|- ( z = Z -> ( ( X .o. Y ) .o. z ) = ( ( X .o. Y ) .o. Z ) )
14		oveq2	|- ( z = Z -> ( Y .o. z ) = ( Y .o. Z ) )
15	14	oveq2d	|- ( z = Z -> ( X .o. ( Y .o. z ) ) = ( X .o. ( Y .o. Z ) ) )
16	13 15	eqeq12d	|- ( z = Z -> ( ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) )
17	7 12 16	rspc3v	|- ( ( 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 ) ) ) )
18	17	com12	|- ( 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 ) ) ) )
19	3 18	simplbiim	|- ( G e. Smgrp -> ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) )
20	19	imp	|- ( ( G e. Smgrp /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) )