Metamath Proof Explorer

Theorem cnvbramul

Description: Multiplication property of the converse bra function. (Contributed by NM, 31-May-2006) (New usage is discouraged.)

Ref Expression
Assertion cnvbramul 
|- ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( `' bra ` ( A .fn T ) ) = ( ( * ` A ) .h ( `' bra ` T ) ) )

Proof

Step Hyp Ref Expression
1 cnvbracl 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( `' bra ` T ) e. ~H )
2 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
3 brafnmul 
 |-  ( ( ( * ` A ) e. CC /\ ( `' bra ` T ) e. ~H ) -> ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) = ( ( * ` ( * ` A ) ) .fn ( bra ` ( `' bra ` T ) ) ) )
4 2 3 sylan 
 |-  ( ( A e. CC /\ ( `' bra ` T ) e. ~H ) -> ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) = ( ( * ` ( * ` A ) ) .fn ( bra ` ( `' bra ` T ) ) ) )
5 cjcj 
 |-  ( A e. CC -> ( * ` ( * ` A ) ) = A )
6 5 adantr 
 |-  ( ( A e. CC /\ ( `' bra ` T ) e. ~H ) -> ( * ` ( * ` A ) ) = A )
7 6 oveq1d 
 |-  ( ( A e. CC /\ ( `' bra ` T ) e. ~H ) -> ( ( * ` ( * ` A ) ) .fn ( bra ` ( `' bra ` T ) ) ) = ( A .fn ( bra ` ( `' bra ` T ) ) ) )
8 4 7 eqtrd 
 |-  ( ( A e. CC /\ ( `' bra ` T ) e. ~H ) -> ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) = ( A .fn ( bra ` ( `' bra ` T ) ) ) )
9 1 8 sylan2 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) = ( A .fn ( bra ` ( `' bra ` T ) ) ) )
10 bracnvbra 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( bra ` ( `' bra ` T ) ) = T )
11 10 oveq2d 
 |-  ( T e. ( LinFn i^i ContFn ) -> ( A .fn ( bra ` ( `' bra ` T ) ) ) = ( A .fn T ) )
12 11 adantl 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( A .fn ( bra ` ( `' bra ` T ) ) ) = ( A .fn T ) )
13 9 12 eqtrd 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) = ( A .fn T ) )
14 13 fveq2d 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( `' bra ` ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) ) = ( `' bra ` ( A .fn T ) ) )
15 hvmulcl 
 |-  ( ( ( * ` A ) e. CC /\ ( `' bra ` T ) e. ~H ) -> ( ( * ` A ) .h ( `' bra ` T ) ) e. ~H )
16 2 1 15 syl2an 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( ( * ` A ) .h ( `' bra ` T ) ) e. ~H )
17 cnvbrabra 
 |-  ( ( ( * ` A ) .h ( `' bra ` T ) ) e. ~H -> ( `' bra ` ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) ) = ( ( * ` A ) .h ( `' bra ` T ) ) )
18 16 17 syl 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( `' bra ` ( bra ` ( ( * ` A ) .h ( `' bra ` T ) ) ) ) = ( ( * ` A ) .h ( `' bra ` T ) ) )
19 14 18 eqtr3d 
 |-  ( ( A e. CC /\ T e. ( LinFn i^i ContFn ) ) -> ( `' bra ` ( A .fn T ) ) = ( ( * ` A ) .h ( `' bra ` T ) ) )