# 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 ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A +h ( -u 1 .h B ) ) .ih C ) = ( ( A .ih C ) + -u ( B .ih C ) ) )`
` |-  ( ( A e. ~H /\ C e. ~H ) -> ( A .ih C ) e. CC )`
` |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih C ) e. CC )`
` |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( B .ih C ) e. CC )`
` |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A .ih C ) + -u ( B .ih C ) ) = ( ( A .ih C ) - ( B .ih C ) ) )`
` |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A -h B ) .ih C ) = ( ( A .ih C ) - ( B .ih C ) ) )`