---

Step * 1 1 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)))
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)))
5. A : Matrix(n;n;r)
6. B : Matrix(n;n;r)
7. C : Matrix(n;n;r)
8. (B*A) = I ∈ Matrix(n;n;r)
9. (A*C) = I ∈ Matrix(n;n;r)
⊢ B = C ∈ Matrix(n;n;r)
BY
{ (SwapVars `B' `C'
   THEN (Assert (C*(A*B)) = C ∈ Matrix(n;n;r) BY
               (RWO "-1" 0 THEN Auto))
   THEN (Assert (C*(A*B)) = B ∈ Matrix(n;n;r) BY
               (RWO "matrix-times-assoc<" 0 THEN Auto))
   THEN Auto) }

---

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))
4.  \mforall{}[A,B,C:Matrix(n;n;r)].    (((B*A)  =  I)  {}\mRightarrow{}  ((C*A)  =  I)  {}\mRightarrow{}  (B  =  C))
5.  A  :  Matrix(n;n;r)
6.  B  :  Matrix(n;n;r)
7.  C  :  Matrix(n;n;r)
8.  (B*A)  =  I
9.  (A*C)  =  I
\mvdash{}  B  =  C


By

---

Latex:
(SwapVars  `B'  `C'
  THEN  (Assert  (C*(A*B))  =  C  BY
                          (RWO  "-1"  0  THEN  Auto))
  THEN  (Assert  (C*(A*B))  =  B  BY
                          (RWO  "matrix-times-assoc<"  0  THEN  Auto))
  THEN  Auto)

---

Home Index