Metamath Proof Explorer

Theorem his35

Description: Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion his35 ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→A⋅ℎC⋅ihB⋅ℎD=A⁢B‾⁢C⋅ihD

Proof

Step Hyp Ref Expression
1 his5 ⊢B∈ℂ∧C∈ℋ∧D∈ℋ→C⋅ihB⋅ℎD=B‾⁢C⋅ihD
2 1 3expb ⊢B∈ℂ∧C∈ℋ∧D∈ℋ→C⋅ihB⋅ℎD=B‾⁢C⋅ihD
3 2 adantll ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→C⋅ihB⋅ℎD=B‾⁢C⋅ihD
4 3 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→A⁢C⋅ihB⋅ℎD=A⁢B‾⁢C⋅ihD
5 simpll ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→A∈ℂ
6 simprl ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→C∈ℋ
7 hvmulcl ⊢B∈ℂ∧D∈ℋ→B⋅ℎD∈ℋ
8 7 ad2ant2l ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→B⋅ℎD∈ℋ
9 ax-his3 ⊢A∈ℂ∧C∈ℋ∧B⋅ℎD∈ℋ→A⋅ℎC⋅ihB⋅ℎD=A⁢C⋅ihB⋅ℎD
10 5 6 8 9 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→A⋅ℎC⋅ihB⋅ℎD=A⁢C⋅ihB⋅ℎD
11 cjcl ⊢B∈ℂ→B‾∈ℂ
12 11 ad2antlr ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→B‾∈ℂ
13 hicl ⊢C∈ℋ∧D∈ℋ→C⋅ihD∈ℂ
14 13 adantl ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→C⋅ihD∈ℂ
15 5 12 14 mulassd ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→A⁢B‾⁢C⋅ihD=A⁢B‾⁢C⋅ihD
16 4 10 15 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℋ∧D∈ℋ→A⋅ℎC⋅ihB⋅ℎD=A⁢B‾⁢C⋅ihD