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