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	$$⊢\mathrm{LMHom}=\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{f\in \left(s\mathrm{GrpHom}t\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(s\right)/w\underset{\dot{}}{]}\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmhm	$$class\mathrm{LMHom}$$
1		vs	$$setvars$$
2		clmod	$$class\mathrm{LMod}$$
3		vt	$$setvart$$
4		vf	$$setvarf$$
5	1	cv	$$setvars$$
6		cghm	$$class\mathrm{GrpHom}$$
7	3	cv	$$setvart$$
8	5 7 6	co	$$class\left(s\mathrm{GrpHom}t\right)$$
9		csca	$$class\mathrm{Scalar}$$
10	5 9	cfv	$$class\mathrm{Scalar}\left(s\right)$$
11		vw	$$setvarw$$
12	7 9	cfv	$$class\mathrm{Scalar}\left(t\right)$$
13	11	cv	$$setvarw$$
14	12 13	wceq	$$wff\mathrm{Scalar}\left(t\right)=w$$
15		vx	$$setvarx$$
16		cbs	$$class\mathrm{Base}$$
17	13 16	cfv	$$class{\mathrm{Base}}_w$$
18		vy	$$setvary$$
19	5 16	cfv	$$class{\mathrm{Base}}_s$$
20	4	cv	$$setvarf$$
21	15	cv	$$setvarx$$
22		cvsca	$$class{\cdot }_{𝑠}$$
23	5 22	cfv	$$class{\cdot }_s$$
24	18	cv	$$setvary$$
25	21 24 23	co	$$class\left(x{\cdot }_{s}y\right)$$
26	25 20	cfv	$$classf\left(x{\cdot }_{s}y\right)$$
27	7 22	cfv	$$class{\cdot }_t$$
28	24 20	cfv	$$classf\left(y\right)$$
29	21 28 27	co	$$class\left(x{\cdot }_{t}f\left(y\right)\right)$$
30	26 29	wceq	$$wfff\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)$$
31	30 18 19	wral	$$wff\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)$$
32	31 15 17	wral	$$wff\forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)$$
33	14 32	wa	$$wff\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)$$
34	33 11 10	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(s\right)/w\underset{\dot{}}{]}\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)$$
35	34 4 8	crab	$$class\left\{f\in \left(s\mathrm{GrpHom}t\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(s\right)/w\underset{\dot{}}{]}\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)\right\}$$
36	1 3 2 2 35	cmpo	$$class\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{f\in \left(s\mathrm{GrpHom}t\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(s\right)/w\underset{\dot{}}{]}\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)\right\}\right)$$
37	0 36	wceq	$$wff\mathrm{LMHom}=\left(s\in \mathrm{LMod},t\in \mathrm{LMod}⟼\left\{f\in \left(s\mathrm{GrpHom}t\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(s\right)/w\underset{\dot{}}{]}\left(\mathrm{Scalar}\left(t\right)=w\wedge \forall x\in {\mathrm{Base}}_w\forall y\in {\mathrm{Base}}_{s}f\left(x{\cdot }_{s}y\right)=x{\cdot }_{t}f\left(y\right)\right)\right\}\right)$$