Metamath Proof Explorer

Theorem his2sub

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion his2sub 
|- ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih C ) = ( ( A .ih C ) - ( B .ih C ) ) )

Proof

Step Hyp Ref Expression
1 hvsubval 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
2 1 oveq1d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h B ) .ih C ) = ( ( A +h ( -u 1 .h B ) ) .ih C ) )
3 2 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih C ) = ( ( A +h ( -u 1 .h B ) ) .ih C ) )
4 neg1cn 
 |-  -u 1 e. CC
5 hvmulcl 
 |-  ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H )
6 4 5 mpan 
 |-  ( B e. ~H -> ( -u 1 .h B ) e. ~H )
7 ax-his2 
 |-  ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) .ih C ) = ( ( A .ih C ) + ( ( -u 1 .h B ) .ih C ) ) )
8 6 7 syl3an2 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) .ih C ) = ( ( A .ih C ) + ( ( -u 1 .h B ) .ih C ) ) )
9 ax-his3 
 |-  ( ( -u 1 e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) .ih C ) = ( -u 1 x. ( B .ih C ) ) )
10 4 9 mp3an1 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) .ih C ) = ( -u 1 x. ( B .ih C ) ) )
11 hicl 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B .ih C ) e. CC )
12 11 mulm1d 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( -u 1 x. ( B .ih C ) ) = -u ( B .ih C ) )
13 10 12 eqtrd 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( -u 1 .h B ) .ih C ) = -u ( B .ih C ) )
14 13 oveq2d 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( A .ih C ) + ( ( -u 1 .h B ) .ih C ) ) = ( ( A .ih C ) + -u ( B .ih C ) ) )
15 14 3adant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A .ih C ) + ( ( -u 1 .h B ) .ih C ) ) = ( ( A .ih C ) + -u ( B .ih C ) ) )
16 8 15 eqtrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) .ih C ) = ( ( A .ih C ) + -u ( B .ih C ) ) )
17 hicl 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( A .ih C ) e. CC )
18 17 3adant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih C ) e. CC )
19 11 3adant1 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( B .ih C ) e. CC )
20 18 19 negsubd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A .ih C ) + -u ( B .ih C ) ) = ( ( A .ih C ) - ( B .ih C ) ) )
21 3 16 20 3eqtrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih C ) = ( ( A .ih C ) - ( B .ih C ) ) )