---

Step * of Lemma inverse-unique

∀[r:CRng]. ∀[n:ℕ]. ∀[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
{ (RepeatFor 2 (Intro)
   THEN (Assert ∀[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))) BY
               (Auto
                THEN (Assert invertible-matrix(r;n;A) BY
                            (D 0 With ⌜C⌝  THEN Auto))
                THEN (FLemma `invertible-matrix-iff-left` [-1] THEN Auto)
                THEN ExRepD
                THEN ((Assert (A*B) = (A*C) ∈ Matrix(n;n;r) BY
                             Auto)
                      THEN (Assert (B1*(A*B)) = (B1*(A*C)) ∈ Matrix(n;n;r) BY
                                  Auto)
                      )
                THEN RWW  "matrix-times-assoc< -3 matrix-times-id-left" (-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)))
⊢ ∀[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:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \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:
(RepeatFor  2  (Intro)
  THEN  (Assert  \mforall{}[A,B,C:Matrix(n;n;r)].    (((A*B)  =  I)  {}\mRightarrow{}  ((A*C)  =  I)  {}\mRightarrow{}  (B  =  C))  BY
                          (Auto
                            THEN  (Assert  invertible-matrix(r;n;A)  BY
                                                    (D  0  With  \mkleeneopen{}C\mkleeneclose{}    THEN  Auto))
                            THEN  (FLemma  `invertible-matrix-iff-left`  [-1]  THEN  Auto)
                            THEN  ExRepD
                            THEN  ((Assert  (A*B)  =  (A*C)  BY  Auto)  THEN  (Assert  (B1*(A*B))  =  (B1*(A*C))  BY  Auto))
                            THEN  RWW    "matrix-times-assoc<  -3  matrix-times-id-left"  (-1)
                            THEN  Auto))
  )

---

Home Index