Metamath Proof Explorer

Definition df-lmhm

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)

Ref Expression
Assertion df-lmhm ⊢ LMHom = s ∈ LMod , t ∈ LMod ⟼ f ∈ s GrpHom t | [˙ Scalar ⁡ s / w]˙ Scalar ⁡ t = w ∧ ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmhm class LMHom
1 vs setvar s
2 clmod class LMod
3 vt setvar t
4 vf setvar f
5 1 cv setvar s
6 cghm class GrpHom
7 3 cv setvar t
8 5 7 6 co class s GrpHom t
9 csca class Scalar
10 5 9 cfv class Scalar ⁡ s
11 vw setvar w
12 7 9 cfv class Scalar ⁡ t
13 11 cv setvar w
14 12 13 wceq wff Scalar ⁡ t = w
15 vx setvar x
16 cbs class Base
17 13 16 cfv class Base w
18 vy setvar y
19 5 16 cfv class Base s
20 4 cv setvar f
21 15 cv setvar x
22 cvsca class ⋅ 𝑠
23 5 22 cfv class ⋅ s
24 18 cv setvar y
25 21 24 23 co class x ⋅ s y
26 25 20 cfv class f ⁡ x ⋅ s y
27 7 22 cfv class ⋅ t
28 24 20 cfv class f ⁡ y
29 21 28 27 co class x ⋅ t f ⁡ y
30 26 29 wceq wff f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
31 30 18 19 wral wff ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
32 31 15 17 wral wff ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
33 14 32 wa wff Scalar ⁡ t = w ∧ ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
34 33 11 10 wsbc wff [˙ Scalar ⁡ s / w]˙ Scalar ⁡ t = w ∧ ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
35 34 4 8 crab class f ∈ s GrpHom t | [˙ Scalar ⁡ s / w]˙ Scalar ⁡ t = w ∧ ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
36 1 3 2 2 35 cmpo class s ∈ LMod , t ∈ LMod ⟼ f ∈ s GrpHom t | [˙ Scalar ⁡ s / w]˙ Scalar ⁡ t = w ∧ ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y
37 0 36 wceq wff LMHom = s ∈ LMod , t ∈ LMod ⟼ f ∈ s GrpHom t | [˙ Scalar ⁡ s / w]˙ Scalar ⁡ t = w ∧ ∀ x ∈ Base w ∀ y ∈ Base s f ⁡ x ⋅ s y = x ⋅ t f ⁡ y