Theorem ncvsdif

Description: The norm of the difference between two vectors. (Contributed by NM, 1-Dec-2006) (Revised by AV, 8-Oct-2021)

	Ref	Expression
Hypotheses	ncvsprp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ncvsprp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	ncvsprp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	ncvsdif.p	⊢ + = ( +g ‘ 𝑊 )
Assertion	ncvsdif	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - 1 · 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ncvsprp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
3		ncvsprp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		ncvsdif.p	⊢ + = ( +g ‘ 𝑊 )
5		elin	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) )
6		id	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
7	6	cvsclm	⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
8	5 7	simplbiim	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ ℂMod )
9		eqid	⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
10		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
11	1 4 9 10 3	clmvsubval	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
12	11	eqcomd	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) )
13	8 12	syl3an1	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) )
14	13	fveq2d	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) )
15		nvcnlm	⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
16		nlmngp	⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
17	15 16	syl	⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmGrp )
18	17	adantr	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) → 𝑊 ∈ NrmGrp )
19	5 18	sylbi	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → 𝑊 ∈ NrmGrp )
20	1 2 9	nmsub	⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) ) )
21	19 20	syl3an1	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) ) )
22	8	3ad2ant1	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
23		simp3	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
24		simp2	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
25	1 4 9 10 3	clmvsubval	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) = ( 𝐵 + ( - 1 · 𝐴 ) ) )
26	22 23 24 25	syl3anc	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) = ( 𝐵 + ( - 1 · 𝐴 ) ) )
27	26	fveq2d	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐵 ( -g ‘ 𝑊 ) 𝐴 ) ) = ( 𝑁 ‘ ( 𝐵 + ( - 1 · 𝐴 ) ) ) )
28	14 21 27	3eqtrd	⊢ ( ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 + ( - 1 · 𝐵 ) ) ) = ( 𝑁 ‘ ( 𝐵 + ( - 1 · 𝐴 ) ) ) )