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 ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P B G C = A P B + A P C

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 ∈ CPreHil OLD ∧ B ∈ X ∧ C ∈ X ∧ A ∈ X → B G C P A = B P A + C P A
9 7 8 sylan2 ⊢ U ∈ CPreHil OLD ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B G C P A = B P A + C P A
10 9 fveq2d ⊢ U ∈ CPreHil OLD ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B G C P A ‾ = B P A + C P A ‾
11 phnv ⊢ U ∈ CPreHil OLD → U ∈ NrmCVec
12 simpl ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → U ∈ NrmCVec
13 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ X → B G C ∈ X
14 13 3com23 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X → B G C ∈ X
15 14 3adant3r3 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B G C ∈ X
16 simpr3 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → A ∈ X
17 1 3 dipcj ⊢ U ∈ NrmCVec ∧ B G C ∈ X ∧ A ∈ X → B G C P A ‾ = A P B G C
18 12 15 16 17 syl3anc ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B G C P A ‾ = A P B G C
19 11 18 sylan ⊢ U ∈ CPreHil OLD ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B G C P A ‾ = A P B G C
20 1 3 dipcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B P A ∈ ℂ
21 20 3adant3r1 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B P A ∈ ℂ
22 1 3 dipcl ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ A ∈ X → C P A ∈ ℂ
23 22 3adant3r2 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → C P A ∈ ℂ
24 21 23 cjaddd ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B P A + C P A ‾ = B P A ‾ + C P A ‾
25 1 3 dipcj ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B P A ‾ = A P B
26 25 3adant3r1 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B P A ‾ = A P B
27 1 3 dipcj ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ A ∈ X → C P A ‾ = A P C
28 27 3adant3r2 ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → C P A ‾ = A P C
29 26 28 oveq12d ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B P A ‾ + C P A ‾ = A P B + A P C
30 24 29 eqtrd ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B P A + C P A ‾ = A P B + A P C
31 11 30 sylan ⊢ U ∈ CPreHil OLD ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → B P A + C P A ‾ = A P B + A P C
32 10 19 31 3eqtr3d ⊢ U ∈ CPreHil OLD ∧ C ∈ X ∧ B ∈ X ∧ A ∈ X → A P B G C = A P B + A P C
33 5 32 sylan2 ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A P B G C = A P B + A P C