Definition df-lmhm 20626

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 20623	. 2 class LMHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		clmod 20464	. . 3 class LMod
5	3	cv 1541	. . . . . . . 8 class 𝑡
6		csca 17197	. . . . . . . 8 class Scalar
7	5, 6	cfv 6541	. . . . . . 7 class (Scalar‘𝑡)
8		vw	. . . . . . . 8 setvar 𝑤
9	8	cv 1541	. . . . . . 7 class 𝑤
10	7, 9	wceq 1542	. . . . . 6 wff (Scalar‘𝑡) = 𝑤
11		vx	. . . . . . . . . . . 12 setvar 𝑥
12	11	cv 1541	. . . . . . . . . . 11 class 𝑥
13		vy	. . . . . . . . . . . 12 setvar 𝑦
14	13	cv 1541	. . . . . . . . . . 11 class 𝑦
15	2	cv 1541	. . . . . . . . . . . 12 class 𝑠
16		cvsca 17198	. . . . . . . . . . . 12 class ·𝑠
17	15, 16	cfv 6541	. . . . . . . . . . 11 class ( ·𝑠 ‘𝑠)
18	12, 14, 17	co 7406	. . . . . . . . . 10 class (𝑥( ·𝑠 ‘𝑠)𝑦)
19		vf	. . . . . . . . . . 11 setvar 𝑓
20	19	cv 1541	. . . . . . . . . 10 class 𝑓
21	18, 20	cfv 6541	. . . . . . . . 9 class (𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦))
22	14, 20	cfv 6541	. . . . . . . . . 10 class (𝑓‘𝑦)
23	5, 16	cfv 6541	. . . . . . . . . 10 class ( ·𝑠 ‘𝑡)
24	12, 22, 23	co 7406	. . . . . . . . 9 class (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
25	21, 24	wceq 1542	. . . . . . . 8 wff (𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
26		cbs 17141	. . . . . . . . 9 class Base
27	15, 26	cfv 6541	. . . . . . . 8 class (Base‘𝑠)
28	25, 13, 27	wral 3062	. . . . . . 7 wff ∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
29	9, 26	cfv 6541	. . . . . . 7 class (Base‘𝑤)
30	28, 11, 29	wral 3062	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦))
31	10, 30	wa 397	. . . . 5 wff ((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))
32	15, 6	cfv 6541	. . . . 5 class (Scalar‘𝑠)
33	31, 8, 32	wsbc 3777	. . . 4 wff [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))
34		cghm 19084	. . . . 5 class GrpHom
35	15, 5, 34	co 7406	. . . 4 class (𝑠 GrpHom 𝑡)
36	33, 19, 35	crab 3433	. . 3 class {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))}
37	2, 3, 4, 4, 36	cmpo 7408	. 2 class (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))})
38	1, 37	wceq 1542	1 wff LMHom = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠 ‘𝑠)𝑦)) = (𝑥( ·𝑠 ‘𝑡)(𝑓‘𝑦)))})

This definition is referenced by:  reldmlmhm  20629  islmhm  20631