Metamath Proof Explorer

Theorem 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 = ⋅ 𝑠OLD ⁡ U
Assertion nvmdi ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → 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 = ⋅ 𝑠OLD ⁡ U
4 simpr1 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A ∈ ℂ
5 simpr2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → B ∈ X
6 neg1cn ⊢ − 1 ∈ ℂ
7 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ C ∈ X → -1 S C ∈ X
8 6 7 mp3an2 ⊢ U ∈ NrmCVec ∧ C ∈ X → -1 S C ∈ X
9 8 3ad2antr3 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → -1 S C ∈ X
10 4 5 9 3jca ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A ∈ ℂ ∧ B ∈ X ∧ -1 S C ∈ X
11 eqid ⊢ + v ⁡ U = + v ⁡ U
12 1 11 3 nvdi ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ -1 S C ∈ X → A S B + v ⁡ U -1 S C = A S B + v ⁡ U A S -1 S C
13 10 12 syldan ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B + v ⁡ U -1 S C = A S B + v ⁡ U A S -1 S C
14 1 3 nvscom ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ − 1 ∈ ℂ ∧ C ∈ X → A S -1 S C = -1 S A S C
15 6 14 mp3anr2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ C ∈ X → A S -1 S C = -1 S A S C
16 15 3adantr2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S -1 S C = -1 S A S C
17 16 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → 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 ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → 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 ∈ NrmCVec ∧ B ∈ X ∧ C ∈ X → B M C = B + v ⁡ U -1 S C
20 19 3adant3r1 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → B M C = B + v ⁡ U -1 S C
21 20 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B M C = A S B + v ⁡ U -1 S C
22 simpl ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → U ∈ NrmCVec
23 1 3 nvscl ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → A S B ∈ X
24 23 3adant3r3 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B ∈ X
25 1 3 nvscl ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ C ∈ X → A S C ∈ X
26 25 3adant3r2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S C ∈ X
27 1 11 3 2 nvmval ⊢ U ∈ NrmCVec ∧ A S B ∈ X ∧ A S C ∈ X → A S B M A S C = A S B + v ⁡ U -1 S A S C
28 22 24 26 27 syl3anc ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B M A S C = A S B + v ⁡ U -1 S A S C
29 18 21 28 3eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B M C = A S B M A S C