Metamath Proof Explorer

Theorem bramul

Description: Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bramul ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → bra ⁡ A ⁡ B ⋅ ℎ C = B ⁢ bra ⁡ A ⁡ C

Proof

Step Hyp Ref Expression
1 ax-his3 ⊢ B ∈ ℂ ∧ C ∈ ℋ ∧ A ∈ ℋ → B ⋅ ℎ C ⋅ ih A = B ⁢ C ⋅ ih A
2 1 3comr ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → B ⋅ ℎ C ⋅ ih A = B ⁢ C ⋅ ih A
3 hvmulcl ⊢ B ∈ ℂ ∧ C ∈ ℋ → B ⋅ ℎ C ∈ ℋ
4 braval ⊢ A ∈ ℋ ∧ B ⋅ ℎ C ∈ ℋ → bra ⁡ A ⁡ B ⋅ ℎ C = B ⋅ ℎ C ⋅ ih A
5 3 4 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → bra ⁡ A ⁡ B ⋅ ℎ C = B ⋅ ℎ C ⋅ ih A
6 5 3impb ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → bra ⁡ A ⁡ B ⋅ ℎ C = B ⋅ ℎ C ⋅ ih A
7 braval ⊢ A ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ C = C ⋅ ih A
8 7 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → bra ⁡ A ⁡ C = C ⋅ ih A
9 8 oveq2d ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → B ⁢ bra ⁡ A ⁡ C = B ⁢ C ⋅ ih A
10 2 6 9 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℂ ∧ C ∈ ℋ → bra ⁡ A ⁡ B ⋅ ℎ C = B ⁢ bra ⁡ A ⁡ C