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 e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A + B ) .h C ) = ( ( A .h C ) +h ( B .h C ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cc 
 |-  CC
2 0 1 wcel 
 |-  A e. CC
3 cB 
 |-  B
4 3 1 wcel 
 |-  B e. CC
5 cC 
 |-  C
6 chba 
 |-  ~H
7 5 6 wcel 
 |-  C e. ~H
8 2 4 7 w3a 
 |-  ( A e. CC /\ B e. CC /\ C e. ~H )
9 caddc 
 |-  +
10 0 3 9 co 
 |-  ( A + B )
11 csm 
 |-  .h
12 10 5 11 co 
 |-  ( ( A + B ) .h C )
13 0 5 11 co 
 |-  ( A .h C )
14 cva 
 |-  +h
15 3 5 11 co 
 |-  ( B .h C )
16 13 15 14 co 
 |-  ( ( A .h C ) +h ( B .h C ) )
17 12 16 wceq 
 |-  ( ( A + B ) .h C ) = ( ( A .h C ) +h ( B .h C ) )
18 8 17 wi 
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A + B ) .h C ) = ( ( A .h C ) +h ( B .h C ) ) )