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 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) − ( 𝐵 , 𝐶 ) ) )