Metamath Proof Explorer


Theorem dvasca

Description: The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom W ). (Contributed by NM, 22-Jun-2014)

Ref Expression
Hypotheses dvasca.h H = LHyp K
dvasca.d D = EDRing K W
dvasca.u U = DVecA K W
dvasca.f F = Scalar U
Assertion dvasca K X W H F = D

Proof

Step Hyp Ref Expression
1 dvasca.h H = LHyp K
2 dvasca.d D = EDRing K W
3 dvasca.u U = DVecA K W
4 dvasca.f F = Scalar U
5 eqid LTrn K W = LTrn K W
6 eqid TEndo K W = TEndo K W
7 1 5 6 2 3 dvaset K X W H U = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx D ndx s TEndo K W , f LTrn K W s f
8 7 fveq2d K X W H Scalar U = Scalar Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx D ndx s TEndo K W , f LTrn K W s f
9 2 fvexi D V
10 eqid Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx D ndx s TEndo K W , f LTrn K W s f = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx D ndx s TEndo K W , f LTrn K W s f
11 10 lmodsca D V D = Scalar Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx D ndx s TEndo K W , f LTrn K W s f
12 9 11 ax-mp D = Scalar Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx D ndx s TEndo K W , f LTrn K W s f
13 8 4 12 3eqtr4g K X W H F = D