Metamath Proof Explorer

Theorem nvnpcan

Description: Cancellation law for a normed complex vector space. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 ⊢ X = BaseSet ⁡ U
nvpncan2.2 ⊢ G = + v ⁡ U
nvpncan2.3 ⊢ M = - v ⁡ U
Assertion nvnpcan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B G B = A

Proof

Step Hyp Ref Expression
1 nvpncan2.1 ⊢ X = BaseSet ⁡ U
2 nvpncan2.2 ⊢ G = + v ⁡ U
3 nvpncan2.3 ⊢ M = - v ⁡ U
4 simprl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A ∈ X
5 simprr ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B ∈ X
6 4 5 5 3jca ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A ∈ X ∧ B ∈ X ∧ B ∈ X
7 1 2 3 nvaddsub ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ B ∈ X → A G B M B = A M B G B
8 6 7 syldan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M B = A M B G B
9 8 3impb ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M B = A M B G B
10 1 2 3 nvpncan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M B = A
11 9 10 eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B G B = A