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