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 𝑋 = ( BaseSet ‘ 𝑈 )
ip2dii.2 𝐺 = ( +𝑣𝑈 )
ip2dii.7 𝑃 = ( ·𝑖OLD𝑈 )
ip2dii.u 𝑈 ∈ CPreHilOLD
ip2dii.a 𝐴𝑋
ip2dii.b 𝐵𝑋
ip2dii.c 𝐶𝑋
ip2dii.d 𝐷𝑋
Assertion ip2dii ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) + ( ( 𝐴 𝑃 𝐷 ) + ( 𝐵 𝑃 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ip2dii.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip2dii.2 𝐺 = ( +𝑣𝑈 )
3 ip2dii.7 𝑃 = ( ·𝑖OLD𝑈 )
4 ip2dii.u 𝑈 ∈ CPreHilOLD
5 ip2dii.a 𝐴𝑋
6 ip2dii.b 𝐵𝑋
7 ip2dii.c 𝐶𝑋
8 ip2dii.d 𝐷𝑋
9 5 7 8 3pm3.2i ( 𝐴𝑋𝐶𝑋𝐷𝑋 )
10 1 2 3 dipdi ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴𝑋𝐶𝑋𝐷𝑋 ) ) → ( 𝐴 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐴 𝑃 𝐷 ) ) )
11 4 9 10 mp2an ( 𝐴 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐴 𝑃 𝐷 ) )
12 6 7 8 3pm3.2i ( 𝐵𝑋𝐶𝑋𝐷𝑋 )
13 1 2 3 dipdi ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐵𝑋𝐶𝑋𝐷𝑋 ) ) → ( 𝐵 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐵 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) )
14 4 12 13 mp2an ( 𝐵 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐵 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) )
15 11 14 oveq12i ( ( 𝐴 𝑃 ( 𝐶 𝐺 𝐷 ) ) + ( 𝐵 𝑃 ( 𝐶 𝐺 𝐷 ) ) ) = ( ( ( 𝐴 𝑃 𝐶 ) + ( 𝐴 𝑃 𝐷 ) ) + ( ( 𝐵 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) )
16 4 phnvi 𝑈 ∈ NrmCVec
17 1 2 nvgcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐶𝑋𝐷𝑋 ) → ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 )
18 16 7 8 17 mp3an ( 𝐶 𝐺 𝐷 ) ∈ 𝑋
19 5 6 18 3pm3.2i ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 )
20 1 2 3 dipdir ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐶 𝐺 𝐷 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑃 ( 𝐶 𝐺 𝐷 ) ) + ( 𝐵 𝑃 ( 𝐶 𝐺 𝐷 ) ) ) )
21 4 19 20 mp2an ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝑃 ( 𝐶 𝐺 𝐷 ) ) + ( 𝐵 𝑃 ( 𝐶 𝐺 𝐷 ) ) )
22 1 3 dipcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐶𝑋 ) → ( 𝐴 𝑃 𝐶 ) ∈ ℂ )
23 16 5 7 22 mp3an ( 𝐴 𝑃 𝐶 ) ∈ ℂ
24 1 3 dipcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐷𝑋 ) → ( 𝐵 𝑃 𝐷 ) ∈ ℂ )
25 16 6 8 24 mp3an ( 𝐵 𝑃 𝐷 ) ∈ ℂ
26 1 3 dipcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐷𝑋 ) → ( 𝐴 𝑃 𝐷 ) ∈ ℂ )
27 16 5 8 26 mp3an ( 𝐴 𝑃 𝐷 ) ∈ ℂ
28 1 3 dipcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐵𝑋𝐶𝑋 ) → ( 𝐵 𝑃 𝐶 ) ∈ ℂ )
29 16 6 7 28 mp3an ( 𝐵 𝑃 𝐶 ) ∈ ℂ
30 23 25 27 29 add42i ( ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) + ( ( 𝐴 𝑃 𝐷 ) + ( 𝐵 𝑃 𝐶 ) ) ) = ( ( ( 𝐴 𝑃 𝐶 ) + ( 𝐴 𝑃 𝐷 ) ) + ( ( 𝐵 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) )
31 15 21 30 3eqtr4i ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) + ( ( 𝐴 𝑃 𝐷 ) + ( 𝐵 𝑃 𝐶 ) ) )