Metamath Proof Explorer

Theorem dipsubdi

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 dipsubdi ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APBMC=APB−APC

Proof

Step Hyp Ref Expression
1 ipsubdir.1 ⊢X=BaseSet⁡U
2 ipsubdir.3 ⊢M=-v⁡U
3 ipsubdir.7 ⊢P=⋅𝑖OLD⁡U
4 id ⊢C∈X∧B∈X∧A∈X→C∈X∧B∈X∧A∈X
5 4 3com13 ⊢A∈X∧B∈X∧C∈X→C∈X∧B∈X∧A∈X
6 id ⊢B∈X∧C∈X∧A∈X→B∈X∧C∈X∧A∈X
7 6 3com12 ⊢C∈X∧B∈X∧A∈X→B∈X∧C∈X∧A∈X
8 1 2 3 dipsubdir ⊢U∈CPreHilOLD∧B∈X∧C∈X∧A∈X→BMCPA=BPA−CPA
9 7 8 sylan2 ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BMCPA=BPA−CPA
10 9 fveq2d ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BMCPA‾=BPA−CPA‾
11 phnv ⊢U∈CPreHilOLD→U∈NrmCVec
12 simpl ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→U∈NrmCVec
13 1 2 nvmcl ⊢U∈NrmCVec∧B∈X∧C∈X→BMC∈X
14 13 3com23 ⊢U∈NrmCVec∧C∈X∧B∈X→BMC∈X
15 14 3adant3r3 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BMC∈X
16 simpr3 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→A∈X
17 1 3 dipcj ⊢U∈NrmCVec∧BMC∈X∧A∈X→BMCPA‾=APBMC
18 12 15 16 17 syl3anc ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BMCPA‾=APBMC
19 11 18 sylan ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BMCPA‾=APBMC
20 1 3 dipcl ⊢U∈NrmCVec∧B∈X∧A∈X→BPA∈ℂ
21 20 3adant3r1 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA∈ℂ
22 1 3 dipcl ⊢U∈NrmCVec∧C∈X∧A∈X→CPA∈ℂ
23 22 3adant3r2 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→CPA∈ℂ
24 cjsub ⊢BPA∈ℂ∧CPA∈ℂ→BPA−CPA‾=BPA‾−CPA‾
25 21 23 24 syl2anc ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA−CPA‾=BPA‾−CPA‾
26 1 3 dipcj ⊢U∈NrmCVec∧B∈X∧A∈X→BPA‾=APB
27 26 3adant3r1 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA‾=APB
28 1 3 dipcj ⊢U∈NrmCVec∧C∈X∧A∈X→CPA‾=APC
29 28 3adant3r2 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→CPA‾=APC
30 27 29 oveq12d ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA‾−CPA‾=APB−APC
31 25 30 eqtrd ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA−CPA‾=APB−APC
32 11 31 sylan ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BPA−CPA‾=APB−APC
33 10 19 32 3eqtr3d ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→APBMC=APB−APC
34 5 33 sylan2 ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APBMC=APB−APC