Metamath Proof Explorer


Theorem tendospdi1

Description: Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)

Ref Expression
Hypotheses tendosp.h H = LHyp K
tendosp.t T = LTrn K W
tendosp.e E = TEndo K W
Assertion tendospdi1 K V W H U E F T G T U F G = U F U G

Proof

Step Hyp Ref Expression
1 tendosp.h H = LHyp K
2 tendosp.t T = LTrn K W
3 tendosp.e E = TEndo K W
4 simpll K V W H U E F T G T K V
5 simplr K V W H U E F T G T W H
6 simpr1 K V W H U E F T G T U E
7 simpr2 K V W H U E F T G T F T
8 simpr3 K V W H U E F T G T G T
9 1 2 3 tendovalco K V W H U E F T G T U F G = U F U G
10 4 5 6 7 8 9 syl32anc K V W H U E F T G T U F G = U F U G