Metamath Proof Explorer

Theorem his5

Description: Associative law for inner product. Lemma 3.1(S5) of Beran p. 95. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
2 ax-his1 ⊢ B ∈ ℋ ∧ A ⋅ ℎ C ∈ ℋ → B ⋅ ih A ⋅ ℎ C = A ⋅ ℎ C ⋅ ih B ‾
3 1 2 sylan2 ⊢ B ∈ ℋ ∧ A ∈ ℂ ∧ C ∈ ℋ → B ⋅ ih A ⋅ ℎ C = A ⋅ ℎ C ⋅ ih B ‾
4 3 3impb ⊢ B ∈ ℋ ∧ A ∈ ℂ ∧ C ∈ ℋ → B ⋅ ih A ⋅ ℎ C = A ⋅ ℎ C ⋅ ih B ‾
5 4 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih A ⋅ ℎ C = A ⋅ ℎ C ⋅ ih B ‾
6 ax-his3 ⊢ A ∈ ℂ ∧ C ∈ ℋ ∧ B ∈ ℋ → A ⋅ ℎ C ⋅ ih B = A ⁢ C ⋅ ih B
7 6 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ C ⋅ ih B = A ⁢ C ⋅ ih B
8 7 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ C ⋅ ih B ‾ = A ⁢ C ⋅ ih B ‾
9 hicl ⊢ C ∈ ℋ ∧ B ∈ ℋ → C ⋅ ih B ∈ ℂ
10 cjmul ⊢ A ∈ ℂ ∧ C ⋅ ih B ∈ ℂ → A ⁢ C ⋅ ih B ‾ = A ‾ ⁢ C ⋅ ih B ‾
11 9 10 sylan2 ⊢ A ∈ ℂ ∧ C ∈ ℋ ∧ B ∈ ℋ → A ⁢ C ⋅ ih B ‾ = A ‾ ⁢ C ⋅ ih B ‾
12 11 3impb ⊢ A ∈ ℂ ∧ C ∈ ℋ ∧ B ∈ ℋ → A ⁢ C ⋅ ih B ‾ = A ‾ ⁢ C ⋅ ih B ‾
13 12 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⁢ C ⋅ ih B ‾ = A ‾ ⁢ C ⋅ ih B ‾
14 ax-his1 ⊢ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih C = C ⋅ ih B ‾
15 14 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih C = C ⋅ ih B ‾
16 15 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ‾ ⁢ B ⋅ ih C = A ‾ ⁢ C ⋅ ih B ‾
17 13 16 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⁢ C ⋅ ih B ‾ = A ‾ ⁢ B ⋅ ih C
18 5 8 17 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → B ⋅ ih A ⋅ ℎ C = A ‾ ⁢ B ⋅ ih C