Proposition. Not zero divisor if and only if left action is injective [ring-0005]

$a \in R$ 不是 zero divisor 若且唯若其 left action $x \mapsto a x$ 是 injective（也就是 left-cancellable）

module ring-0005 where

open import MLTT.Spartan

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

left-action : {R : 𝓤 ̇ } {{_ : Ring R}} (a : R) → R → R
left-action a x = a ⊗ x

proposition-3 : {R : 𝓤 ̇ } {{_ : Ring R}} {a : R} →
  (NonZeroDivisor a → left-cancellable (left-action a)) × (left-cancellable (left-action a) → NonZeroDivisor a)
proposition-3 {_}{R}{a} = if , only-if
  where
  if : NonZeroDivisor a → left-cancellable (left-action a)
  if is-not-zd {x}{y} Ax=Ay = ring-cancel-right (II ∙ III ⁻¹)
    where
    I : left-action a (x ⊕ - y) ＝ 𝟘R
    I =
      left-action a (x ⊕ - y) ＝⟨by-definition⟩
      a ⊗ (x ⊕ - y)           ＝⟨ distrib2 ⟩
      a ⊗ x ⊕ a ⊗ - y         ＝⟨ ap (a ⊗ x ⊕_) (neg-lemma-right a y) ⟩
      a ⊗ x ⊕ - (a ⊗ y)       ＝⟨ ap (_⊕ - (a ⊗ y)) Ax=Ay ⟩
      a ⊗ y ⊕ - (a ⊗ y)       ＝⟨ cancel .pr₂ ⟩
      𝟘R ∎
    II : x ⊕ - y ＝ 𝟘R
    II = is-not-zd (x ⊕ - y) I
    III : y ⊕ - y ＝ 𝟘R
    III = cancel .pr₂
  only-if : left-cancellable (left-action a) → NonZeroDivisor a
  only-if inj b ab=0 = inj I
    where
    I : a ⊗ b ＝ a ⊗ 𝟘R
    I = left-action a b ＝⟨by-definition⟩
        a ⊗ b           ＝⟨ ab=0 ⟩
        𝟘R              ＝⟨ lemma-1 a .pr₁ ⁻¹ ⟩
        a ⊗ 𝟘R          ＝⟨by-definition⟩
        left-action a 𝟘R ∎