This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem his7

Description: Distributive law for inner product. Lemma 3.1(S7) of Beran p. 95. (Contributed by NM, 31-Jul-1999) (New usage is discouraged.)

Ref Expression
Assertion his7 
|- ( ( 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 ax-his2 
 |-  ( ( 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 cjadd 
 |-  ( ( ( 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 hvaddcl 
 |-  ( ( 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 ) ) )