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 ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ ( 𝐴 ·fn 𝑇 ) ) = ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 cnvbracl ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( ◡ bra ‘ 𝑇 ) ∈ ℋ )
2 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
3 brafnmul ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) → ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) )
4 2 3 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) → ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) )
5 cjcj ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
7 6 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) → ( ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) = ( 𝐴 ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) )
8 4 7 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) → ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) = ( 𝐴 ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) )
9 1 8 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) = ( 𝐴 ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) )
10 bracnvbra ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) = 𝑇 )
11 10 oveq2d ⊢ ( 𝑇 ∈ ( LinFn ∩ ContFn ) → ( 𝐴 ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) = ( 𝐴 ·fn 𝑇 ) )
12 11 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( 𝐴 ·fn ( bra ‘ ( ◡ bra ‘ 𝑇 ) ) ) = ( 𝐴 ·fn 𝑇 ) )
13 9 12 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) = ( 𝐴 ·fn 𝑇 ) )
14 13 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) ) = ( ◡ bra ‘ ( 𝐴 ·fn 𝑇 ) ) )
15 hvmulcl ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( ◡ bra ‘ 𝑇 ) ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ∈ ℋ )
16 2 1 15 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ∈ ℋ )
17 cnvbrabra ⊢ ( ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ∈ ℋ → ( ◡ bra ‘ ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) )
18 16 17 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ ( bra ‘ ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) )
19 14 18 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( LinFn ∩ ContFn ) ) → ( ◡ bra ‘ ( 𝐴 ·fn 𝑇 ) ) = ( ( ∗ ‘ 𝐴 ) ·ℎ ( ◡ bra ‘ 𝑇 ) ) )