Metamath Proof Explorer

Theorem cph2subdi

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

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

Proof

Step Hyp Ref Expression
1 cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
2 cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 cphsubdir.m ⊢ − = ( -g ‘ 𝑊 )
4 cph2subdi.1 ⊢ ( 𝜑 → 𝑊 ∈ ℂPreHil )
5 cph2subdi.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 cph2subdi.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7 cph2subdi.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8 cph2subdi.5 ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
10 4 9 syl ⊢ ( 𝜑 → 𝑊 ∈ ℂMod )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 11 clmadd ⊢ ( 𝑊 ∈ ℂMod → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
13 10 12 syl ⊢ ( 𝜑 → + = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
14 13 oveqd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) = ( ( 𝐴 , 𝐶 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐷 ) ) )
15 13 oveqd ⊢ ( 𝜑 → ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 , 𝐷 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) )
16 14 15 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐷 ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) ) )
17 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
18 4 17 syl ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
19 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
20 11 1 2 19 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21 18 5 7 20 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
22 11 1 2 19 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐵 , 𝐷 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 18 6 8 22 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐷 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
24 11 19 clmacl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝐵 , 𝐷 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
25 10 21 23 24 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
26 11 1 2 19 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐴 , 𝐷 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
27 18 5 8 26 syl3anc ⊢ ( 𝜑 → ( 𝐴 , 𝐷 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
28 11 1 2 19 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29 18 6 7 28 syl3anc ⊢ ( 𝜑 → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
30 11 19 clmacl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 , 𝐷 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝐵 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
31 10 27 29 30 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32 11 19 clmsub ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) − ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )
33 10 25 31 32 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) − ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )
34 eqid ⊢ ( -g ‘ ( Scalar ‘ 𝑊 ) ) = ( -g ‘ ( Scalar ‘ 𝑊 ) )
35 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
36 11 1 2 3 34 35 18 5 6 7 8 ip2subdi ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐷 ) ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 , 𝐷 ) ( +g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) ) )
37 16 33 36 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) , ( 𝐶 − 𝐷 ) ) = ( ( ( 𝐴 , 𝐶 ) + ( 𝐵 , 𝐷 ) ) − ( ( 𝐴 , 𝐷 ) + ( 𝐵 , 𝐶 ) ) ) )