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