Proposition. 負負得正 [ring-0003]

module ring-0003 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}
open import ring-0002

負負得正通常可能在說兩件事。第一，− − a = a，因為 −a 的反元素是 a 也可以是 − − a，因此 − − a 一定等於 a（因為 Ring 的加法部分是一個 commutative group）。

neg-neg-lemma : {R : 𝓤 ̇ } {{_ : Ring R}} (x : R) → - - x ＝ x
neg-neg-lemma x = ring-cancel-right (I ∙ II ⁻¹)
  where
  I : - - x ⊕ - x ＝ 𝟘R
  I = cancel .pr₁
  II : x ⊕ - x ＝ 𝟘R
  II = cancel .pr₂

或是更重要的 −a × −b = a × b，也就是這裡要證明的命題

neg-lemma-left : {R : 𝓤 ̇ } {{_ : Ring R}} (a b : R) → - a ⊗ b ＝ - (a ⊗ b)
neg-lemma-left a b = ring-cancel-right (II ∙ I ⁻¹)
  where
  I : (- (a ⊗ b)) ⊕ a ⊗ b ＝ 𝟘R
  I = (- (a ⊗ b)) ⊕ a ⊗ b ＝⟨ cancel .pr₁ ⟩
      𝟘R ∎
  II : (- a ⊗ b) ⊕ a ⊗ b ＝ 𝟘R
  II = (- a ⊗ b) ⊕ a ⊗ b ＝⟨ distrib1 ⁻¹ ⟩
      (- a ⊕ a) ⊗ b      ＝⟨ ap (_⊗ b) (cancel .pr₁) ⟩
      𝟘R ⊗ b             ＝⟨ lemma-1 b .pr₂ ⟩
      𝟘R ∎
neg-lemma-right : {R : 𝓤 ̇ } {{_ : Ring R}} (a b : R) → a ⊗ - b ＝ - (a ⊗ b)
neg-lemma-right a b = ring-cancel-right (II ∙ I ⁻¹)
  where
  I : (- (a ⊗ b)) ⊕ a ⊗ b ＝ 𝟘R
  I = cancel .pr₁
  II : (a ⊗ - b) ⊕ a ⊗ b ＝ 𝟘R
  II = (a ⊗ - b) ⊕ a ⊗ b ＝⟨ distrib2 ⁻¹ ⟩
      a ⊗ (- b ⊕ b)      ＝⟨ ap (a ⊗_) (cancel .pr₁) ⟩
      a ⊗ 𝟘R             ＝⟨ lemma-1 a .pr₁ ⟩
      𝟘R ∎

proposition-2 : {R : 𝓤 ̇ } {{_ : Ring R}} → (a b : R) → - a ⊗ - b ＝ a ⊗ b
proposition-2 {_}{R} a b =
  (- a ⊗ - b) ＝⟨ neg-lemma-left a (- b) ⟩
  - (a ⊗ - b) ＝⟨ ap -_ (neg-lemma-right a b) ⟩
  - - (a ⊗ b) ＝⟨ neg-neg-lemma (a ⊗ b) ⟩
  a ⊗ b ∎