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 ‘ 𝐵 ) ) )