Metamath Proof Explorer

Theorem ip2dii

Description: Inner product of two sums. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ip2dii.1 ⊢ X = BaseSet ⁡ U
ip2dii.2 ⊢ G = + v ⁡ U
ip2dii.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip2dii.u ⊢ U ∈ CPreHil OLD
ip2dii.a ⊢ A ∈ X
ip2dii.b ⊢ B ∈ X
ip2dii.c ⊢ C ∈ X
ip2dii.d ⊢ D ∈ X
Assertion ip2dii ⊢ A G B P C G D = A P C + B P D + A P D + B P C

Proof

Step Hyp Ref Expression
1 ip2dii.1 ⊢ X = BaseSet ⁡ U
2 ip2dii.2 ⊢ G = + v ⁡ U
3 ip2dii.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 ip2dii.u ⊢ U ∈ CPreHil OLD
5 ip2dii.a ⊢ A ∈ X
6 ip2dii.b ⊢ B ∈ X
7 ip2dii.c ⊢ C ∈ X
8 ip2dii.d ⊢ D ∈ X
9 5 7 8 3pm3.2i ⊢ A ∈ X ∧ C ∈ X ∧ D ∈ X
10 1 2 3 dipdi ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ C ∈ X ∧ D ∈ X → A P C G D = A P C + A P D
11 4 9 10 mp2an ⊢ A P C G D = A P C + A P D
12 6 7 8 3pm3.2i ⊢ B ∈ X ∧ C ∈ X ∧ D ∈ X
13 1 2 3 dipdi ⊢ U ∈ CPreHil OLD ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → B P C G D = B P C + B P D
14 4 12 13 mp2an ⊢ B P C G D = B P C + B P D
15 11 14 oveq12i ⊢ A P C G D + B P C G D = A P C + A P D + B P C + B P D
16 4 phnvi ⊢ U ∈ NrmCVec
17 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ C ∈ X ∧ D ∈ X → C G D ∈ X
18 16 7 8 17 mp3an ⊢ C G D ∈ X
19 5 6 18 3pm3.2i ⊢ A ∈ X ∧ B ∈ X ∧ C G D ∈ X
20 1 2 3 dipdir ⊢ U ∈ CPreHil OLD ∧ A ∈ X ∧ B ∈ X ∧ C G D ∈ X → A G B P C G D = A P C G D + B P C G D
21 4 19 20 mp2an ⊢ A G B P C G D = A P C G D + B P C G D
22 1 3 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ C ∈ X → A P C ∈ ℂ
23 16 5 7 22 mp3an ⊢ A P C ∈ ℂ
24 1 3 dipcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ D ∈ X → B P D ∈ ℂ
25 16 6 8 24 mp3an ⊢ B P D ∈ ℂ
26 1 3 dipcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ D ∈ X → A P D ∈ ℂ
27 16 5 8 26 mp3an ⊢ A P D ∈ ℂ
28 1 3 dipcl ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ C ∈ X → B P C ∈ ℂ
29 16 6 7 28 mp3an ⊢ B P C ∈ ℂ
30 23 25 27 29 add42i ⊢ A P C + B P D + A P D + B P C = A P C + A P D + B P C + B P D
31 15 21 30 3eqtr4i ⊢ A G B P C G D = A P C + B P D + A P D + B P C