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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvdif.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvdif.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvdif.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvdif ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 nvdif.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvdif.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 nvdif.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 nvdif.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
5 simp1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑈 ∈ NrmCVec )
6 neg1cn ⊢ - 1 ∈ ℂ
7 6 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → - 1 ∈ ℂ )
8 simp3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
9 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
10 6 9 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
11 10 3adant3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐴 ) ∈ 𝑋 )
12 1 2 3 nvdi ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) ) → ( - 1 𝑆 ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) ) )
13 5 7 8 11 12 syl13anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) ) )
14 1 3 nvnegneg ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) = 𝐴 )
15 14 3adant3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) = 𝐴 )
16 15 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐵 ) 𝐺 ( - 1 𝑆 ( - 1 𝑆 𝐴 ) ) ) = ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) )
17 1 3 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
18 6 17 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
19 18 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
20 simp2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
21 1 2 nvcom ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
22 5 19 20 21 syl3anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( - 1 𝑆 𝐵 ) 𝐺 𝐴 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
23 13 16 22 3eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )
24 23 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) )
25 1 2 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 𝑆 𝐴 ) ∈ 𝑋 ) → ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ∈ 𝑋 )
26 5 8 11 25 syl3anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ∈ 𝑋 )
27 1 3 4 nvm1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) )
28 5 26 27 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 𝑆 ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) )
29 24 28 eqtr3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 𝐺 ( - 1 𝑆 𝐴 ) ) ) )