---

Step * 1 of Lemma inverse-unique


1. [r] : CRng
2. [n] : ℕ
3. ∀[A,B,C:Matrix(n;n;r)].  (((A*B) = I ∈ Matrix(n;n;r)) ⇒ ((A*C) = I ∈ Matrix(n;n;r)) ⇒ (B = C ∈ Matrix(n;n;r)))
⊢ ∀[A,B,C:Matrix(n;n;r)].
    ((((A*B) = I ∈ Matrix(n;n;r)) ∨ ((B*A) = I ∈ Matrix(n;n;r)))
    ⇒ (((A*C) = I ∈ Matrix(n;n;r)) ∨ ((C*A) = I ∈ Matrix(n;n;r)))
    ⇒ (B = C ∈ Matrix(n;n;r)))
BY
{ (Assert ∀[A,B,C:Matrix(n;n;r)].
            (((B*A) = I ∈ Matrix(n;n;r)) ⇒ ((C*A) = I ∈ Matrix(n;n;r)) ⇒ (B = C ∈ Matrix(n;n;r))) BY
         (Auto
          THEN (Assert invertible-matrix(r;n;A) BY
                      (BLemma `invertible-matrix-iff-left`  THEN Auto))
          THEN D -1
          THEN ((Assert (B*A) = (C*A) ∈ Matrix(n;n;r) BY
                       Auto)
                THEN (Assert ((B*A)*B1) = ((C*A)*B1) ∈ Matrix(n;n;r) BY
                            Auto)
                )
          THEN RWW  "matrix-times-assoc -3 matrix-times-id-right" (-1)
          THEN Auto)) }

1
1. [r] : CRng
2. [n] : ℕ
3. ∀[A,B,C:Matrix(n;n;r)].  (((A*B) = I ∈ Matrix(n;n;r)) ⇒ ((A*C) = I ∈ Matrix(n;n;r)) ⇒ (B = C ∈ Matrix(n;n;r)))
4. ∀[A,B,C:Matrix(n;n;r)].  (((B*A) = I ∈ Matrix(n;n;r)) ⇒ ((C*A) = I ∈ Matrix(n;n;r)) ⇒ (B = C ∈ Matrix(n;n;r)))
⊢ ∀[A,B,C:Matrix(n;n;r)].
    ((((A*B) = I ∈ Matrix(n;n;r)) ∨ ((B*A) = I ∈ Matrix(n;n;r)))
    ⇒ (((A*C) = I ∈ Matrix(n;n;r)) ∨ ((C*A) = I ∈ Matrix(n;n;r)))
    ⇒ (B = C ∈ Matrix(n;n;r)))

---

Latex:

---

Latex:

1.  [r]  :  CRng
2.  [n]  :  \mBbbN{}
3.  \mforall{}[A,B,C:Matrix(n;n;r)].    (((A*B)  =  I)  {}\mRightarrow{}  ((A*C)  =  I)  {}\mRightarrow{}  (B  =  C))
\mvdash{}  \mforall{}[A,B,C:Matrix(n;n;r)].    ((((A*B)  =  I)  \mvee{}  ((B*A)  =  I))  {}\mRightarrow{}  (((A*C)  =  I)  \mvee{}  ((C*A)  =  I))  {}\mRightarrow{}  (B  =  C))


By

---

Latex:
(Assert  \mforall{}[A,B,C:Matrix(n;n;r)].    (((B*A)  =  I)  {}\mRightarrow{}  ((C*A)  =  I)  {}\mRightarrow{}  (B  =  C))  BY
              (Auto
                THEN  (Assert  invertible-matrix(r;n;A)  BY
                                        (BLemma  `invertible-matrix-iff-left`    THEN  Auto))
                THEN  D  -1
                THEN  ((Assert  (B*A)  =  (C*A)  BY  Auto)  THEN  (Assert  ((B*A)*B1)  =  ((C*A)*B1)  BY  Auto))
                THEN  RWW    "matrix-times-assoc  -3  matrix-times-id-right"  (-1)
                THEN  Auto))

---

Home Index