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

Definition df-lmhm 17083
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 17080 . 2  class LMHom
2 vs . . 3  setvar  s
3 vt . . 3  setvar  t
4 clmod 16928 . . 3  class  LMod
53cv 1368 . . . . . . . 8  class  t
6 csca 14233 . . . . . . . 8  class Scalar
75, 6cfv 5413 . . . . . . 7  class  (Scalar `  t )
8 vw . . . . . . . 8  setvar  w
98cv 1368 . . . . . . 7  class  w
107, 9wceq 1369 . . . . . 6  wff  (Scalar `  t )  =  w
11 vx . . . . . . . . . . . 12  setvar  x
1211cv 1368 . . . . . . . . . . 11  class  x
13 vy . . . . . . . . . . . 12  setvar  y
1413cv 1368 . . . . . . . . . . 11  class  y
152cv 1368 . . . . . . . . . . . 12  class  s
16 cvsca 14234 . . . . . . . . . . . 12  class  .s
1715, 16cfv 5413 . . . . . . . . . . 11  class  ( .s
`  s )
1812, 14, 17co 6086 . . . . . . . . . 10  class  ( x ( .s `  s
) y )
19 vf . . . . . . . . . . 11  setvar  f
2019cv 1368 . . . . . . . . . 10  class  f
2118, 20cfv 5413 . . . . . . . . 9  class  ( f `
 ( x ( .s `  s ) y ) )
2214, 20cfv 5413 . . . . . . . . . 10  class  ( f `
 y )
235, 16cfv 5413 . . . . . . . . . 10  class  ( .s
`  t )
2412, 22, 23co 6086 . . . . . . . . 9  class  ( x ( .s `  t
) ( f `  y ) )
2521, 24wceq 1369 . . . . . . . 8  wff  ( f `
 ( x ( .s `  s ) y ) )  =  ( x ( .s
`  t ) ( f `  y ) )
26 cbs 14166 . . . . . . . . 9  class  Base
2715, 26cfv 5413 . . . . . . . 8  class  ( Base `  s )
2825, 13, 27wral 2710 . . . . . . 7  wff  A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) )
299, 26cfv 5413 . . . . . . 7  class  ( Base `  w )
3028, 11, 29wral 2710 . . . . . 6  wff  A. x  e.  ( Base `  w
) A. y  e.  ( Base `  s
) ( f `  ( x ( .s
`  s ) y ) )  =  ( x ( .s `  t ) ( f `
 y ) )
3110, 30wa 369 . . . . 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 5413 . . . . 5  class  (Scalar `  s )
3331, 8, 32wsbc 3181 . . . 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 15735 . . . . 5  class  GrpHom
3515, 5, 34co 6086 . . . 4  class  ( s 
GrpHom  t )
3633, 19, 35crab 2714 . . 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 6088 . 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 1369 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 setvar class
This definition is referenced by:  reldmlmhm  17086  islmhm  17088
  Copyright terms: Public domain W3C validator