This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divcan8d

Description: A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses divcan8d.a ⊢ φ → A ∈ ℂ
divcan8d.b ⊢ φ → B ∈ ℂ
divcan8d.a0 ⊢ φ → A ≠ 0
divcan8d.b0 ⊢ φ → B ≠ 0
Assertion divcan8d ⊢ φ → B A ⁢ B = 1 A

Proof

Step Hyp Ref Expression
1 divcan8d.a ⊢ φ → A ∈ ℂ
2 divcan8d.b ⊢ φ → B ∈ ℂ
3 divcan8d.a0 ⊢ φ → A ≠ 0
4 divcan8d.b0 ⊢ φ → B ≠ 0
5 1 2 mulcld ⊢ φ → A ⁢ B ∈ ℂ
6 1 2 3 4 mulne0d ⊢ φ → A ⁢ B ≠ 0
7 1 2 6 mulne0bbd ⊢ φ → B ≠ 0
8 2 5 2 6 7 divcan7d ⊢ φ → B B A ⁢ B B = B A ⁢ B
9 8 eqcomd ⊢ φ → B A ⁢ B = B B A ⁢ B B
10 2 4 dividd ⊢ φ → B B = 1
11 1 2 4 divcan4d ⊢ φ → A ⁢ B B = A
12 10 11 oveq12d ⊢ φ → B B A ⁢ B B = 1 A
13 eqidd ⊢ φ → 1 A = 1 A
14 9 12 13 3eqtrd ⊢ φ → B A ⁢ B = 1 A