---

Step * 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)))
⊢ ∀[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
{ (Auto THEN SplitOrHyps 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)))
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)

2
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)

---

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))
\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:
(Auto  THEN  SplitOrHyps  THEN  Auto)

---

Home Index