Metamath Proof Explorer


Theorem dvaabl

Description: The constructed partial vector space A for a lattice K is an abelian group. (Contributed by NM, 11-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses dvalvec.h H = LHyp K
dvalvec.v U = DVecA K W
Assertion dvaabl K HL W H U Abel

Proof

Step Hyp Ref Expression
1 dvalvec.h H = LHyp K
2 dvalvec.v U = DVecA K W
3 eqid LTrn K W = LTrn K W
4 eqid TEndo K W = TEndo K W
5 eqid EDRing K W = EDRing K W
6 1 3 4 5 2 dvaset K HL W H U = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
7 eqid TGrp K W = TGrp K W
8 1 3 7 tgrpset K HL W H TGrp K W = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
9 1 7 tgrpabl K HL W H TGrp K W Abel
10 8 9 eqeltrrd K HL W H Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Abel
11 fvex LTrn K W V
12 eqid Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g = Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
13 12 grpbase LTrn K W V LTrn K W = Base Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
14 eqid Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W 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 EDRing K W ndx s TEndo K W , f LTrn K W s f
15 14 lmodbase LTrn K W V LTrn K W = Base Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
16 13 15 eqtr3d LTrn K W V Base Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g = Base Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
17 11 16 ax-mp Base Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g = Base Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
18 11 11 mpoex f LTrn K W , g LTrn K W f g V
19 12 grpplusg f LTrn K W , g LTrn K W f g V f LTrn K W , g LTrn K W f g = + Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g
20 14 lmodplusg f LTrn K W , g LTrn K W f g V f LTrn K W , g LTrn K W f g = + Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
21 19 20 eqtr3d f LTrn K W , g LTrn K W f g V + Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g = + Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
22 18 21 ax-mp + Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g = + Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f
23 17 22 ablprop Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Abel Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f Abel
24 10 23 sylib K HL W H Base ndx LTrn K W + ndx f LTrn K W , g LTrn K W f g Scalar ndx EDRing K W ndx s TEndo K W , f LTrn K W s f Abel
25 6 24 eqeltrd K HL W H U Abel