Description: Acommutative magma is a magma with a commutative operation. Definition 8 of BourbakiAlg1 p. 7. (Contributed by AV, 20-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-cmgm2 | ⊢ CMgmALT = { 𝑚 ∈ MgmALT ∣ ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ccmgm2 | ⊢ CMgmALT | |
1 | vm | ⊢ 𝑚 | |
2 | cmgm2 | ⊢ MgmALT | |
3 | cplusg | ⊢ +g | |
4 | 1 | cv | ⊢ 𝑚 |
5 | 4 3 | cfv | ⊢ ( +g ‘ 𝑚 ) |
6 | ccomlaw | ⊢ comLaw | |
7 | cbs | ⊢ Base | |
8 | 4 7 | cfv | ⊢ ( Base ‘ 𝑚 ) |
9 | 5 8 6 | wbr | ⊢ ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) |
10 | 9 1 2 | crab | ⊢ { 𝑚 ∈ MgmALT ∣ ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) } |
11 | 0 10 | wceq | ⊢ CMgmALT = { 𝑚 ∈ MgmALT ∣ ( +g ‘ 𝑚 ) comLaw ( Base ‘ 𝑚 ) } |