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 ‾ · fn bra ⁡ B

Proof

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