Metamath Proof Explorer


Theorem isasslaw

Description: The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009) (Revised by AV, 13-Jan-2020)

Ref Expression
Assertion isasslaw
|- ( ( .o. e. V /\ M e. W ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( o = .o. /\ m = M ) -> m = M )
2 id
 |-  ( o = .o. -> o = .o. )
3 oveq
 |-  ( o = .o. -> ( x o y ) = ( x .o. y ) )
4 eqidd
 |-  ( o = .o. -> z = z )
5 2 3 4 oveq123d
 |-  ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) )
6 eqidd
 |-  ( o = .o. -> x = x )
7 oveq
 |-  ( o = .o. -> ( y o z ) = ( y .o. z ) )
8 2 6 7 oveq123d
 |-  ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) )
9 5 8 eqeq12d
 |-  ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
10 9 adantr
 |-  ( ( o = .o. /\ m = M ) -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
11 1 10 raleqbidv
 |-  ( ( o = .o. /\ m = M ) -> ( A. z e. m ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
12 1 11 raleqbidv
 |-  ( ( o = .o. /\ m = M ) -> ( A. y e. m A. z e. m ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
13 1 12 raleqbidv
 |-  ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m A. z e. m ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )
14 df-asslaw
 |-  assLaw = { <. o , m >. | A. x e. m A. y e. m A. z e. m ( ( x o y ) o z ) = ( x o ( y o z ) ) }
15 13 14 brabga
 |-  ( ( .o. e. V /\ M e. W ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) )