Description: The predicate "is a semigroup". (Contributed by AV, 16-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ismgmALT.b | ⊢ 𝐵 = ( Base ‘ 𝑀 ) | |
| ismgmALT.o | ⊢ ⚬ = ( +g ‘ 𝑀 ) | ||
| Assertion | issgrpALT | ⊢ ( 𝑀 ∈ SGrpALT ↔ ( 𝑀 ∈ MgmALT ∧ ⚬ assLaw 𝐵 ) ) |
| 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 ‘ 𝑚 ) assLaw ( Base ‘ 𝑚 ) ↔ ⚬ assLaw 𝐵 ) ) |
| 8 | df-sgrp2 | ⊢ SGrpALT = { 𝑚 ∈ MgmALT ∣ ( +g ‘ 𝑚 ) assLaw ( Base ‘ 𝑚 ) } | |
| 9 | 7 8 | elrab2 | ⊢ ( 𝑀 ∈ SGrpALT ↔ ( 𝑀 ∈ MgmALT ∧ ⚬ assLaw 𝐵 ) ) |