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 = \cdot_{𝑠OLD} (U)$
	nvdif.6	$⊢ N = {norm}_{CV} (U)$
Assertion	nvdif	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 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 = \cdot_{𝑠OLD} (U)$
4		nvdif.6	$⊢ N = {norm}_{CV} (U)$
5		simp1	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to U \in NrmCVec$
6		neg1cn	$⊢ - 1 \in ℂ$
7	6	a1i	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to - 1 \in ℂ$
8		simp3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to B \in X$
9	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land A \in X) \to -1 S A \in X$
10	6 9	mp3an2	$⊢ (U \in NrmCVec \land A \in X) \to -1 S A \in X$
11	10	3adant3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S A \in X$
12	1 2 3	nvdi	$⊢ (U \in NrmCVec \land (- 1 \in ℂ \land B \in X \land -1 S A \in X)) \to -1 S (B G (-1 S A)) = (-1 S B) G (-1 S (-1 S A))$
13	5 7 8 11 12	syl13anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S (B G (-1 S A)) = (-1 S B) G (-1 S (-1 S A))$
14	1 3	nvnegneg	$⊢ (U \in NrmCVec \land A \in X) \to -1 S (-1 S A) = A$
15	14	3adant3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S (-1 S A) = A$
16	15	oveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (-1 S B) G (-1 S (-1 S A)) = (-1 S B) G A$
17	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
18	6 17	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to -1 S B \in X$
19	18	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S B \in X$
20		simp2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A \in X$
21	1 2	nvcom	$⊢ (U \in NrmCVec \land -1 S B \in X \land A \in X) \to (-1 S B) G A = A G (-1 S B)$
22	5 19 20 21	syl3anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to (-1 S B) G A = A G (-1 S B)$
23	13 16 22	3eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S (B G (-1 S A)) = A G (-1 S B)$
24	23	fveq2d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (-1 S (B G (-1 S A))) = N (A G (-1 S B))$
25	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land -1 S A \in X) \to B G (-1 S A) \in X$
26	5 8 11 25	syl3anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to B G (-1 S A) \in X$
27	1 3 4	nvm1	$⊢ (U \in NrmCVec \land B G (-1 S A) \in X) \to N (-1 S (B G (-1 S A))) = N (B G (-1 S A))$
28	5 26 27	syl2anc	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (-1 S (B G (-1 S A))) = N (B G (-1 S A))$
29	24 28	eqtr3d	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to N (A G (-1 S B)) = N (B G (-1 S A))$

Metamath Proof Explorer

Theorem nvdif

Proof