Theorem hvdistr1 8913

Description: Scalar multiplication distributive law.

Hypotheses

Ref	Expression
hvdistr1.1	|- A e. CC
hvdistr1.2	|- B e. H~
hvdistr1.3	|- C e. H~

Assertion

Ref	Expression
hvdistr1	|- (A .h (B +h C)) = ((A .h B) +h (A .h C))

Proof of Theorem hvdistr1

Step	Hyp	Ref	Expression
1		hvdistr1.1	. 2 |- A e. CC
2		hvdistr1.2	. 2 |- B e. H~
3		hvdistr1.3	. 2 |- C e. H~
4		ax-hvdistr1 8873	. 2 |- ((A e. CC /\ B e. H~ /\ C e. H~) -> (A .h (B +h C)) = ((A .h B) +h (A .h C)))
5	1, 2, 3, 4	mp3an 918	1 |- (A .h (B +h C)) = ((A .h B) +h (A .h C))

Syntax hints:   = wceq 958   e. wcel 960  (class class class)co 3969  CCcc 5244  H~chil 8783   +h cva 8784   .h csm 8785

This theorem is referenced by:  hvsubass 8917  hvsubsub4 8921  hvnegdi 8924  pjmul 9617  lnophmlem2 9937

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-hvdistr1 8873

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779

Copyright terms: Public domain