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

Metamath Proof Explorer

Theorem brafnmul

Description: Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion brafnmul 
|- ( ( A e. CC /\ B e. ~H ) -> ( bra ` ( A .h B ) ) = ( ( * ` A ) .fn ( bra ` B ) ) )

Proof

Step Hyp Ref Expression
1 hvmulcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
2 brafval 
 |-  ( ( A .h B ) e. ~H -> ( bra ` ( A .h B ) ) = ( x e. ~H |-> ( x .ih ( A .h B ) ) ) )
3 1 2 syl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( bra ` ( A .h B ) ) = ( x e. ~H |-> ( x .ih ( A .h B ) ) ) )
4 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
5 brafn 
 |-  ( B e. ~H -> ( bra ` B ) : ~H --> CC )
6 hfmmval 
 |-  ( ( ( * ` A ) e. CC /\ ( bra ` B ) : ~H --> CC ) -> ( ( * ` A ) .fn ( bra ` B ) ) = ( x e. ~H |-> ( ( * ` A ) x. ( ( bra ` B ) ` x ) ) ) )
7 4 5 6 syl2an 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( ( * ` A ) .fn ( bra ` B ) ) = ( x e. ~H |-> ( ( * ` A ) x. ( ( bra ` B ) ` x ) ) ) )
8 his5 
 |-  ( ( A e. CC /\ x e. ~H /\ B e. ~H ) -> ( x .ih ( A .h B ) ) = ( ( * ` A ) x. ( x .ih B ) ) )
9 8 3expa 
 |-  ( ( ( A e. CC /\ x e. ~H ) /\ B e. ~H ) -> ( x .ih ( A .h B ) ) = ( ( * ` A ) x. ( x .ih B ) ) )
10 9 an32s 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ x e. ~H ) -> ( x .ih ( A .h B ) ) = ( ( * ` A ) x. ( x .ih B ) ) )
11 braval 
 |-  ( ( B e. ~H /\ x e. ~H ) -> ( ( bra ` B ) ` x ) = ( x .ih B ) )
12 11 adantll 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ x e. ~H ) -> ( ( bra ` B ) ` x ) = ( x .ih B ) )
13 12 oveq2d 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ x e. ~H ) -> ( ( * ` A ) x. ( ( bra ` B ) ` x ) ) = ( ( * ` A ) x. ( x .ih B ) ) )
14 10 13 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ x e. ~H ) -> ( x .ih ( A .h B ) ) = ( ( * ` A ) x. ( ( bra ` B ) ` x ) ) )
15 14 mpteq2dva 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( x e. ~H |-> ( x .ih ( A .h B ) ) ) = ( x e. ~H |-> ( ( * ` A ) x. ( ( bra ` B ) ` x ) ) ) )
16 7 15 eqtr4d 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( ( * ` A ) .fn ( bra ` B ) ) = ( x e. ~H |-> ( x .ih ( A .h B ) ) ) )
17 3 16 eqtr4d 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( bra ` ( A .h B ) ) = ( ( * ` A ) .fn ( bra ` B ) ) )