Metamath Proof Explorer

Theorem his2sub2

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 his2sub 
 |-  ( ( B e. ~H /\ C e. ~H /\ A e. ~H ) -> ( ( B -h C ) .ih A ) = ( ( B .ih A ) - ( C .ih A ) ) )
2 1 fveq2d 
 |-  ( ( B e. ~H /\ C e. ~H /\ A e. ~H ) -> ( * ` ( ( B -h C ) .ih A ) ) = ( * ` ( ( B .ih A ) - ( C .ih A ) ) ) )
3 hicl 
 |-  ( ( B e. ~H /\ A e. ~H ) -> ( B .ih A ) e. CC )
4 hicl 
 |-  ( ( C e. ~H /\ A e. ~H ) -> ( C .ih A ) e. CC )
5 cjsub 
 |-  ( ( ( B .ih A ) e. CC /\ ( C .ih A ) e. CC ) -> ( * ` ( ( B .ih A ) - ( C .ih A ) ) ) = ( ( * ` ( B .ih A ) ) - ( * ` ( C .ih A ) ) ) )
6 3 4 5 syl2an 
 |-  ( ( ( B e. ~H /\ A e. ~H ) /\ ( C e. ~H /\ A e. ~H ) ) -> ( * ` ( ( B .ih A ) - ( C .ih A ) ) ) = ( ( * ` ( B .ih A ) ) - ( * ` ( C .ih A ) ) ) )
7 6 3impdir 
 |-  ( ( B e. ~H /\ C e. ~H /\ A e. ~H ) -> ( * ` ( ( B .ih A ) - ( C .ih A ) ) ) = ( ( * ` ( B .ih A ) ) - ( * ` ( C .ih A ) ) ) )
8 2 7 eqtrd 
 |-  ( ( B e. ~H /\ C e. ~H /\ A e. ~H ) -> ( * ` ( ( B -h C ) .ih A ) ) = ( ( * ` ( B .ih A ) ) - ( * ` ( C .ih A ) ) ) )
9 8 3comr 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( * ` ( ( B -h C ) .ih A ) ) = ( ( * ` ( B .ih A ) ) - ( * ` ( C .ih A ) ) ) )
10 hvsubcl 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B -h C ) e. ~H )
11 ax-his1 
 |-  ( ( A e. ~H /\ ( B -h C ) e. ~H ) -> ( A .ih ( B -h C ) ) = ( * ` ( ( B -h C ) .ih A ) ) )
12 10 11 sylan2 
 |-  ( ( A e. ~H /\ ( B e. ~H /\ C e. ~H ) ) -> ( A .ih ( B -h C ) ) = ( * ` ( ( B -h C ) .ih A ) ) )
13 12 3impb 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih ( B -h C ) ) = ( * ` ( ( B -h C ) .ih A ) ) )
14 ax-his1 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )
15 14 3adant3 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) )
16 ax-his1 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( A .ih C ) = ( * ` ( C .ih A ) ) )
17 16 3adant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih C ) = ( * ` ( C .ih A ) ) )
18 15 17 oveq12d 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( ( A .ih B ) - ( A .ih C ) ) = ( ( * ` ( B .ih A ) ) - ( * ` ( C .ih A ) ) ) )
19 9 13 18 3eqtr4d 
 |-  ( ( A e. ~H /\ B e. ~H /\ C e. ~H ) -> ( A .ih ( B -h C ) ) = ( ( A .ih B ) - ( A .ih C ) ) )