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 𝑆 𝐴 ) ) ) )