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