Metamath Proof Explorer

Axiom ax-his2

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 chba class ℋ
2 0 1 wcel wff A ∈ ℋ
3 cB class B
4 3 1 wcel wff B ∈ ℋ
5 cC class C
6 5 1 wcel wff C ∈ ℋ
7 2 4 6 w3a wff A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ
8 cva class + ℎ
9 0 3 8 co class A + ℎ B
10 csp class ⋅ ih
11 9 5 10 co class A + ℎ B ⋅ ih C
12 0 5 10 co class A ⋅ ih C
13 caddc class +
14 3 5 10 co class B ⋅ ih C
15 12 14 13 co class A ⋅ ih C + B ⋅ ih C
16 11 15 wceq wff A + ℎ B ⋅ ih C = A ⋅ ih C + B ⋅ ih C
17 7 16 wi wff A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B ⋅ ih C = A ⋅ ih C + B ⋅ ih C