Metamath Proof Explorer

Theorem his52

Description: Associative law for inner product. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion his52 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih A ‾ ⋅ ℎ C = A ⁢ B ⋅ ih C

Proof

Step Hyp Ref Expression
1 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
2 his5 ⊢ A ‾ ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih A ‾ ⋅ ℎ C = A ‾ ‾ ⁢ B ⋅ ih C
3 1 2 syl3an1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih A ‾ ⋅ ℎ C = A ‾ ‾ ⁢ B ⋅ ih C
4 cjcj ⊢ A ∈ ℂ → A ‾ ‾ = A
5 4 oveq1d ⊢ A ∈ ℂ → A ‾ ‾ ⁢ B ⋅ ih C = A ⁢ B ⋅ ih C
6 5 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ‾ ‾ ⁢ B ⋅ ih C = A ⁢ B ⋅ ih C
7 3 6 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih A ‾ ⋅ ℎ C = A ⁢ B ⋅ ih C