Definition df-lmhm 19022

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

Step	Hyp	Ref	Expression
1		clmhm 19019	. 2 class LMHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		clmod 18863	. . 3 class LMod
5	3	cv 1482	. . . . . . . 8 class t
6		csca 15944	. . . . . . . 8 class Scalar
7	5, 6	cfv 5888	. . . . . . 7 class (Scalar ` t )
8		vw	. . . . . . . 8 setvar w
9	8	cv 1482	. . . . . . 7 class w
10	7, 9	wceq 1483	. . . . . 6 wff (Scalar ` t ) = w
11		vx	. . . . . . . . . . . 12 setvar x
12	11	cv 1482	. . . . . . . . . . 11 class x
13		vy	. . . . . . . . . . . 12 setvar y
14	13	cv 1482	. . . . . . . . . . 11 class y
15	2	cv 1482	. . . . . . . . . . . 12 class s
16		cvsca 15945	. . . . . . . . . . . 12 class .s
17	15, 16	cfv 5888	. . . . . . . . . . 11 class ( .s ` s )
18	12, 14, 17	co 6650	. . . . . . . . . 10 class ( x ( .s ` s ) y )
19		vf	. . . . . . . . . . 11 setvar f
20	19	cv 1482	. . . . . . . . . 10 class f
21	18, 20	cfv 5888	. . . . . . . . 9 class ( f ` ( x ( .s ` s ) y ) )
22	14, 20	cfv 5888	. . . . . . . . . 10 class ( f ` y )
23	5, 16	cfv 5888	. . . . . . . . . 10 class ( .s ` t )
24	12, 22, 23	co 6650	. . . . . . . . 9 class ( x ( .s ` t ) ( f ` y ) )
25	21, 24	wceq 1483	. . . . . . . 8 wff ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) )
26		cbs 15857	. . . . . . . . 9 class Base
27	15, 26	cfv 5888	. . . . . . . 8 class ( Base ` s )
28	25, 13, 27	wral 2912	. . . . . . 7 wff A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) )
29	9, 26	cfv 5888	. . . . . . 7 class ( Base ` w )
30	28, 11, 29	wral 2912	. . . . . 6 wff A. x e. ( Base ` w ) A. y e. ( Base ` s ) ( f ` ( x ( .s ` s ) y ) ) = ( x ( .s ` t ) ( f ` y ) )
31	10, 30	wa 384	. . . . 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 ) ) )
32	15, 6	cfv 5888	. . . . 5 class (Scalar ` s )
33	31, 8, 32	wsbc 3435	. . . 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 17657	. . . . 5 class GrpHom
35	15, 5, 34	co 6650	. . . 4 class ( s GrpHom t )
36	33, 19, 35	crab 2916	. . 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 ) ) ) }
37	2, 3, 4, 4, 36	cmpt2 6652	. 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 ) ) ) } )
38	1, 37	wceq 1483	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 ) ) ) } )

This definition is referenced by:  reldmlmhm  19025  islmhm  19027