Metamath Proof Explorer

Axiom ax-hvdistr2

Description: Scalar multiplication distributive law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

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

Detailed syntax breakdown

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