Theorem hvdistr1 8857

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 8817	. 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 914	1 |- (A .h (B +h C)) = ((A .h B) +h (A .h C))

Syntax hints:   = wceq 954   e. wcel 956  (class class class)co 3954  CCcc 5212  H~chil 8727   +h cva 8728   .h csm 8729

This theorem is referenced by:  hvsubass 8861  hvsubsub4 8865  hvnegdi 8868  pjmul 9562  lnophmlem2 9880

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

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

Copyright terms: Public domain