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

Metamath Proof Explorer

Theorem his5

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

Ref Expression
Assertion his5 
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B .ih ( A .h C ) ) = ( ( * ` A ) x. ( B .ih C ) ) )

Proof

Step Hyp Ref Expression
1 hvmulcl 
 |-  ( ( A e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
2 ax-his1 
 |-  ( ( B e. ~H /\ ( A .h C ) e. ~H ) -> ( B .ih ( A .h C ) ) = ( * ` ( ( A .h C ) .ih B ) ) )
3 1 2 sylan2 
 |-  ( ( B e. ~H /\ ( A e. CC /\ C e. ~H ) ) -> ( B .ih ( A .h C ) ) = ( * ` ( ( A .h C ) .ih B ) ) )
4 3 3impb 
 |-  ( ( B e. ~H /\ A e. CC /\ C e. ~H ) -> ( B .ih ( A .h C ) ) = ( * ` ( ( A .h C ) .ih B ) ) )
5 4 3com12 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B .ih ( A .h C ) ) = ( * ` ( ( A .h C ) .ih B ) ) )
6 ax-his3 
 |-  ( ( A e. CC /\ C e. ~H /\ B e. ~H ) -> ( ( A .h C ) .ih B ) = ( A x. ( C .ih B ) ) )
7 6 3com23 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h C ) .ih B ) = ( A x. ( C .ih B ) ) )
8 7 fveq2d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( * ` ( ( A .h C ) .ih B ) ) = ( * ` ( A x. ( C .ih B ) ) ) )
9 hicl 
 |-  ( ( C e. ~H /\ B e. ~H ) -> ( C .ih B ) e. CC )
10 cjmul 
 |-  ( ( A e. CC /\ ( C .ih B ) e. CC ) -> ( * ` ( A x. ( C .ih B ) ) ) = ( ( * ` A ) x. ( * ` ( C .ih B ) ) ) )
11 9 10 sylan2 
 |-  ( ( A e. CC /\ ( C e. ~H /\ B e. ~H ) ) -> ( * ` ( A x. ( C .ih B ) ) ) = ( ( * ` A ) x. ( * ` ( C .ih B ) ) ) )
12 11 3impb 
 |-  ( ( A e. CC /\ C e. ~H /\ B e. ~H ) -> ( * ` ( A x. ( C .ih B ) ) ) = ( ( * ` A ) x. ( * ` ( C .ih B ) ) ) )
13 12 3com23 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( * ` ( A x. ( C .ih B ) ) ) = ( ( * ` A ) x. ( * ` ( C .ih B ) ) ) )
14 ax-his1 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B .ih C ) = ( * ` ( C .ih B ) ) )
15 14 3adant1 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B .ih C ) = ( * ` ( C .ih B ) ) )
16 15 oveq2d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( * ` A ) x. ( B .ih C ) ) = ( ( * ` A ) x. ( * ` ( C .ih B ) ) ) )
17 13 16 eqtr4d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( * ` ( A x. ( C .ih B ) ) ) = ( ( * ` A ) x. ( B .ih C ) ) )
18 5 8 17 3eqtrd 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B .ih ( A .h C ) ) = ( ( * ` A ) x. ( B .ih C ) ) )