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	⊢ ( ( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
2		id	⊢ ( 𝑜 = ⚬ → 𝑜 = ⚬ )
3		oveq	⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
4		eqidd	⊢ ( 𝑜 = ⚬ → 𝑧 = 𝑧 )
5	2 3 4	oveq123d	⊢ ( 𝑜 = ⚬ → ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) )
6		eqidd	⊢ ( 𝑜 = ⚬ → 𝑥 = 𝑥 )
7		oveq	⊢ ( 𝑜 = ⚬ → ( 𝑦 𝑜 𝑧 ) = ( 𝑦 ⚬ 𝑧 ) )
8	2 6 7	oveq123d	⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
9	5 8	eqeq12d	⊢ ( 𝑜 = ⚬ → ( ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
10	9	adantr	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
11	1 10	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑧 ∈ 𝑚 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
12	1 11	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑦 ∈ 𝑚 ∀ 𝑧 ∈ 𝑚 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
13	1 12	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ∀ 𝑧 ∈ 𝑚 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
14		df-asslaw	⊢ assLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ∀ 𝑧 ∈ 𝑚 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }
15	13 14	brabga	⊢ ( ( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )