Ring Theory

Equational axioms for Ring theory.

We would base this on Group theory, but the constructor used in that definition is mul, whereas here we need the "addition" part of the ring to be the group, so that naming would be confusing. So let's just do it all from scratch here, for better or worse.

The additive operator forms an Abelian group:

axiom (#add-id-right)   add(A, zero) = A
axiom (#add-id-left)    add(zero, A) = A
axiom (#add-assoc)      add(A, add(B, C)) = add(add(A, B), C)
axiom (#add-comm)       add(A, B) = add(B, A)
axiom (#add-neg-right)  add(A, neg(A)) = zero
axiom (#add-neg-left)   add(neg(A), A) = zero

The multiplicative operator forms a monoid:

axiom (#mul-id-right)   mul(A, one) = A
axiom (#mul-id-left)    mul(one, A) = A
axiom (#mul-assoc)      mul(A, mul(B, C)) = mul(mul(A, B), C)

Multiplication distributes over addition.

axiom (#mul-distr-add-right)  mul(add(A, B), C) = add(mul(A, C), mul(B, C))
axiom (#mul-distr-add-left)   mul(A, add(B, C)) = add(mul(A, B), mul(A, C))

Now, some simple theorems in ring theory.

Additive Identity is Absorbing Element for Multiplication

theorem (#zero-absorb-right)
    mul(A, zero) = zero
proof
    mul(A, zero) = mul(A, zero)
    mul(A, zero) = mul(A, add(zero, zero))
    mul(A, zero) = add(mul(A, zero), mul(A, zero))
    add(mul(A, zero), neg(mul(A, zero))) = add(add(mul(A, zero), mul(A, zero)), neg(mul(A, zero)))
        [by congruence of C and add(C, neg(mul(A, zero)))]
    zero = add(add(mul(A, zero), mul(A, zero)), neg(mul(A, zero)))
    zero = add(mul(A, zero), add(mul(A, zero), neg(mul(A, zero))))
    zero = add(mul(A, zero), zero)
    zero = mul(A, zero)
    mul(A, zero) = zero  [by symmetry]
qed

theorem (#zero-absorb-left)
    mul(zero, A) = zero
proof
    mul(zero, A) = mul(zero, A)
    mul(zero, A) = mul(add(zero, zero), A)
    mul(zero, A) = add(mul(zero, A), mul(zero, A))
    add(mul(zero, A), neg(mul(zero, A))) = add(add(mul(zero, A), mul(zero, A)), neg(mul(zero, A)))
        [by congruence of C and add(C, neg(mul(zero, A)))]
    zero = add(add(mul(zero, A), mul(zero, A)), neg(mul(zero, A)))
    zero = add(mul(zero, A), add(mul(zero, A), neg(mul(zero, A))))
    zero = add(mul(zero, A), zero)
    zero = mul(zero, A)
    mul(zero, A) = zero  [by symmetry]
qed

Negative of Ring Negative

Also see Negative of Ring Negative on ProofWiki.

theorem
    neg(neg(A)) = A
proof
    zero = zero
    zero = add(neg(A), A)
    add(neg(neg(A)), zero) = add(neg(neg(A)), add(neg(A), A))   [by congruence of X and add(neg(neg(A)), X)]
    neg(neg(A)) = add(neg(neg(A)), add(neg(A), A))
    neg(neg(A)) = add(add(neg(neg(A)), neg(A)), A)
    neg(neg(A)) = add(zero, A)
    neg(neg(A)) = A
qed

Product with Ring Negative

See also Product with Ring Negative on ProofWiki. First we state it as a zero-sum, then refactor it into an equality by "adding -(A * B) to both sides".

We need both right and left product versions of this theorem.

theorem (#prog-neg-zero-right)
    add(mul(A, B), mul(A, neg(B))) = zero
proof
    add(mul(A, B), mul(A, neg(B))) = add(mul(A, B), mul(A, neg(B)))
    add(mul(A, B), mul(A, neg(B))) = mul(A, add(B, neg(B)))
    add(mul(A, B), mul(A, neg(B))) = mul(A, zero)
    add(mul(A, B), mul(A, neg(B))) = zero
qed

theorem (#prog-neg-right)
    neg(mul(A, B)) = mul(A, neg(B))
proof
    add(mul(A, B), mul(A, neg(B))) = add(mul(A, B), mul(A, neg(B)))
    add(mul(A, B), mul(A, neg(B))) = zero
    add(neg(mul(A, B)), add(mul(A, B), mul(A, neg(B)))) = add(neg(mul(A, B)), zero)
        [by congruence of C and add(neg(mul(A, B)), C)]
    add(neg(mul(A, B)), add(mul(A, B), mul(A, neg(B)))) = neg(mul(A, B))
    add(add(neg(mul(A, B)), mul(A, B)), mul(A, neg(B))) = neg(mul(A, B))
    add(zero, mul(A, neg(B))) = neg(mul(A, B))
    mul(A, neg(B)) = neg(mul(A, B))
    neg(mul(A, B)) = mul(A, neg(B))  [by symmetry]
qed

theorem (#prog-neg-zero-left)
    add(mul(A, B), mul(neg(A), B)) = zero
proof
    add(mul(A, B), mul(neg(A), B)) = add(mul(A, B), mul(neg(A), B))
    add(mul(A, B), mul(neg(A), B)) = mul(add(A, neg(A)), B)
    add(mul(A, B), mul(neg(A), B)) = mul(zero, B)
    add(mul(A, B), mul(neg(A), B)) = zero
qed

theorem (#prog-neg-left)
    neg(mul(A, B)) = mul(neg(A), B)
proof
    add(mul(A, B), mul(neg(A), B)) = add(mul(A, B), mul(neg(A), B))
    add(mul(A, B), mul(neg(A), B)) = zero
    add(neg(mul(A, B)), add(mul(A, B), mul(neg(A), B))) = add(neg(mul(A, B)), zero)
        [by congruence of C and add(neg(mul(A, B)), C)]
    add(neg(mul(A, B)), add(mul(A, B), mul(neg(A), B))) = neg(mul(A, B))
    add(add(neg(mul(A, B)), mul(A, B)), mul(neg(A), B)) = neg(mul(A, B))
    add(zero, mul(neg(A), B)) = neg(mul(A, B))
    mul(neg(A), B) = neg(mul(A, B))
    neg(mul(A, B)) = mul(neg(A), B)  [by symmetry]
qed

Product of Ring Negatives

See also Product of Ring Negatives on ProofWiki. With the above lemmas in place, this is very straightforward.

theorem
    mul(neg(A), neg(B)) = mul(A, B)
proof
    mul(neg(A), neg(B)) = mul(neg(A), neg(B))
    mul(neg(A), neg(B)) = neg(mul(A, neg(B)))
    mul(neg(A), neg(B)) = neg(neg(mul(A, B)))
    mul(neg(A), neg(B)) = mul(A, B)
qed