MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lmhm Unicode version

Definition df-lmhm 15779
Description: A homomorphism of left modules is a group homomorphism which additionally preserves the scalar product. This requires both structures to be left modules over the same ring. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Assertion
Ref Expression
df-lmhm  |- LMHom  =  ( s  e.  LMod ,  t  e.  LMod  |->  { f  e.  ( s  GrpHom  t )  |  [. (Scalar `  s )  /  w ]. ( (Scalar `  t
)  =  w  /\  A. x  e.  ( Base `  w ) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) ) ) } )
Distinct variable group:    f, s, t, w, x, y

Detailed syntax breakdown of Definition df-lmhm
StepHypRef Expression
1 clmhm 15776 . 2  class LMHom
2 vs . . 3  set  s
3 vt . . 3  set  t
4 clmod 15627 . . 3  class  LMod
53cv 1622 . . . . . . . 8  class  t
6 csca 13211 . . . . . . . 8  class Scalar
75, 6cfv 5255 . . . . . . 7  class  (Scalar `  t )
8 vw . . . . . . . 8  set  w
98cv 1622 . . . . . . 7  class  w
107, 9wceq 1623 . . . . . 6  wff  (Scalar `  t )  =  w
11 vx . . . . . . . . . . . 12  set  x
1211cv 1622 . . . . . . . . . . 11  class  x
13 vy . . . . . . . . . . . 12  set  y
1413cv 1622 . . . . . . . . . . 11  class  y
152cv 1622 . . . . . . . . . . . 12  class  s
16 cvsca 13212 . . . . . . . . . . . 12  class  .s
1715, 16cfv 5255 . . . . . . . . . . 11  class  ( .s
`  s )
1812, 14, 17co 5858 . . . . . . . . . 10  class  ( x ( .s `  s
) y )
19 vf . . . . . . . . . . 11  set  f
2019cv 1622 . . . . . . . . . 10  class  f
2118, 20cfv 5255 . . . . . . . . 9  class  ( f `
 ( x ( .s `  s ) y ) )
2214, 20cfv 5255 . . . . . . . . . 10  class  ( f `
 y )
235, 16cfv 5255 . . . . . . . . . 10  class  ( .s
`  t )
2412, 22, 23co 5858 . . . . . . . . 9  class  ( x ( .s `  t
) ( f `  y ) )
2521, 24wceq 1623 . . . . . . . 8  wff  ( f `
 ( x ( .s `  s ) y ) )  =  ( x ( .s
`  t ) ( f `  y ) )
26 cbs 13148 . . . . . . . . 9  class  Base
2715, 26cfv 5255 . . . . . . . 8  class  ( Base `  s )
2825, 13, 27wral 2543 . . . . . . 7  wff  A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) )
299, 26cfv 5255 . . . . . . 7  class  ( Base `  w )
3028, 11, 29wral 2543 . . . . . 6  wff  A. x  e.  ( Base `  w
) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) )
3110, 30wa 358 . . . . 5  wff  ( (Scalar `  t )  =  w  /\  A. x  e.  ( Base `  w
) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) ) )
3215, 6cfv 5255 . . . . 5  class  (Scalar `  s )
3331, 8, 32wsbc 2991 . . . 4  wff  [. (Scalar `  s )  /  w ]. ( (Scalar `  t
)  =  w  /\  A. x  e.  ( Base `  w ) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) ) )
34 cghm 14680 . . . . 5  class  GrpHom
3515, 5, 34co 5858 . . . 4  class  ( s 
GrpHom  t )
3633, 19, 35crab 2547 . . 3  class  { f  e.  ( s  GrpHom  t )  |  [. (Scalar `  s )  /  w ]. ( (Scalar `  t
)  =  w  /\  A. x  e.  ( Base `  w ) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) ) ) }
372, 3, 4, 4, 36cmpt2 5860 . 2  class  ( s  e.  LMod ,  t  e. 
LMod  |->  { f  e.  ( s  GrpHom  t )  |  [. (Scalar `  s )  /  w ]. ( (Scalar `  t
)  =  w  /\  A. x  e.  ( Base `  w ) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) ) ) } )
381, 37wceq 1623 1  wff LMHom  =  ( s  e.  LMod ,  t  e.  LMod  |->  { f  e.  ( s  GrpHom  t )  |  [. (Scalar `  s )  /  w ]. ( (Scalar `  t
)  =  w  /\  A. x  e.  ( Base `  w ) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  reldmlmhm  15782  islmhm  15784
  Copyright terms: Public domain W3C validator