Metamath Proof Explorer

Theorem dipsubdir

Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipsubdir.1 ⊢ X = BaseSet ⁡ U
ipsubdir.3 ⊢ M = - v ⁡ U
ipsubdir.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion dipsubdir ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A M B P C = A P C − B P C

Proof

Step Hyp Ref Expression
1 ipsubdir.1 ⊢ X = BaseSet ⁡ U
2 ipsubdir.3 ⊢ M = - v ⁡ U
3 ipsubdir.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 idd ⊢ U ∈ CPreHil OLD → A ∈ X → A ∈ X
5 phnv ⊢ U ∈ CPreHil OLD → U ∈ NrmCVec
6 neg1cn ⊢ − 1 ∈ ℂ
7 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
8 1 7 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X
9 6 8 mp3an2 ⊢ U ∈ NrmCVec ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X
10 5 9 sylan ⊢ U ∈ CPreHil OLD ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X
11 10 ex ⊢ U ∈ CPreHil OLD → B ∈ X → -1 ⋅ 𝑠OLD ⁡ U B ∈ X
12 idd ⊢ U ∈ CPreHil OLD → C ∈ X → C ∈ X
13 4 11 12 3anim123d ⊢ U ∈ CPreHil OLD → A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U B ∈ X ∧ C ∈ X
14 13 imp ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U B ∈ X ∧ C ∈ X
15 eqid ⊢ + v ⁡ U = + v ⁡ U
16 1 15 3 dipdir ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U B ∈ X ∧ C ∈ X → A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B P C = A P C + -1 ⋅ 𝑠OLD ⁡ U B P C
17 14 16 syldan ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B P C = A P C + -1 ⋅ 𝑠OLD ⁡ U B P C
18 1 15 7 2 nvmval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
19 5 18 syl3an1 ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
20 19 3adant3r3 ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A M B = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B
21 20 oveq1d ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A M B P C = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U B P C
22 1 7 3 dipass ⊢ U ∈ CPreHil OLD ∧ − 1 ∈ ℂ ∧ B ∈ X ∧ C ∈ X → -1 ⋅ 𝑠OLD ⁡ U B P C = -1 ⁢ B P C
23 6 22 mp3anr1 ⊢ U ∈ CPreHil OLD ∧ B ∈ X ∧ C ∈ X → -1 ⋅ 𝑠OLD ⁡ U B P C = -1 ⁢ B P C
24 1 3 dipcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ X → B P C ∈ ℂ
25 24 3expb ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ X → B P C ∈ ℂ
26 5 25 sylan ⊢ U ∈ CPreHil OLD ∧ B ∈ X ∧ C ∈ X → B P C ∈ ℂ
27 26 mulm1d ⊢ U ∈ CPreHil OLD ∧ B ∈ X ∧ C ∈ X → -1 ⁢ B P C = − B P C
28 23 27 eqtrd ⊢ U ∈ CPreHil OLD ∧ B ∈ X ∧ C ∈ X → -1 ⋅ 𝑠OLD ⁡ U B P C = − B P C
29 28 3adantr1 ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → -1 ⋅ 𝑠OLD ⁡ U B P C = − B P C
30 29 oveq2d ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P C + -1 ⋅ 𝑠OLD ⁡ U B P C = A P C + − B P C
31 1 3 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ C ∈ X → A P C ∈ ℂ
32 31 3adant3r2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P C ∈ ℂ
33 24 3adant3r1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B P C ∈ ℂ
34 32 33 negsubd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P C + − B P C = A P C − B P C
35 5 34 sylan ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P C + − B P C = A P C − B P C
36 30 35 eqtr2d ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P C − B P C = A P C + -1 ⋅ 𝑠OLD ⁡ U B P C
37 17 21 36 3eqtr4d ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A M B P C = A P C − B P C