Theorem iscomlaw

Description: The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	iscomlaw	⊢ ( ( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( ⚬ comLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) = ( 𝑦 ⚬ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
2		oveq	⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
3		oveq	⊢ ( 𝑜 = ⚬ → ( 𝑦 𝑜 𝑥 ) = ( 𝑦 ⚬ 𝑥 ) )
4	2 3	eqeq12d	⊢ ( 𝑜 = ⚬ → ( ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) ↔ ( 𝑥 ⚬ 𝑦 ) = ( 𝑦 ⚬ 𝑥 ) ) )
5	4	adantr	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) ↔ ( 𝑥 ⚬ 𝑦 ) = ( 𝑦 ⚬ 𝑥 ) ) )
6	1 5	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) = ( 𝑦 ⚬ 𝑥 ) ) )
7	1 6	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) = ( 𝑦 ⚬ 𝑥 ) ) )
8		df-comlaw	⊢ comLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) = ( 𝑦 𝑜 𝑥 ) }
9	7 8	brabga	⊢ ( ( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( ⚬ comLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) = ( 𝑦 ⚬ 𝑥 ) ) )