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⋅ihA=B⁢C⋅ihA
2 1 3comr ⊢A∈ℋ∧B∈ℂ∧C∈ℋ→B⋅ℎC⋅ihA=B⁢C⋅ihA
3 hvmulcl ⊢B∈ℂ∧C∈ℋ→B⋅ℎC∈ℋ
4 braval ⊢A∈ℋ∧B⋅ℎC∈ℋ→bra⁡A⁡B⋅ℎC=B⋅ℎC⋅ihA
5 3 4 sylan2 ⊢A∈ℋ∧B∈ℂ∧C∈ℋ→bra⁡A⁡B⋅ℎC=B⋅ℎC⋅ihA
6 5 3impb ⊢A∈ℋ∧B∈ℂ∧C∈ℋ→bra⁡A⁡B⋅ℎC=B⋅ℎC⋅ihA
7 braval ⊢A∈ℋ∧C∈ℋ→bra⁡A⁡C=C⋅ihA
8 7 3adant2 ⊢A∈ℋ∧B∈ℂ∧C∈ℋ→bra⁡A⁡C=C⋅ihA
9 8 oveq2d ⊢A∈ℋ∧B∈ℂ∧C∈ℋ→B⁢bra⁡A⁡C=B⁢C⋅ihA
10 2 6 9 3eqtr4d ⊢A∈ℋ∧B∈ℂ∧C∈ℋ→bra⁡A⁡B⋅ℎC=B⁢bra⁡A⁡C