# Metamath Proof Explorer

## Axiom ax-hvdistr1

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

Ref Expression
Assertion ax-hvdistr1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({B}{+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cc ${class}ℂ$
2 0 1 wcel ${wff}{A}\in ℂ$
3 cB ${class}{B}$
4 chba ${class}ℋ$
5 3 4 wcel ${wff}{B}\in ℋ$
6 cC ${class}{C}$
7 6 4 wcel ${wff}{C}\in ℋ$
8 2 5 7 w3a ${wff}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)$
9 csm ${class}{\cdot }_{ℎ}$
10 cva ${class}{+}_{ℎ}$
11 3 6 10 co ${class}\left({B}{+}_{ℎ}{C}\right)$
12 0 11 9 co ${class}\left({A}{\cdot }_{ℎ}\left({B}{+}_{ℎ}{C}\right)\right)$
13 0 3 9 co ${class}\left({A}{\cdot }_{ℎ}{B}\right)$
14 0 6 9 co ${class}\left({A}{\cdot }_{ℎ}{C}\right)$
15 13 14 10 co ${class}\left(\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)$
16 12 15 wceq ${wff}{A}{\cdot }_{ℎ}\left({B}{+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)$
17 8 16 wi ${wff}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({B}{+}_{ℎ}{C}\right)=\left({A}{\cdot }_{ℎ}{B}\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{C}\right)\right)$