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