Metamath Proof Explorer


Definition df-dveca

Description: Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013)

Ref Expression
Assertion df-dveca DVecA = k V w LHyp k 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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdveca class DVecA
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp k
7 cbs class Base
8 cnx class ndx
9 8 7 cfv class Base ndx
10 cltrn class LTrn
11 5 10 cfv class LTrn k
12 3 cv setvar w
13 12 11 cfv class LTrn k w
14 9 13 cop class Base ndx LTrn k w
15 cplusg class + 𝑔
16 8 15 cfv class + ndx
17 vf setvar f
18 vg setvar g
19 17 cv setvar f
20 18 cv setvar g
21 19 20 ccom class f g
22 17 18 13 13 21 cmpo class f LTrn k w , g LTrn k w f g
23 16 22 cop class + ndx f LTrn k w , g LTrn k w f g
24 csca class Scalar
25 8 24 cfv class Scalar ndx
26 cedring class EDRing
27 5 26 cfv class EDRing k
28 12 27 cfv class EDRing k w
29 25 28 cop class Scalar ndx EDRing k w
30 14 23 29 ctp class Base ndx LTrn k w + ndx f LTrn k w , g LTrn k w f g Scalar ndx EDRing k w
31 cvsca class 𝑠
32 8 31 cfv class ndx
33 vs setvar s
34 ctendo class TEndo
35 5 34 cfv class TEndo k
36 12 35 cfv class TEndo k w
37 33 cv setvar s
38 19 37 cfv class s f
39 33 17 36 13 38 cmpo class s TEndo k w , f LTrn k w s f
40 32 39 cop class ndx s TEndo k w , f LTrn k w s f
41 40 csn class ndx s TEndo k w , f LTrn k w s f
42 30 41 cun class 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
43 3 6 42 cmpt class w LHyp k 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
44 1 2 43 cmpt class k V w LHyp k 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
45 0 44 wceq wff DVecA = k V w LHyp k 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