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 ⋅ ih B ⋅ ℎ D = A ⁢ B ‾ ⁢ C ⋅ ih D

Proof

Step Hyp Ref Expression
1 his5 ⊢ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ D = B ‾ ⁢ C ⋅ ih D
2 1 3expb ⊢ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ D = B ‾ ⁢ C ⋅ ih D
3 2 adantll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih B ⋅ ℎ D = B ‾ ⁢ C ⋅ ih D
4 3 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⁢ C ⋅ ih B ⋅ ℎ D = A ⁢ B ‾ ⁢ C ⋅ ih D
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 ⋅ ih B ⋅ ℎ D = A ⁢ C ⋅ ih B ⋅ ℎ D
10 5 6 8 9 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ C ⋅ ih B ⋅ ℎ D = A ⁢ C ⋅ ih B ⋅ ℎ D
11 cjcl ⊢ B ∈ ℂ → B ‾ ∈ ℂ
12 11 ad2antlr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → B ‾ ∈ ℂ
13 hicl ⊢ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih D ∈ ℂ
14 13 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → C ⋅ ih D ∈ ℂ
15 5 12 14 mulassd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⁢ B ‾ ⁢ C ⋅ ih D = A ⁢ B ‾ ⁢ C ⋅ ih D
16 4 10 15 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ C ⋅ ih B ⋅ ℎ D = A ⁢ B ‾ ⁢ C ⋅ ih D