Metamath Proof Explorer

Definition df-lmhm

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)

Ref Expression
Assertion 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmhm 
 |-  LMHom
1 vs 
 |-  s
2 clmod 
 |-  LMod
3 vt 
 |-  t
4 vf 
 |-  f
5 1 cv 
 |-  s
6 cghm 
 |-  GrpHom
7 3 cv 
 |-  t
8 5 7 6 co 
 |-  ( s GrpHom t )
9 csca 
 |-  Scalar
10 5 9 cfv 
 |-  ( Scalar ` s )
11 vw 
 |-  w
12 7 9 cfv 
 |-  ( Scalar ` t )
13 11 cv 
 |-  w
14 12 13 wceq 
 |-  ( Scalar ` t ) = w
15 vx 
 |-  x
16 cbs 
 |-  Base
17 13 16 cfv 
 |-  ( Base ` w )
18 vy 
 |-  y
19 5 16 cfv 
 |-  ( Base ` s )
20 4 cv 
 |-  f
21 15 cv 
 |-  x
22 cvsca 
 |-  .s
23 5 22 cfv 
 |-  ( .s ` s )
24 18 cv 
 |-  y
25 21 24 23 co 
 |-  ( x ( .s ` s ) y )
26 25 20 cfv 
 |-  ( f ` ( x ( .s ` s ) y ) )
27 7 22 cfv 
 |-  ( .s ` t )
28 24 20 cfv 
 |-  ( f ` y )
29 21 28 27 co 
 |-  ( x ( .s ` t ) ( f ` y ) )
30 26 29 wceq 
 |-  ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) )
31 30 18 19 wral 
 |-  A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) )
32 31 15 17 wral 
 |-  A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) )
33 14 32 wa 
 |-  ( ( Scalar ` t ) = w /\ A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) ) )
34 33 11 10 wsbc 
 |-  [. ( 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 ) ) )
35 34 4 8 crab 
 |-  { 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 ) ) ) }
36 1 3 2 2 35 cmpo 
 |-  ( 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 ) ) ) } )
37 0 36 wceq 
 |-  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 ) ) ) } )