Theorem ismgmALT

Description: The predicate "is a magma". (Contributed by AV, 16-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	ismgmALT.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	ismgmALT.o	⊢ ⚬ = ( +g ‘ 𝑀 )
Assertion	ismgmALT	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ MgmALT ↔ ⚬ clLaw 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ismgmALT.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		ismgmALT.o	⊢ ⚬ = ( +g ‘ 𝑀 )
3		fveq2	⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
4	3 2	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ⚬ )
5		fveq2	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
6	5 1	eqtr4di	⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
7	4 6	breq12d	⊢ ( 𝑚 = 𝑀 → ( ( +g ‘ 𝑚 ) clLaw ( Base ‘ 𝑚 ) ↔ ⚬ clLaw 𝐵 ) )
8		df-mgm2	⊢ MgmALT = { 𝑚 ∣ ( +g ‘ 𝑚 ) clLaw ( Base ‘ 𝑚 ) }
9	7 8	elab2g	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ MgmALT ↔ ⚬ clLaw 𝐵 ) )