Metamath Proof Explorer

Theorem hiassdi

Description: Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hiassdi ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B + ℎ C ⋅ ih D = A ⁢ B ⋅ ih D + C ⋅ ih D

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
2 ax-his2 ⊢ A ⋅ ℎ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B + ℎ C ⋅ ih D = A ⋅ ℎ B ⋅ ih D + C ⋅ ih D
3 2 3expb ⊢ A ⋅ ℎ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B + ℎ C ⋅ ih D = A ⋅ ℎ B ⋅ ih D + C ⋅ ih D
4 1 3 sylan ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B + ℎ C ⋅ ih D = A ⋅ ℎ B ⋅ ih D + C ⋅ ih D
5 ax-his3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B ⋅ ih D = A ⁢ B ⋅ ih D
6 5 3expa ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B ⋅ ih D = A ⁢ B ⋅ ih D
7 6 adantrl ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B ⋅ ih D = A ⁢ B ⋅ ih D
8 7 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B ⋅ ih D + C ⋅ ih D = A ⁢ B ⋅ ih D + C ⋅ ih D
9 4 8 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A ⋅ ℎ B + ℎ C ⋅ ih D = A ⁢ B ⋅ ih D + C ⋅ ih D