Metamath Proof Explorer


Theorem cphsubdir

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

Ref Expression
Hypotheses cphipcj.h , = ( ·𝑖𝑊 )
cphipcj.v 𝑉 = ( Base ‘ 𝑊 )
cphsubdir.m = ( -g𝑊 )
Assertion cphsubdir ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐴 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) − ( 𝐵 , 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h , = ( ·𝑖𝑊 )
2 cphipcj.v 𝑉 = ( Base ‘ 𝑊 )
3 cphsubdir.m = ( -g𝑊 )
4 cphphl ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
5 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ( -g ‘ ( Scalar ‘ 𝑊 ) ) = ( -g ‘ ( Scalar ‘ 𝑊 ) )
7 5 1 2 3 6 ipsubdir ( ( 𝑊 ∈ PreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐴 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) )
8 4 7 sylan ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐴 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) )
9 cphclm ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
10 9 adantr ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → 𝑊 ∈ ℂMod )
11 4 adantr ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → 𝑊 ∈ PreHil )
12 simpr1 ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → 𝐴𝑉 )
13 simpr3 ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → 𝐶𝑉 )
14 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
15 5 1 2 14 ipcl ( ( 𝑊 ∈ PreHil ∧ 𝐴𝑉𝐶𝑉 ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
16 11 12 13 15 syl3anc ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 simpr2 ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → 𝐵𝑉 )
18 5 1 2 14 ipcl ( ( 𝑊 ∈ PreHil ∧ 𝐵𝑉𝐶𝑉 ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 11 17 13 18 syl3anc ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20 5 14 clmsub ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝐵 , 𝐶 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝐴 , 𝐶 ) − ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 , 𝐶 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) )
21 10 16 19 20 syl3anc ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐴 , 𝐶 ) − ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 , 𝐶 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( 𝐵 , 𝐶 ) ) )
22 8 21 eqtr4d ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐴 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) − ( 𝐵 , 𝐶 ) ) )