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