Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dveca Unicode version

Definition df-dveca 31192
Description: Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.)
Assertion
Ref Expression
df-dveca  |-  DVecA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( {
<. ( Base `  ndx ) ,  ( ( LTrn `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. ,  <. (Scalar `  ndx ) ,  ( (
EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( LTrn `  k ) `  w )  |->  ( s `
 f ) )
>. } ) ) )
Distinct variable group:    w, k, s, f, g

Detailed syntax breakdown of Definition df-dveca
StepHypRef Expression
1 cdveca 31191 . 2  class  DVecA
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
8 cnx 13145 . . . . . . . 8  class  ndx
9 cbs 13148 . . . . . . . 8  class  Base
108, 9cfv 5255 . . . . . . 7  class  ( Base `  ndx )
114cv 1622 . . . . . . . 8  class  w
12 cltrn 30290 . . . . . . . . 9  class  LTrn
135, 12cfv 5255 . . . . . . . 8  class  ( LTrn `  k )
1411, 13cfv 5255 . . . . . . 7  class  ( (
LTrn `  k ) `  w )
1510, 14cop 3643 . . . . . 6  class  <. ( Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >.
16 cplusg 13208 . . . . . . . 8  class  +g
178, 16cfv 5255 . . . . . . 7  class  ( +g  ` 
ndx )
18 vf . . . . . . . 8  set  f
19 vg . . . . . . . 8  set  g
2018cv 1622 . . . . . . . . 9  class  f
2119cv 1622 . . . . . . . . 9  class  g
2220, 21ccom 4693 . . . . . . . 8  class  ( f  o.  g )
2318, 19, 14, 14, 22cmpt2 5860 . . . . . . 7  class  ( f  e.  ( ( LTrn `  k ) `  w
) ,  g  e.  ( ( LTrn `  k
) `  w )  |->  ( f  o.  g
) )
2417, 23cop 3643 . . . . . 6  class  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>.
25 csca 13211 . . . . . . . 8  class Scalar
268, 25cfv 5255 . . . . . . 7  class  (Scalar `  ndx )
27 cedring 30942 . . . . . . . . 9  class  EDRing
285, 27cfv 5255 . . . . . . . 8  class  ( EDRing `  k )
2911, 28cfv 5255 . . . . . . 7  class  ( (
EDRing `  k ) `  w )
3026, 29cop 3643 . . . . . 6  class  <. (Scalar ` 
ndx ) ,  ( ( EDRing `  k ) `  w ) >.
3115, 24, 30ctp 3642 . . . . 5  class  { <. (
Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. ,  <. (Scalar `  ndx ) ,  ( (
EDRing `  k ) `  w ) >. }
32 cvsca 13212 . . . . . . . 8  class  .s
338, 32cfv 5255 . . . . . . 7  class  ( .s
`  ndx )
34 vs . . . . . . . 8  set  s
35 ctendo 30941 . . . . . . . . . 10  class  TEndo
365, 35cfv 5255 . . . . . . . . 9  class  ( TEndo `  k )
3711, 36cfv 5255 . . . . . . . 8  class  ( (
TEndo `  k ) `  w )
3834cv 1622 . . . . . . . . 9  class  s
3920, 38cfv 5255 . . . . . . . 8  class  ( s `
 f )
4034, 18, 37, 14, 39cmpt2 5860 . . . . . . 7  class  ( s  e.  ( ( TEndo `  k ) `  w
) ,  f  e.  ( ( LTrn `  k
) `  w )  |->  ( s `  f
) )
4133, 40cop 3643 . . . . . 6  class  <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k ) `  w ) ,  f  e.  ( ( LTrn `  k ) `  w
)  |->  ( s `  f ) ) >.
4241csn 3640 . . . . 5  class  { <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( LTrn `  k ) `  w )  |->  ( s `
 f ) )
>. }
4331, 42cun 3150 . . . 4  class  ( {
<. ( Base `  ndx ) ,  ( ( LTrn `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. ,  <. (Scalar `  ndx ) ,  ( (
EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( LTrn `  k ) `  w )  |->  ( s `
 f ) )
>. } )
444, 7, 43cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( { <. (
Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. ,  <. (Scalar `  ndx ) ,  ( (
EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( LTrn `  k ) `  w )  |->  ( s `
 f ) )
>. } ) )
452, 3, 44cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( { <. (
Base `  ndx ) ,  ( ( LTrn `  k
) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. ,  <. (Scalar `  ndx ) ,  ( (
EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( LTrn `  k ) `  w )  |->  ( s `
 f ) )
>. } ) ) )
461, 45wceq 1623 1  wff  DVecA  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( {
<. ( Base `  ndx ) ,  ( ( LTrn `  k ) `  w ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( LTrn `  k
) `  w ) ,  g  e.  (
( LTrn `  k ) `  w )  |->  ( f  o.  g ) )
>. ,  <. (Scalar `  ndx ) ,  ( (
EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( LTrn `  k ) `  w )  |->  ( s `
 f ) )
>. } ) ) )
Colors of variables: wff set class
This definition is referenced by:  dvafset  31193
  Copyright terms: Public domain W3C validator