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

Theorem dvhfset 31195
Description: The constructed full vector space H for a lattice  K. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
Hypothesis
Ref Expression
dvhset.h  |-  H  =  ( LHyp `  K
)
Assertion
Ref Expression
dvhfset  |-  ( K  e.  V  ->  ( DVecH `  K )  =  ( w  e.  H  |->  ( { <. ( 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 groups:    f, g, w, H    f, h, s, K, g, w
Allowed substitution hints:    H( h, s)    V( w, f, g, h, s)

Proof of Theorem dvhfset
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 elex 2907 . 2  |-  ( K  e.  V  ->  K  e.  _V )
2 fveq2 5668 . . . . 5  |-  ( k  =  K  ->  ( LHyp `  k )  =  ( LHyp `  K
) )
3 dvhset.h . . . . 5  |-  H  =  ( LHyp `  K
)
42, 3syl6eqr 2437 . . . 4  |-  ( k  =  K  ->  ( LHyp `  k )  =  H )
5 fveq2 5668 . . . . . . . . 9  |-  ( k  =  K  ->  ( LTrn `  k )  =  ( LTrn `  K
) )
65fveq1d 5670 . . . . . . . 8  |-  ( k  =  K  ->  (
( LTrn `  k ) `  w )  =  ( ( LTrn `  K
) `  w )
)
7 fveq2 5668 . . . . . . . . 9  |-  ( k  =  K  ->  ( TEndo `  k )  =  ( TEndo `  K )
)
87fveq1d 5670 . . . . . . . 8  |-  ( k  =  K  ->  (
( TEndo `  k ) `  w )  =  ( ( TEndo `  K ) `  w ) )
96, 8xpeq12d 4843 . . . . . . 7  |-  ( k  =  K  ->  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  =  ( ( ( LTrn `  K
) `  w )  X.  ( ( TEndo `  K
) `  w )
) )
109opeq2d 3933 . . . . . 6  |-  ( k  =  K  ->  <. ( Base `  ndx ) ,  ( ( ( LTrn `  k ) `  w
)  X.  ( (
TEndo `  k ) `  w ) ) >.  =  <. ( Base `  ndx ) ,  ( (
( LTrn `  K ) `  w )  X.  (
( TEndo `  K ) `  w ) ) >.
)
116mpteq1d 4231 . . . . . . . . 9  |-  ( k  =  K  ->  (
h  e.  ( (
LTrn `  k ) `  w )  |->  ( ( ( 2nd `  f
) `  h )  o.  ( ( 2nd `  g
) `  h )
) )  =  ( h  e.  ( (
LTrn `  K ) `  w )  |->  ( ( ( 2nd `  f
) `  h )  o.  ( ( 2nd `  g
) `  h )
) ) )
1211opeq2d 3933 . . . . . . . 8  |-  ( k  =  K  ->  <. (
( 1st `  f
)  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  k
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >.  =  <. ( ( 1st `  f
)  o.  ( 1st `  g ) ) ,  ( h  e.  ( ( LTrn `  K
) `  w )  |->  ( ( ( 2nd `  f ) `  h
)  o.  ( ( 2nd `  g ) `
 h ) ) ) >. )
139, 9, 12mpt2eq123dv 6075 . . . . . . 7  |-  ( k  =  K  ->  (
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 ) ) ) >. )  =  ( 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 ) ) ) >. ) )
1413opeq2d 3933 . . . . . 6  |-  ( k  =  K  ->  <. ( +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 ) ) ) >. ) >.  =  <. ( +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 ) ) ) >. ) >. )
15 fveq2 5668 . . . . . . . 8  |-  ( k  =  K  ->  ( EDRing `
 k )  =  ( EDRing `  K )
)
1615fveq1d 5670 . . . . . . 7  |-  ( k  =  K  ->  (
( EDRing `  k ) `  w )  =  ( ( EDRing `  K ) `  w ) )
1716opeq2d 3933 . . . . . 6  |-  ( k  =  K  ->  <. (Scalar ` 
ndx ) ,  ( ( EDRing `  k ) `  w ) >.  =  <. (Scalar `  ndx ) ,  ( ( EDRing `  K ) `  w ) >. )
1810, 14, 17tpeq123d 3841 . . . . 5  |-  ( k  =  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 ) >. }  =  { <. ( 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 ) >. } )
19 eqidd 2388 . . . . . . . 8  |-  ( k  =  K  ->  <. (
s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f ) )
>.  =  <. ( s `
 ( 1st `  f
) ) ,  ( s  o.  ( 2nd `  f ) ) >.
)
208, 9, 19mpt2eq123dv 6075 . . . . . . 7  |-  ( k  =  K  ->  (
s  e.  ( (
TEndo `  k ) `  w ) ,  f  e.  ( ( (
LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) )  |->  <.
( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )  =  ( s  e.  ( ( TEndo `  K
) `  w ) ,  f  e.  (
( ( LTrn `  K
) `  w )  X.  ( ( TEndo `  K
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. )
)
2120opeq2d 3933 . . . . . 6  |-  ( k  =  K  ->  <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k ) `  w ) ,  f  e.  ( ( (
LTrn `  k ) `  w )  X.  (
( TEndo `  k ) `  w ) )  |->  <.
( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >.  =  <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  K ) `  w
) ,  f  e.  ( ( ( LTrn `  K ) `  w
)  X.  ( (
TEndo `  K ) `  w ) )  |->  <.
( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. )
2221sneqd 3770 . . . . 5  |-  ( k  =  K  ->  { <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  k
) `  w ) ,  f  e.  (
( ( LTrn `  k
) `  w )  X.  ( ( TEndo `  k
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. }  =  { <. ( .s `  ndx ) ,  ( s  e.  ( ( TEndo `  K
) `  w ) ,  f  e.  (
( ( LTrn `  K
) `  w )  X.  ( ( TEndo `  K
) `  w )
)  |->  <. ( s `  ( 1st `  f ) ) ,  ( s  o.  ( 2nd `  f
) ) >. ) >. } )
2318, 22uneq12d 3445 . . . 4  |-  ( k  =  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
) ) >. ) >. } )  =  ( { <. ( 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
) ) >. ) >. } ) )
244, 23mpteq12dv 4228 . . 3  |-  ( k  =  K  ->  (
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
) ) >. ) >. } ) )  =  ( w  e.  H  |->  ( { <. ( 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
) ) >. ) >. } ) ) )
25 df-dvech 31194 . . 3  |-  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
) ) >. ) >. } ) ) )
26 fvex 5682 . . . . 5  |-  ( LHyp `  K )  e.  _V
273, 26eqeltri 2457 . . . 4  |-  H  e. 
_V
2827mptex 5905 . . 3  |-  ( w  e.  H  |->  ( {
<. ( 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
) ) >. ) >. } ) )  e. 
_V
2924, 25, 28fvmpt 5745 . 2  |-  ( K  e.  _V  ->  ( DVecH `  K )  =  ( w  e.  H  |->  ( { <. ( 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
) ) >. ) >. } ) ) )
301, 29syl 16 1  |-  ( K  e.  V  ->  ( DVecH `  K )  =  ( w  e.  H  |->  ( { <. ( 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
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   _Vcvv 2899    u. cun 3261   {csn 3757   {ctp 3759   <.cop 3760    e. cmpt 4207    X. cxp 4816    o. ccom 4822   ` cfv 5394    e. cmpt2 6022   1stc1st 6286   2ndc2nd 6287   ndxcnx 13393   Basecbs 13396   +g cplusg 13456  Scalarcsca 13459   .scvsca 13460   LHypclh 30098   LTrncltrn 30215   TEndoctendo 30866   EDRingcedring 30867   DVecHcdvh 31193
This theorem is referenced by:  dvhset  31196
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-oprab 6024  df-mpt2 6025  df-dvech 31194
  Copyright terms: Public domain W3C validator