Metamath Proof Explorer


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 𝐵 ) )