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

Definition df-lmhm 16103
 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 Scalar Scalar
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-lmhm
StepHypRef Expression
1 clmhm 16100 . 2 LMHom
2 vs . . 3
3 vt . . 3
4 clmod 15955 . . 3
53cv 1652 . . . . . . . 8
6 csca 13537 . . . . . . . 8 Scalar
75, 6cfv 5457 . . . . . . 7 Scalar
8 vw . . . . . . . 8
98cv 1652 . . . . . . 7
107, 9wceq 1653 . . . . . 6 Scalar
11 vx . . . . . . . . . . . 12
1211cv 1652 . . . . . . . . . . 11
13 vy . . . . . . . . . . . 12
1413cv 1652 . . . . . . . . . . 11
152cv 1652 . . . . . . . . . . . 12
16 cvsca 13538 . . . . . . . . . . . 12
1715, 16cfv 5457 . . . . . . . . . . 11
1812, 14, 17co 6084 . . . . . . . . . 10
19 vf . . . . . . . . . . 11
2019cv 1652 . . . . . . . . . 10
2118, 20cfv 5457 . . . . . . . . 9
2214, 20cfv 5457 . . . . . . . . . 10
235, 16cfv 5457 . . . . . . . . . 10
2412, 22, 23co 6084 . . . . . . . . 9
2521, 24wceq 1653 . . . . . . . 8
26 cbs 13474 . . . . . . . . 9
2715, 26cfv 5457 . . . . . . . 8
2825, 13, 27wral 2707 . . . . . . 7
299, 26cfv 5457 . . . . . . 7
3028, 11, 29wral 2707 . . . . . 6
3110, 30wa 360 . . . . 5 Scalar
3215, 6cfv 5457 . . . . 5 Scalar
3331, 8, 32wsbc 3163 . . . 4 Scalar Scalar
34 cghm 15008 . . . . 5
3515, 5, 34co 6084 . . . 4
3633, 19, 35crab 2711 . . 3 Scalar Scalar
372, 3, 4, 4, 36cmpt2 6086 . 2 Scalar Scalar
381, 37wceq 1653 1 LMHom Scalar Scalar
 Colors of variables: wff set class This definition is referenced by:  reldmlmhm  16106  islmhm  16108
 Copyright terms: Public domain W3C validator