Metamath Proof Explorer

Theorem dipdi

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

Ref Expression
Hypotheses dipdir.1 ⊢X=BaseSet⁡U
dipdir.2 ⊢G=+v⁡U
dipdir.7 ⊢P=⋅𝑖OLD⁡U
Assertion dipdi ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APBGC=APB+APC

Proof

Step Hyp Ref Expression
1 dipdir.1 ⊢X=BaseSet⁡U
2 dipdir.2 ⊢G=+v⁡U
3 dipdir.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 dipdir ⊢U∈CPreHilOLD∧B∈X∧C∈X∧A∈X→BGCPA=BPA+CPA
9 7 8 sylan2 ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BGCPA=BPA+CPA
10 9 fveq2d ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BGCPA‾=BPA+CPA‾
11 phnv ⊢U∈CPreHilOLD→U∈NrmCVec
12 simpl ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→U∈NrmCVec
13 1 2 nvgcl ⊢U∈NrmCVec∧B∈X∧C∈X→BGC∈X
14 13 3com23 ⊢U∈NrmCVec∧C∈X∧B∈X→BGC∈X
15 14 3adant3r3 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BGC∈X
16 simpr3 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→A∈X
17 1 3 dipcj ⊢U∈NrmCVec∧BGC∈X∧A∈X→BGCPA‾=APBGC
18 12 15 16 17 syl3anc ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BGCPA‾=APBGC
19 11 18 sylan ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BGCPA‾=APBGC
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 21 23 cjaddd ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA+CPA‾=BPA‾+CPA‾
25 1 3 dipcj ⊢U∈NrmCVec∧B∈X∧A∈X→BPA‾=APB
26 25 3adant3r1 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA‾=APB
27 1 3 dipcj ⊢U∈NrmCVec∧C∈X∧A∈X→CPA‾=APC
28 27 3adant3r2 ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→CPA‾=APC
29 26 28 oveq12d ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA‾+CPA‾=APB+APC
30 24 29 eqtrd ⊢U∈NrmCVec∧C∈X∧B∈X∧A∈X→BPA+CPA‾=APB+APC
31 11 30 sylan ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→BPA+CPA‾=APB+APC
32 10 19 31 3eqtr3d ⊢U∈CPreHilOLD∧C∈X∧B∈X∧A∈X→APBGC=APB+APC
33 5 32 sylan2 ⊢U∈CPreHilOLD∧A∈X∧B∈X∧C∈X→APBGC=APB+APC