---

Step * 1 1 2 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. (A*B) = I ∈ Matrix(n;n;r)
9. (C*A) = I ∈ Matrix(n;n;r)
⊢ B = C ∈ Matrix(n;n;r)
BY
{ ((Assert (C*(A*B)) = C ∈ Matrix(n;n;r) BY
          (RWO "-2" 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.  (A*B)  =  I
9.  (C*A)  =  I
\mvdash{}  B  =  C


By

---

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

---

Home Index