Metamath Proof Explorer

Theorem nvmval

Description: Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvmval.1 ⊢ X = BaseSet ⁡ U
nvmval.2 ⊢ G = + v ⁡ U
nvmval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvmval.3 ⊢ M = - v ⁡ U
Assertion nvmval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = A G -1 S B

Proof

Step Hyp Ref Expression
1 nvmval.1 ⊢ X = BaseSet ⁡ U
2 nvmval.2 ⊢ G = + v ⁡ U
3 nvmval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 nvmval.3 ⊢ M = - v ⁡ U
5 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
6 1 2 bafval ⊢ X = ran ⁡ G
7 eqid ⊢ inv ⁡ G = inv ⁡ G
8 eqid ⊢ / g ⁡ G = / g ⁡ G
9 6 7 8 grpodivval ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X → A / g ⁡ G B = A G inv ⁡ G ⁡ B
10 5 9 syl3an1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A / g ⁡ G B = A G inv ⁡ G ⁡ B
11 1 2 4 8 nvm ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = A / g ⁡ G B
12 1 2 3 7 nvinv ⊢ U ∈ NrmCVec ∧ B ∈ X → -1 S B = inv ⁡ G ⁡ B
13 12 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B = inv ⁡ G ⁡ B
14 13 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G -1 S B = A G inv ⁡ G ⁡ B
15 10 11 14 3eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = A G -1 S B