Definition df-lmhm 21021

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 = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))})

Distinct variable group:   𝑓,𝑠,𝑡,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-lmhm

Step	Hyp	Ref	Expression
1		clmhm 21018	. 2 class LMHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		clmod 20858	. . 3 class LMod
5	3	cv 1539	. . . . . . . 8 class 𝑡
6		csca 17300	. . . . . . . 8 class Scalar
7	5, 6	cfv 6561	. . . . . . 7 class (Scalar‘𝑡)
8		vw	. . . . . . . 8 setvar 𝑤
9	8	cv 1539	. . . . . . 7 class 𝑤
10	7, 9	wceq 1540	. . . . . 6 wff (Scalar‘𝑡) = 𝑤
11		vx	. . . . . . . . . . . 12 setvar 𝑥
12	11	cv 1539	. . . . . . . . . . 11 class 𝑥
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1539	. . . . . . . . . . 11 class 𝑦
15	2	cv 1539	. . . . . . . . . . . 12 class 𝑠
16		cvsca 17301	. . . . . . . . . . . 12 class ·𝑠
17	15, 16	cfv 6561	. . . . . . . . . . 11 class ( ·𝑠 ‘𝑠)
18	12, 14, 17	co 7431	. . . . . . . . . 10 class (𝑥( ·𝑠 ‘𝑠)𝑦)
19		vf	. . . . . . . . . . 11 setvar 𝑓
20	19	cv 1539	. . . . . . . . . 10 class 𝑓
21	18, 20	cfv 6561	. . . . . . . . 9 class (𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦))
22	14, 20	cfv 6561	. . . . . . . . . 10 class (𝑓‘𝑦)
23	5, 16	cfv 6561	. . . . . . . . . 10 class ( ·𝑠 ‘𝑡)
24	12, 22, 23	co 7431	. . . . . . . . 9 class (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
25	21, 24	wceq 1540	. . . . . . . 8 wff (𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
26		cbs 17247	. . . . . . . . 9 class Base
27	15, 26	cfv 6561	. . . . . . . 8 class (Base‘𝑠)
28	25, 13, 27	wral 3061	. . . . . . 7 wff ∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
29	9, 26	cfv 6561	. . . . . . 7 class (Base‘𝑤)
30	28, 11, 29	wral 3061	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
31	10, 30	wa 395	. . . . 5 wff ((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))
32	15, 6	cfv 6561	. . . . 5 class (Scalar‘𝑠)
33	31, 8, 32	wsbc 3788	. . . 4 wff [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))
34		cghm 19230	. . . . 5 class GrpHom
35	15, 5, 34	co 7431	. . . 4 class (𝑠 GrpHom 𝑡)
36	33, 19, 35	crab 3436	. . 3 class {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))}
37	2, 3, 4, 4, 36	cmpo 7433	. 2 class (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))})
38	1, 37	wceq 1540	1 wff LMHom = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))})

This definition is referenced by:  reldmlmhm  21024  islmhm  21026