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

Definition df-dvech 31891
Description: Define constructed full vector space H. (Contributed by NM, 17-Oct-2013.)
Assertion
Ref Expression
df-dvech  |-  DVecH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( {
<. ( Base `  ndx ) ,  ( (
( LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. } ) ) )
Distinct variable group:    f, g, h, k, s, w

Detailed syntax breakdown of Definition df-dvech
StepHypRef Expression
1 cdvh 31890 . 2  class  DVecH
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1631 . . . . 5  class  k
6 clh 30795 . . . . 5  class  LHyp
75, 6cfv 5271 . . . 4  class  ( LHyp `  k )
8 cnx 13161 . . . . . . . 8  class  ndx
9 cbs 13164 . . . . . . . 8  class  Base
108, 9cfv 5271 . . . . . . 7  class  ( Base `  ndx )
114cv 1631 . . . . . . . . 9  class  w
12 cltrn 30912 . . . . . . . . . 10  class  LTrn
135, 12cfv 5271 . . . . . . . . 9  class  ( LTrn `  k )
1411, 13cfv 5271 . . . . . . . 8  class  ( (
LTrn `  k ) `  w )
15 ctendo 31563 . . . . . . . . . 10  class  TEndo
165, 15cfv 5271 . . . . . . . . 9  class  ( TEndo `  k )
1711, 16cfv 5271 . . . . . . . 8  class  ( (
TEndo `  k ) `  w )
1814, 17cxp 4703 . . . . . . 7  class  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)
1910, 18cop 3656 . . . . . 6  class  <. ( Base `  ndx ) ,  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) >.
20 cplusg 13224 . . . . . . . 8  class  +g
218, 20cfv 5271 . . . . . . 7  class  ( +g  ` 
ndx )
22 vf . . . . . . . 8  set  f
23 vg . . . . . . . 8  set  g
2422cv 1631 . . . . . . . . . . 11  class  f
25 c1st 6136 . . . . . . . . . . 11  class  1st
2624, 25cfv 5271 . . . . . . . . . 10  class  ( 1st `  f )
2723cv 1631 . . . . . . . . . . 11  class  g
2827, 25cfv 5271 . . . . . . . . . 10  class  ( 1st `  g )
2926, 28ccom 4709 . . . . . . . . 9  class  ( ( 1st `  f )  o.  ( 1st `  g
) )
30 vh . . . . . . . . . 10  set  h
3130cv 1631 . . . . . . . . . . . 12  class  h
32 c2nd 6137 . . . . . . . . . . . . 13  class  2nd
3324, 32cfv 5271 . . . . . . . . . . . 12  class  ( 2nd `  f )
3431, 33cfv 5271 . . . . . . . . . . 11  class  ( ( 2nd `  f ) `
 h )
3527, 32cfv 5271 . . . . . . . . . . . 12  class  ( 2nd `  g )
3631, 35cfv 5271 . . . . . . . . . . 11  class  ( ( 2nd `  g ) `
 h )
3734, 36ccom 4709 . . . . . . . . . 10  class  ( ( ( 2nd `  f
) `  h )  o.  ( ( 2nd `  g
) `  h )
)
3830, 14, 37cmpt 4093 . . . . . . . . 9  class  ( h  e.  ( ( LTrn `  k ) `  w
)  |->  ( ( ( 2nd `  f ) `
 h )  o.  ( ( 2nd `  g
) `  h )
) )
3929, 38cop 3656 . . . . . . . 8  class  <. (
( 1st `  f
)  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >.
4022, 23, 18, 18, 39cmpt2 5876 . . . . . . 7  class  ( f  e.  ( ( (
LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. )
4121, 40cop 3656 . . . . . 6  class  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
) ,  g  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) )  |->  <.
( ( 1st `  f
)  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >.
42 csca 13227 . . . . . . . 8  class Scalar
438, 42cfv 5271 . . . . . . 7  class  (Scalar `  ndx )
44 cedring 31564 . . . . . . . . 9  class  EDRing
455, 44cfv 5271 . . . . . . . 8  class  ( EDRing `  k )
4611, 45cfv 5271 . . . . . . 7  class  ( (
EDRing `  k ) `  w )
4743, 46cop 3656 . . . . . 6  class  <. (Scalar ` 
ndx ) ,  ( ( EDRing `  k ) `  w ) >.
4819, 41, 47ctp 3655 . . . . 5  class  { <. (
Base `  ndx ) ,  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k ) `  w ) >. }
49 cvsca 13228 . . . . . . . 8  class  .s
508, 49cfv 5271 . . . . . . 7  class  ( .s
`  ndx )
51 vs . . . . . . . 8  set  s
5251cv 1631 . . . . . . . . . 10  class  s
5326, 52cfv 5271 . . . . . . . . 9  class  ( s `
 ( 1st `  f
) )
5452, 33ccom 4709 . . . . . . . . 9  class  ( s  o.  ( 2nd `  f
) )
5553, 54cop 3656 . . . . . . . 8  class  <. (
s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f ) )
>.
5651, 22, 17, 18, 55cmpt2 5876 . . . . . . 7  class  ( s  e.  ( ( TEndo `  k ) `  w
) ,  f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) )  |->  <.
( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )
5750, 56cop 3656 . . . . . 6  class  <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k ) `  w ) ,  f  e.  ( ( (
LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) )  |->  <.
( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >.
5857csn 3653 . . . . 5  class  { <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. }
5948, 58cun 3163 . . . 4  class  ( {
<. ( Base `  ndx ) ,  ( (
( LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. } )
604, 7, 59cmpt 4093 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( { <. (
Base `  ndx ) ,  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. } ) )
612, 3, 60cmpt 4093 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( { <. (
Base `  ndx ) ,  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. } ) ) )
621, 61wceq 1632 1  wff  DVecH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( {
<. ( Base `  ndx ) ,  ( (
( LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) ) >. ,  <. ( +g  `  ndx ) ,  ( f  e.  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) ,  g  e.  ( ( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( ( 1st `  f )  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. ) >. ,  <. (Scalar `  ndx ) ,  ( ( EDRing `  k ) `  w ) >. }  u.  {
<. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. } ) ) )
Colors of variables: wff set class
This definition is referenced by:  dvhfset  31892
  Copyright terms: Public domain W3C validator