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 
|- ., = ( .i ` W )
cphipcj.v 
|- V = ( Base ` W )
cphsubdir.m 
|- .- = ( -g ` W )
Assertion cphsubdir 
|- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) ., C ) = ( ( A ., C ) - ( B ., C ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h 
 |-  ., = ( .i ` W )
2 cphipcj.v 
 |-  V = ( Base ` W )
3 cphsubdir.m 
 |-  .- = ( -g ` W )
4 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid 
 |-  ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` W ) )
7 5 1 2 3 6 ipsubdir 
 |-  ( ( W e. PreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) ., C ) = ( ( A ., C ) ( -g ` ( Scalar ` W ) ) ( B ., C ) ) )
8 4 7 sylan 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) ., C ) = ( ( A ., C ) ( -g ` ( Scalar ` W ) ) ( B ., C ) ) )
9 cphclm 
 |-  ( W e. CPreHil -> W e. CMod )
10 9 adantr 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. CMod )
11 4 adantr 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> W e. PreHil )
12 simpr1 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> A e. V )
13 simpr3 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> C e. V )
14 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
15 5 1 2 14 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ C e. V ) -> ( A ., C ) e. ( Base ` ( Scalar ` W ) ) )
16 11 12 13 15 syl3anc 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., C ) e. ( Base ` ( Scalar ` W ) ) )
17 simpr2 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> B e. V )
18 5 1 2 14 ipcl 
 |-  ( ( W e. PreHil /\ B e. V /\ C e. V ) -> ( B ., C ) e. ( Base ` ( Scalar ` W ) ) )
19 11 17 13 18 syl3anc 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( B ., C ) e. ( Base ` ( Scalar ` W ) ) )
20 5 14 clmsub 
 |-  ( ( W e. CMod /\ ( A ., C ) e. ( Base ` ( Scalar ` W ) ) /\ ( B ., C ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( A ., C ) - ( B ., C ) ) = ( ( A ., C ) ( -g ` ( Scalar ` W ) ) ( B ., C ) ) )
21 10 16 19 20 syl3anc 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A ., C ) - ( B ., C ) ) = ( ( A ., C ) ( -g ` ( Scalar ` W ) ) ( B ., C ) ) )
22 8 21 eqtr4d 
 |-  ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) ., C ) = ( ( A ., C ) - ( B ., C ) ) )