This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝐴 𝐺 𝐵 ) 𝑃 ( 𝐶 𝐺 𝐷 ) ) = ( ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐷 ) ) + ( ( 𝐴 𝑃 𝐷 ) + ( 𝐵 𝑃 𝐶 ) ) )