Metamath Proof Explorer


Theorem dvhfset

Description: The constructed full vector space H for a lattice K . (Contributed by NM, 17-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypothesis dvhset.h H = LHyp K
Assertion dvhfset K V DVecH K = w H Base ndx LTrn K w × TEndo K w + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h Scalar ndx EDRing K w ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f

Proof

Step Hyp Ref Expression
1 dvhset.h H = LHyp K
2 elex K V K V
3 fveq2 k = K LHyp k = LHyp K
4 3 1 eqtr4di k = K LHyp k = H
5 fveq2 k = K LTrn k = LTrn K
6 5 fveq1d k = K LTrn k w = LTrn K w
7 fveq2 k = K TEndo k = TEndo K
8 7 fveq1d k = K TEndo k w = TEndo K w
9 6 8 xpeq12d k = K LTrn k w × TEndo k w = LTrn K w × TEndo K w
10 9 opeq2d k = K Base ndx LTrn k w × TEndo k w = Base ndx LTrn K w × TEndo K w
11 6 mpteq1d k = K h LTrn k w 2 nd f h 2 nd g h = h LTrn K w 2 nd f h 2 nd g h
12 11 opeq2d k = K 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h = 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h
13 9 9 12 mpoeq123dv k = K f LTrn k w × TEndo k w , g LTrn k w × TEndo k w 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h = f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h
14 13 opeq2d k = K + ndx f LTrn k w × TEndo k w , g LTrn k w × TEndo k w 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h = + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h
15 fveq2 k = K EDRing k = EDRing K
16 15 fveq1d k = K EDRing k w = EDRing K w
17 16 opeq2d k = K Scalar ndx EDRing k w = Scalar ndx EDRing K w
18 10 14 17 tpeq123d k = K Base ndx LTrn k w × TEndo k w + ndx f LTrn k w × TEndo k w , g LTrn k w × TEndo k w 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h Scalar ndx EDRing k w = Base ndx LTrn K w × TEndo K w + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h Scalar ndx EDRing K w
19 eqidd k = K s 1 st f s 2 nd f = s 1 st f s 2 nd f
20 8 9 19 mpoeq123dv k = K s TEndo k w , f LTrn k w × TEndo k w s 1 st f s 2 nd f = s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f
21 20 opeq2d k = K ndx s TEndo k w , f LTrn k w × TEndo k w s 1 st f s 2 nd f = ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f
22 21 sneqd k = K ndx s TEndo k w , f LTrn k w × TEndo k w s 1 st f s 2 nd f = ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f
23 18 22 uneq12d k = K Base ndx LTrn k w × TEndo k w + ndx f LTrn k w × TEndo k w , g LTrn k w × TEndo k w 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h Scalar ndx EDRing k w ndx s TEndo k w , f LTrn k w × TEndo k w s 1 st f s 2 nd f = Base ndx LTrn K w × TEndo K w + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h Scalar ndx EDRing K w ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f
24 4 23 mpteq12dv k = K w LHyp k Base ndx LTrn k w × TEndo k w + ndx f LTrn k w × TEndo k w , g LTrn k w × TEndo k w 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h Scalar ndx EDRing k w ndx s TEndo k w , f LTrn k w × TEndo k w s 1 st f s 2 nd f = w H Base ndx LTrn K w × TEndo K w + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h Scalar ndx EDRing K w ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f
25 df-dvech DVecH = k V w LHyp k Base ndx LTrn k w × TEndo k w + ndx f LTrn k w × TEndo k w , g LTrn k w × TEndo k w 1 st f 1 st g h LTrn k w 2 nd f h 2 nd g h Scalar ndx EDRing k w ndx s TEndo k w , f LTrn k w × TEndo k w s 1 st f s 2 nd f
26 24 25 1 mptfvmpt K V DVecH K = w H Base ndx LTrn K w × TEndo K w + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h Scalar ndx EDRing K w ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f
27 2 26 syl K V DVecH K = w H Base ndx LTrn K w × TEndo K w + ndx f LTrn K w × TEndo K w , g LTrn K w × TEndo K w 1 st f 1 st g h LTrn K w 2 nd f h 2 nd g h Scalar ndx EDRing K w ndx s TEndo K w , f LTrn K w × TEndo K w s 1 st f s 2 nd f