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	$⊢ V = {Base}_{W}$
	ncvsprp.n	$⊢ N = norm (W)$
	ncvsprp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	ncvsdif.p	$⊢ \underset{˙}{+} = +_{W}$
Assertion	ncvsdif	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = N (B \underset{˙}{+} (-1 \underset{˙}{\cdot} A))$

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	$⊢ V = {Base}_{W}$
2		ncvsprp.n	$⊢ N = norm (W)$
3		ncvsprp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		ncvsdif.p	$⊢ \underset{˙}{+} = +_{W}$
5		elin	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in NrmVec \land W \in ℂVec)$
6		id	$⊢ W \in ℂVec \to W \in ℂVec$
7	6	cvsclm	$⊢ W \in ℂVec \to W \in CMod$
8	5 7	simplbiim	$⊢ W \in (NrmVec \cap ℂVec) \to W \in CMod$
9		eqid	$⊢ -_{W} = -_{W}$
10		eqid	$⊢ Scalar (W) = Scalar (W)$
11	1 4 9 10 3	clmvsubval	$⊢ (W \in CMod \land A \in V \land B \in V) \to A -_{W} B = A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)$
12	11	eqcomd	$⊢ (W \in CMod \land A \in V \land B \in V) \to A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) = A -_{W} B$
13	8 12	syl3an1	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to A \underset{˙}{+} (-1 \underset{˙}{\cdot} B) = A -_{W} B$
14	13	fveq2d	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = N (A -_{W} B)$
15		nvcnlm	$⊢ W \in NrmVec \to W \in NrmMod$
16		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
17	15 16	syl	$⊢ W \in NrmVec \to W \in NrmGrp$
18	17	adantr	$⊢ (W \in NrmVec \land W \in ℂVec) \to W \in NrmGrp$
19	5 18	sylbi	$⊢ W \in (NrmVec \cap ℂVec) \to W \in NrmGrp$
20	1 2 9	nmsub	$⊢ (W \in NrmGrp \land A \in V \land B \in V) \to N (A -_{W} B) = N (B -_{W} A)$
21	19 20	syl3an1	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to N (A -_{W} B) = N (B -_{W} A)$
22	8	3ad2ant1	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to W \in CMod$
23		simp3	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to B \in V$
24		simp2	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to A \in V$
25	1 4 9 10 3	clmvsubval	$⊢ (W \in CMod \land B \in V \land A \in V) \to B -_{W} A = B \underset{˙}{+} (-1 \underset{˙}{\cdot} A)$
26	22 23 24 25	syl3anc	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to B -_{W} A = B \underset{˙}{+} (-1 \underset{˙}{\cdot} A)$
27	26	fveq2d	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to N (B -_{W} A) = N (B \underset{˙}{+} (-1 \underset{˙}{\cdot} A))$
28	14 21 27	3eqtrd	$⊢ (W \in (NrmVec \cap ℂVec) \land A \in V \land B \in V) \to N (A \underset{˙}{+} (-1 \underset{˙}{\cdot} B)) = N (B \underset{˙}{+} (-1 \underset{˙}{\cdot} A))$

Metamath Proof Explorer

Theorem ncvsdif

Proof