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∈CPreHilOLD∧A∈X∧B∈X∧C∈X→AMBPC=APC−BPC

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∈CPreHilOLD→A∈X→A∈X
5 phnv ⊢U∈CPreHilOLD→U∈NrmCVec
6 neg1cn ⊢−1∈ℂ
7 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
8 1 7 nvscl ⊢U∈NrmCVec∧−1∈ℂ∧B∈X→-1⋅𝑠OLD⁡UB∈X
9 6 8 mp3an2 ⊢U∈NrmCVec∧B∈X→-1⋅𝑠OLD⁡UB∈X
10 5 9 sylan ⊢U∈CPreHilOLD∧B∈X→-1⋅𝑠OLD⁡UB∈X
11 10 ex ⊢U∈CPreHilOLD→B∈X→-1⋅𝑠OLD⁡UB∈X
12 idd ⊢U∈CPreHilOLD→C∈X→C∈X
13 4 11 12 3anim123d ⊢U∈CPreHilOLD→A∈X∧B∈X∧C∈X→A∈X∧-1⋅𝑠OLD⁡UB∈X∧C∈X
14 13 imp ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→A∈X∧-1⋅𝑠OLD⁡UB∈X∧C∈X
15 eqid ⊢+v⁡U=+v⁡U
16 1 15 3 dipdir ⊢U∈CPreHilOLD∧A∈X∧-1⋅𝑠OLD⁡UB∈X∧C∈X→A+v⁡U-1⋅𝑠OLD⁡UBPC=APC+-1⋅𝑠OLD⁡UBPC
17 14 16 syldan ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→A+v⁡U-1⋅𝑠OLD⁡UBPC=APC+-1⋅𝑠OLD⁡UBPC
18 1 15 7 2 nvmval ⊢U∈NrmCVec∧A∈X∧B∈X→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
19 5 18 syl3an1 ⊢U∈CPreHilOLD∧A∈X∧B∈X→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
20 19 3adant3r3 ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→AMB=A+v⁡U-1⋅𝑠OLD⁡UB
21 20 oveq1d ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→AMBPC=A+v⁡U-1⋅𝑠OLD⁡UBPC
22 1 7 3 dipass ⊢U∈CPreHilOLD∧−1∈ℂ∧B∈X∧C∈X→-1⋅𝑠OLD⁡UBPC=-1⁢BPC
23 6 22 mp3anr1 ⊢U∈CPreHilOLD∧B∈X∧C∈X→-1⋅𝑠OLD⁡UBPC=-1⁢BPC
24 1 3 dipcl ⊢U∈NrmCVec∧B∈X∧C∈X→BPC∈ℂ
25 24 3expb ⊢U∈NrmCVec∧B∈X∧C∈X→BPC∈ℂ
26 5 25 sylan ⊢U∈CPreHilOLD∧B∈X∧C∈X→BPC∈ℂ
27 26 mulm1d ⊢U∈CPreHilOLD∧B∈X∧C∈X→-1⁢BPC=−BPC
28 23 27 eqtrd ⊢U∈CPreHilOLD∧B∈X∧C∈X→-1⋅𝑠OLD⁡UBPC=−BPC
29 28 3adantr1 ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→-1⋅𝑠OLD⁡UBPC=−BPC
30 29 oveq2d ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APC+-1⋅𝑠OLD⁡UBPC=APC+−BPC
31 1 3 dipcl ⊢U∈NrmCVec∧A∈X∧C∈X→APC∈ℂ
32 31 3adant3r2 ⊢U∈NrmCVec∧A∈X∧B∈X∧C∈X→APC∈ℂ
33 24 3adant3r1 ⊢U∈NrmCVec∧A∈X∧B∈X∧C∈X→BPC∈ℂ
34 32 33 negsubd ⊢U∈NrmCVec∧A∈X∧B∈X∧C∈X→APC+−BPC=APC−BPC
35 5 34 sylan ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APC+−BPC=APC−BPC
36 30 35 eqtr2d ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APC−BPC=APC+-1⋅𝑠OLD⁡UBPC
37 17 21 36 3eqtr4d ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→AMBPC=APC−BPC