# 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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \left({A}+{B}\right){\cdot }_{ℎ}{C}=\left({A}{\cdot }_{ℎ}{C}\right){+}_{ℎ}\left({B}{\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 3 1 wcel ${wff}{B}\in ℂ$
5 cC ${class}{C}$
6 chba ${class}ℋ$
7 5 6 wcel ${wff}{C}\in ℋ$
8 2 4 7 w3a ${wff}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)$
9 caddc ${class}+$
10 0 3 9 co ${class}\left({A}+{B}\right)$
11 csm ${class}{\cdot }_{ℎ}$
12 10 5 11 co ${class}\left(\left({A}+{B}\right){\cdot }_{ℎ}{C}\right)$
13 0 5 11 co ${class}\left({A}{\cdot }_{ℎ}{C}\right)$
14 cva ${class}{+}_{ℎ}$
15 3 5 11 co ${class}\left({B}{\cdot }_{ℎ}{C}\right)$
16 13 15 14 co ${class}\left(\left({A}{\cdot }_{ℎ}{C}\right){+}_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)\right)$
17 12 16 wceq ${wff}\left({A}+{B}\right){\cdot }_{ℎ}{C}=\left({A}{\cdot }_{ℎ}{C}\right){+}_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)$
18 8 17 wi ${wff}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \left({A}+{B}\right){\cdot }_{ℎ}{C}=\left({A}{\cdot }_{ℎ}{C}\right){+}_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)\right)$