nvmdi

Description: Distributive law for scalar product over subtraction. (Contributed by NM, 14-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvmdi.1	$⊢ X = BaseSet (U)$
	nvmdi.3	$⊢ M = -_{v} (U)$
	nvmdi.4	$⊢ S = \cdot_{𝑠OLD} (U)$
Assertion	nvmdi	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B M C) = (A S B) M (A S C)$

Proof

Step	Hyp	Ref	Expression
1		nvmdi.1	$⊢ X = BaseSet (U)$
2		nvmdi.3	$⊢ M = -_{v} (U)$
3		nvmdi.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		simpr1	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A \in ℂ$
5		simpr2	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to B \in X$
6		neg1cn	$⊢ - 1 \in ℂ$
7	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land C \in X) \to -1 S C \in X$
8	6 7	mp3an2	$⊢ (U \in NrmCVec \land C \in X) \to -1 S C \in X$
9	8	3ad2antr3	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to -1 S C \in X$
10	4 5 9	3jca	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to (A \in ℂ \land B \in X \land -1 S C \in X)$
11		eqid	$⊢ +_{v} (U) = +_{v} (U)$
12	1 11 3	nvdi	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land -1 S C \in X)) \to A S (B +_{v} (U) (-1 S C)) = (A S B) +_{v} (U) (A S (-1 S C))$
13	10 12	syldan	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B +_{v} (U) (-1 S C)) = (A S B) +_{v} (U) (A S (-1 S C))$
14	1 3	nvscom	$⊢ (U \in NrmCVec \land (A \in ℂ \land - 1 \in ℂ \land C \in X)) \to A S (-1 S C) = -1 S (A S C)$
15	6 14	mp3anr2	$⊢ (U \in NrmCVec \land (A \in ℂ \land C \in X)) \to A S (-1 S C) = -1 S (A S C)$
16	15	3adantr2	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S (-1 S C) = -1 S (A S C)$
17	16	oveq2d	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to (A S B) +_{v} (U) (A S (-1 S C)) = (A S B) +_{v} (U) (-1 S (A S C))$
18	13 17	eqtrd	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B +_{v} (U) (-1 S C)) = (A S B) +_{v} (U) (-1 S (A S C))$
19	1 11 3 2	nvmval	$⊢ (U \in NrmCVec \land B \in X \land C \in X) \to B M C = B +_{v} (U) (-1 S C)$
20	19	3adant3r1	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to B M C = B +_{v} (U) (-1 S C)$
21	20	oveq2d	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B M C) = A S (B +_{v} (U) (-1 S C))$
22		simpl	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to U \in NrmCVec$
23	1 3	nvscl	$⊢ (U \in NrmCVec \land A \in ℂ \land B \in X) \to A S B \in X$
24	23	3adant3r3	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S B \in X$
25	1 3	nvscl	$⊢ (U \in NrmCVec \land A \in ℂ \land C \in X) \to A S C \in X$
26	25	3adant3r2	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S C \in X$
27	1 11 3 2	nvmval	$⊢ (U \in NrmCVec \land A S B \in X \land A S C \in X) \to (A S B) M (A S C) = (A S B) +_{v} (U) (-1 S (A S C))$
28	22 24 26 27	syl3anc	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to (A S B) M (A S C) = (A S B) +_{v} (U) (-1 S (A S C))$
29	18 21 28	3eqtr4d	$⊢ (U \in NrmCVec \land (A \in ℂ \land B \in X \land C \in X)) \to A S (B M C) = (A S B) M (A S C)$

Metamath Proof Explorer

Theorem nvmdi

Proof