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	Could not format assertion : No typesetting found for |- ( ( .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 ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpr	Could not format ( ( o = .o. /\ m = M ) -> m = M ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> m = M ) with typecode |-
2		id	Could not format ( o = .o. -> o = .o. ) : No typesetting found for |- ( o = .o. -> o = .o. ) with typecode |-
3		oveq	Could not format ( o = .o. -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( o = .o. -> ( x o y ) = ( x .o. y ) ) with typecode |-
4		eqidd	Could not format ( o = .o. -> z = z ) : No typesetting found for |- ( o = .o. -> z = z ) with typecode |-
5	2 3 4	oveq123d	Could not format ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) ) : No typesetting found for |- ( o = .o. -> ( ( x o y ) o z ) = ( ( x .o. y ) .o. z ) ) with typecode |-
6		eqidd	Could not format ( o = .o. -> x = x ) : No typesetting found for |- ( o = .o. -> x = x ) with typecode |-
7		oveq	Could not format ( o = .o. -> ( y o z ) = ( y .o. z ) ) : No typesetting found for |- ( o = .o. -> ( y o z ) = ( y .o. z ) ) with typecode |-
8	2 6 7	oveq123d	Could not format ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( o = .o. -> ( x o ( y o z ) ) = ( x .o. ( y .o. z ) ) ) with typecode |-
9	5 8	eqeq12d	Could not format ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( o = .o. -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
10	9	adantr	Could not format ( ( o = .o. /\ m = M ) -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( ( ( x o y ) o z ) = ( x o ( y o z ) ) <-> ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
11	1 10	raleqbidv	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
12	1 11	raleqbidv	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
13	1 12	raleqbidv	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
14		df-asslaw	$$⊢\mathrm{assLaw}=\left\{⟨o,m⟩|\forall x\in m\forall y\in m\forall z\in m\left(xoy\right)oz=xo\left(yoz\right)\right\}$$
15	13 14	brabga	Could not format ( ( .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 ) ) ) ) : No typesetting found for |- ( ( .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 ) ) ) ) with typecode |-