Description: Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | srgacl.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
srgacl.p | ⊢ + = ( +g ‘ 𝑅 ) | ||
Assertion | srgcom | ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srgacl.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
2 | srgacl.p | ⊢ + = ( +g ‘ 𝑅 ) | |
3 | srgcmn | ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd ) | |
4 | 1 2 | cmncom | ⊢ ( ( 𝑅 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) |
5 | 3 4 | syl3an1 | ⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ) |