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

Definition df-lmhm 18843
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
StepHypRef Expression
1 clmhm 18840 . 2 class LMHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 clmod 18686 . . 3 class LMod
53cv 1474 . . . . . . . 8 class 𝑡
6 csca 15771 . . . . . . . 8 class Scalar
75, 6cfv 5804 . . . . . . 7 class (Scalar‘𝑡)
8 vw . . . . . . . 8 setvar 𝑤
98cv 1474 . . . . . . 7 class 𝑤
107, 9wceq 1475 . . . . . 6 wff (Scalar‘𝑡) = 𝑤
11 vx . . . . . . . . . . . 12 setvar 𝑥
1211cv 1474 . . . . . . . . . . 11 class 𝑥
13 vy . . . . . . . . . . . 12 setvar 𝑦
1413cv 1474 . . . . . . . . . . 11 class 𝑦
152cv 1474 . . . . . . . . . . . 12 class 𝑠
16 cvsca 15772 . . . . . . . . . . . 12 class ·𝑠
1715, 16cfv 5804 . . . . . . . . . . 11 class ( ·𝑠𝑠)
1812, 14, 17co 6549 . . . . . . . . . 10 class (𝑥( ·𝑠𝑠)𝑦)
19 vf . . . . . . . . . . 11 setvar 𝑓
2019cv 1474 . . . . . . . . . 10 class 𝑓
2118, 20cfv 5804 . . . . . . . . 9 class (𝑓‘(𝑥( ·𝑠𝑠)𝑦))
2214, 20cfv 5804 . . . . . . . . . 10 class (𝑓𝑦)
235, 16cfv 5804 . . . . . . . . . 10 class ( ·𝑠𝑡)
2412, 22, 23co 6549 . . . . . . . . 9 class (𝑥( ·𝑠𝑡)(𝑓𝑦))
2521, 24wceq 1475 . . . . . . . 8 wff (𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦))
26 cbs 15695 . . . . . . . . 9 class Base
2715, 26cfv 5804 . . . . . . . 8 class (Base‘𝑠)
2825, 13, 27wral 2896 . . . . . . 7 wff 𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦))
299, 26cfv 5804 . . . . . . 7 class (Base‘𝑤)
3028, 11, 29wral 2896 . . . . . 6 wff 𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦))
3110, 30wa 383 . . . . 5 wff ((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦)))
3215, 6cfv 5804 . . . . 5 class (Scalar‘𝑠)
3331, 8, 32wsbc 3402 . . . 4 wff [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦)))
34 cghm 17480 . . . . 5 class GrpHom
3515, 5, 34co 6549 . . . 4 class (𝑠 GrpHom 𝑡)
3633, 19, 35crab 2900 . . 3 class {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦)))}
372, 3, 4, 4, 36cmpt2 6551 . 2 class (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦)))})
381, 37wceq 1475 1 wff LMHom = (𝑠 ∈ LMod, 𝑡 ∈ LMod ↦ {𝑓 ∈ (𝑠 GrpHom 𝑡) ∣ [(Scalar‘𝑠) / 𝑤]((Scalar‘𝑡) = 𝑤 ∧ ∀𝑥 ∈ (Base‘𝑤)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥( ·𝑠𝑠)𝑦)) = (𝑥( ·𝑠𝑡)(𝑓𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  reldmlmhm  18846  islmhm  18848
  Copyright terms: Public domain W3C validator