Theorem cph2di

Description: Distributive law for inner product. Complex version of ip2di . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cphdir.P	⊢ + = ( +g ‘ 𝑊 )
	cph2di.1	⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
	cph2di.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	cph2di.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	cph2di.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	cph2di.5	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	cph2di	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) + ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
2		cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		cphdir.P	⊢ + = ( +g ‘ 𝑊 )
4		cph2di.1	⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
5		cph2di.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		cph2di.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		cph2di.4	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		cph2di.5	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10		eqid	⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
11		cphphl	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
12	4 11	syl	⊢ ( 𝜑 → 𝑊 ∈ PreHil )
13	9 1 2 3 10 12 5 6 7 8	ip2di	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐷 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) ) )
14		cphclm	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
15	9	clmadd	⊢ ( 𝑊 ∈ ℂMod → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
16	4 14 15	3syl	⊢ ( 𝜑 → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
17	16	oveqd	⊢ ( 𝜑 → ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) = ( ( 𝐴 , 𝐶 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐷 ) ) )
18	16	oveqd	⊢ ( 𝜑 → ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 , 𝐷 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) )
19	16 17 18	oveq123d	⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) + ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐷 ) ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) ) )
20	13 19	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) , ( 𝐶 + 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) + ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )