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∈ℂ∧B∈ℋ→bra⁡A⋅ℎB=A‾·fnbra⁡B

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢A∈ℂ∧B∈ℋ→A⋅ℎB∈ℋ
2 brafval ⊢A⋅ℎB∈ℋ→bra⁡A⋅ℎB=x∈ℋ⟼x⋅ihA⋅ℎB
3 1 2 syl ⊢A∈ℂ∧B∈ℋ→bra⁡A⋅ℎB=x∈ℋ⟼x⋅ihA⋅ℎB
4 cjcl ⊢A∈ℂ→A‾∈ℂ
5 brafn ⊢B∈ℋ→bra⁡B:ℋ⟶ℂ
6 hfmmval ⊢A‾∈ℂ∧bra⁡B:ℋ⟶ℂ→A‾·fnbra⁡B=x∈ℋ⟼A‾⁢bra⁡B⁡x
7 4 5 6 syl2an ⊢A∈ℂ∧B∈ℋ→A‾·fnbra⁡B=x∈ℋ⟼A‾⁢bra⁡B⁡x
8 his5 ⊢A∈ℂ∧x∈ℋ∧B∈ℋ→x⋅ihA⋅ℎB=A‾⁢x⋅ihB
9 8 3expa ⊢A∈ℂ∧x∈ℋ∧B∈ℋ→x⋅ihA⋅ℎB=A‾⁢x⋅ihB
10 9 an32s ⊢A∈ℂ∧B∈ℋ∧x∈ℋ→x⋅ihA⋅ℎB=A‾⁢x⋅ihB
11 braval ⊢B∈ℋ∧x∈ℋ→bra⁡B⁡x=x⋅ihB
12 11 adantll ⊢A∈ℂ∧B∈ℋ∧x∈ℋ→bra⁡B⁡x=x⋅ihB
13 12 oveq2d ⊢A∈ℂ∧B∈ℋ∧x∈ℋ→A‾⁢bra⁡B⁡x=A‾⁢x⋅ihB
14 10 13 eqtr4d ⊢A∈ℂ∧B∈ℋ∧x∈ℋ→x⋅ihA⋅ℎB=A‾⁢bra⁡B⁡x
15 14 mpteq2dva ⊢A∈ℂ∧B∈ℋ→x∈ℋ⟼x⋅ihA⋅ℎB=x∈ℋ⟼A‾⁢bra⁡B⁡x
16 7 15 eqtr4d ⊢A∈ℂ∧B∈ℋ→A‾·fnbra⁡B=x∈ℋ⟼x⋅ihA⋅ℎB
17 3 16 eqtr4d ⊢A∈ℂ∧B∈ℋ→bra⁡A⋅ℎB=A‾·fnbra⁡B