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

Definition df-dic 30642
Description: Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom 
w. The value is a one-dimensional subspace generated by the pair consisting of the  iota_ vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom  ( ( oc k )  w ) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.)
Assertion
Ref Expression
df-dic  |-  DIsoC  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( q  e.  { r  e.  ( Atoms `  k )  |  -.  r ( le
`  k ) w }  |->  { <. f ,  s >.  |  ( f  =  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
) } ) ) )
Distinct variable group:    w, k, q, r, f, s, g

Detailed syntax breakdown of Definition df-dic
StepHypRef Expression
1 cdic 30641 . 2  class  DIsoC
2 vk . . 3  set  k
3 cvv 2789 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 29452 . . . . 5  class  LHyp
75, 6cfv 5221 . . . 4  class  ( LHyp `  k )
8 vq . . . . 5  set  q
9 vr . . . . . . . . 9  set  r
109cv 1622 . . . . . . . 8  class  r
114cv 1622 . . . . . . . 8  class  w
12 cple 13211 . . . . . . . . 9  class  le
135, 12cfv 5221 . . . . . . . 8  class  ( le
`  k )
1410, 11, 13wbr 4024 . . . . . . 7  wff  r ( le `  k ) w
1514wn 3 . . . . . 6  wff  -.  r
( le `  k
) w
16 catm 28732 . . . . . . 7  class  Atoms
175, 16cfv 5221 . . . . . 6  class  ( Atoms `  k )
1815, 9, 17crab 2548 . . . . 5  class  { r  e.  ( Atoms `  k
)  |  -.  r
( le `  k
) w }
19 vf . . . . . . . . 9  set  f
2019cv 1622 . . . . . . . 8  class  f
21 coc 13212 . . . . . . . . . . . . . 14  class  oc
225, 21cfv 5221 . . . . . . . . . . . . 13  class  ( oc
`  k )
2311, 22cfv 5221 . . . . . . . . . . . 12  class  ( ( oc `  k ) `
 w )
24 vg . . . . . . . . . . . . 13  set  g
2524cv 1622 . . . . . . . . . . . 12  class  g
2623, 25cfv 5221 . . . . . . . . . . 11  class  ( g `
 ( ( oc
`  k ) `  w ) )
278cv 1622 . . . . . . . . . . 11  class  q
2826, 27wceq 1623 . . . . . . . . . 10  wff  ( g `
 ( ( oc
`  k ) `  w ) )  =  q
29 cltrn 29569 . . . . . . . . . . . 12  class  LTrn
305, 29cfv 5221 . . . . . . . . . . 11  class  ( LTrn `  k )
3111, 30cfv 5221 . . . . . . . . . 10  class  ( (
LTrn `  k ) `  w )
3228, 24, 31crio 6291 . . . . . . . . 9  class  ( iota_ g  e.  ( ( LTrn `  k ) `  w
) ( g `  ( ( oc `  k ) `  w
) )  =  q )
33 vs . . . . . . . . . 10  set  s
3433cv 1622 . . . . . . . . 9  class  s
3532, 34cfv 5221 . . . . . . . 8  class  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )
3620, 35wceq 1623 . . . . . . 7  wff  f  =  ( s `  ( iota_ g  e.  ( (
LTrn `  k ) `  w ) ( g `
 ( ( oc
`  k ) `  w ) )  =  q ) )
37 ctendo 30220 . . . . . . . . . 10  class  TEndo
385, 37cfv 5221 . . . . . . . . 9  class  ( TEndo `  k )
3911, 38cfv 5221 . . . . . . . 8  class  ( (
TEndo `  k ) `  w )
4034, 39wcel 1685 . . . . . . 7  wff  s  e.  ( ( TEndo `  k
) `  w )
4136, 40wa 358 . . . . . 6  wff  ( f  =  ( s `  ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
)
4241, 19, 33copab 4077 . . . . 5  class  { <. f ,  s >.  |  ( f  =  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
) }
438, 18, 42cmpt 4078 . . . 4  class  ( q  e.  { r  e.  ( Atoms `  k )  |  -.  r ( le
`  k ) w }  |->  { <. f ,  s >.  |  ( f  =  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
) } )
444, 7, 43cmpt 4078 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( q  e. 
{ r  e.  (
Atoms `  k )  |  -.  r ( le
`  k ) w }  |->  { <. f ,  s >.  |  ( f  =  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
) } ) )
452, 3, 44cmpt 4078 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( q  e. 
{ r  e.  (
Atoms `  k )  |  -.  r ( le
`  k ) w }  |->  { <. f ,  s >.  |  ( f  =  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
) } ) ) )
461, 45wceq 1623 1  wff  DIsoC  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( q  e.  { r  e.  ( Atoms `  k )  |  -.  r ( le
`  k ) w }  |->  { <. f ,  s >.  |  ( f  =  ( s `
 ( iota_ g  e.  ( ( LTrn `  k
) `  w )
( g `  (
( oc `  k
) `  w )
)  =  q ) )  /\  s  e.  ( ( TEndo `  k
) `  w )
) } ) ) )
Colors of variables: wff set class
This definition is referenced by:  dicffval  30643
  Copyright terms: Public domain W3C validator