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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( bra ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) ·fn ( bra ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ )
2 brafval ⊢ ( ( 𝐴 ·ℎ 𝐵 ) ∈ ℋ → ( bra ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( bra ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) )
4 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
5 brafn ⊢ ( 𝐵 ∈ ℋ → ( bra ‘ 𝐵 ) : ℋ ⟶ ℂ )
6 hfmmval ⊢ ( ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( bra ‘ 𝐵 ) : ℋ ⟶ ℂ ) → ( ( ∗ ‘ 𝐴 ) ·fn ( bra ‘ 𝐵 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ∗ ‘ 𝐴 ) · ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
7 4 5 6 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) ·fn ( bra ‘ 𝐵 ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ∗ ‘ 𝐴 ) · ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
8 his5 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝑥 ·ih 𝐵 ) ) )
9 8 3expa ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝑥 ·ih 𝐵 ) ) )
10 9 an32s ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝑥 ·ih 𝐵 ) ) )
11 braval ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝐵 ) )
12 11 adantll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) = ( 𝑥 ·ih 𝐵 ) )
13 12 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) · ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝑥 ·ih 𝐵 ) ) )
14 10 13 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) · ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) ) )
15 14 mpteq2dva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( ( ∗ ‘ 𝐴 ) · ( ( bra ‘ 𝐵 ) ‘ 𝑥 ) ) ) )
16 7 15 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( ∗ ‘ 𝐴 ) ·fn ( bra ‘ 𝐵 ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih ( 𝐴 ·ℎ 𝐵 ) ) ) )
17 3 16 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( bra ‘ ( 𝐴 ·ℎ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) ·fn ( bra ‘ 𝐵 ) ) )