This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )