Metamath Proof Explorer

Theorem his7

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

Ref Expression
Assertion his7 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B + ℎ C = A ⋅ ih B + A ⋅ ih C

Proof

Step Hyp Ref Expression
1 ax-his2 ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B + ℎ C ⋅ ih A = B ⋅ ih A + C ⋅ ih A
2 1 fveq2d ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B + ℎ C ⋅ ih A ‾ = B ⋅ ih A + C ⋅ ih A ‾
3 hicl ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A ∈ ℂ
4 hicl ⊢ C ∈ ℋ ∧ A ∈ ℋ → C ⋅ ih A ∈ ℂ
5 cjadd ⊢ B ⋅ ih A ∈ ℂ ∧ C ⋅ ih A ∈ ℂ → B ⋅ ih A + C ⋅ ih A ‾ = B ⋅ ih A ‾ + C ⋅ ih A ‾
6 3 4 5 syl2an ⊢ B ∈ ℋ ∧ A ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A + C ⋅ ih A ‾ = B ⋅ ih A ‾ + C ⋅ ih A ‾
7 6 3impdir ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A + C ⋅ ih A ‾ = B ⋅ ih A ‾ + C ⋅ ih A ‾
8 2 7 eqtrd ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B + ℎ C ⋅ ih A ‾ = B ⋅ ih A ‾ + C ⋅ ih A ‾
9 8 3comr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → B + ℎ C ⋅ ih A ‾ = B ⋅ ih A ‾ + C ⋅ ih A ‾
10 hvaddcl ⊢ B ∈ ℋ ∧ C ∈ ℋ → B + ℎ C ∈ ℋ
11 ax-his1 ⊢ A ∈ ℋ ∧ B + ℎ C ∈ ℋ → A ⋅ ih B + ℎ C = B + ℎ C ⋅ ih A ‾
12 10 11 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B + ℎ C = B + ℎ C ⋅ ih A ‾
13 12 3impb ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B + ℎ C = B + ℎ C ⋅ ih A ‾
14 ax-his1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
15 14 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
16 ax-his1 ⊢ A ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih C = C ⋅ ih A ‾
17 16 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih C = C ⋅ ih A ‾
18 15 17 oveq12d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B + A ⋅ ih C = B ⋅ ih A ‾ + C ⋅ ih A ‾
19 9 13 18 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B + ℎ C = A ⋅ ih B + A ⋅ ih C