Metamath Proof Explorer

Theorem nvdif

Description: The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvdif.1 ⊢ X = BaseSet ⁡ U
nvdif.2 ⊢ G = + v ⁡ U
nvdif.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvdif.6 ⊢ N = norm CV ⁡ U
Assertion nvdif ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A G -1 S B = N ⁡ B G -1 S A

Proof

Step Hyp Ref Expression
1 nvdif.1 ⊢ X = BaseSet ⁡ U
2 nvdif.2 ⊢ G = + v ⁡ U
3 nvdif.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 nvdif.6 ⊢ N = norm CV ⁡ U
5 simp1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → U ∈ NrmCVec
6 neg1cn ⊢ − 1 ∈ ℂ
7 6 a1i ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → − 1 ∈ ℂ
8 simp3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B ∈ X
9 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → -1 S A ∈ X
10 6 9 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S A ∈ X
11 10 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S A ∈ X
12 1 2 3 nvdi ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X ∧ -1 S A ∈ X → -1 S B G -1 S A = -1 S B G -1 S -1 S A
13 5 7 8 11 12 syl13anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B G -1 S A = -1 S B G -1 S -1 S A
14 1 3 nvnegneg ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 S -1 S A = A
15 14 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S -1 S A = A
16 15 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B G -1 S -1 S A = -1 S B G A
17 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 S B ∈ X
18 6 17 mp3an2 ⊢ U ∈ NrmCVec ∧ B ∈ X → -1 S B ∈ X
19 18 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B ∈ X
20 simp2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A ∈ X
21 1 2 nvcom ⊢ U ∈ NrmCVec ∧ -1 S B ∈ X ∧ A ∈ X → -1 S B G A = A G -1 S B
22 5 19 20 21 syl3anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B G A = A G -1 S B
23 13 16 22 3eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B G -1 S A = A G -1 S B
24 23 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ -1 S B G -1 S A = N ⁡ A G -1 S B
25 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ -1 S A ∈ X → B G -1 S A ∈ X
26 5 8 11 25 syl3anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B G -1 S A ∈ X
27 1 3 4 nvm1 ⊢ U ∈ NrmCVec ∧ B G -1 S A ∈ X → N ⁡ -1 S B G -1 S A = N ⁡ B G -1 S A
28 5 26 27 syl2anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ -1 S B G -1 S A = N ⁡ B G -1 S A
29 24 28 eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → N ⁡ A G -1 S B = N ⁡ B G -1 S A