Theorem lmhmlin

Description: A homomorphism of left modules is K -linear. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lmhmlin.k	$$⊢K=\mathrm{Scalar}\left(S\right)$$
	lmhmlin.b	$$⊢B={\mathrm{Base}}_K$$
	lmhmlin.e	$$⊢E={\mathrm{Base}}_S$$
	lmhmlin.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	lmhmlin.n	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
Assertion	lmhmlin	$$⊢\left(F\in \left(S\mathrm{LMHom}T\right)\wedge X\in B\wedge Y\in E\right)\to F\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{\times }F\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmhmlin.k	$$⊢K=\mathrm{Scalar}\left(S\right)$$
2		lmhmlin.b	$$⊢B={\mathrm{Base}}_K$$
3		lmhmlin.e	$$⊢E={\mathrm{Base}}_S$$
4		lmhmlin.m	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
5		lmhmlin.n	$$⊢\underset{\dot{}}{\times }={\cdot }_T$$
6		eqid	$$⊢\mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(T\right)$$
7	1 6 2 3 4 5	islmhm	$$⊢F\in \left(S\mathrm{LMHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{LMod}\wedge T\in \mathrm{LMod}\right)\wedge \left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \mathrm{Scalar}\left(T\right)=K\wedge \forall a\in B\forall b\in EF\left(a\underset{\dot{}}{·}b\right)=a\underset{\dot{}}{\times }F\left(b\right)\right)\right)$$
8	7	simprbi	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to \left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \mathrm{Scalar}\left(T\right)=K\wedge \forall a\in B\forall b\in EF\left(a\underset{\dot{}}{·}b\right)=a\underset{\dot{}}{\times }F\left(b\right)\right)$$
9	8	simp3d	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to \forall a\in B\forall b\in EF\left(a\underset{\dot{}}{·}b\right)=a\underset{\dot{}}{\times }F\left(b\right)$$
10		fvoveq1	$$⊢a=X\to F\left(a\underset{\dot{}}{·}b\right)=F\left(X\underset{\dot{}}{·}b\right)$$
11		oveq1	$$⊢a=X\to a\underset{\dot{}}{\times }F\left(b\right)=X\underset{\dot{}}{\times }F\left(b\right)$$
12	10 11	eqeq12d	$$⊢a=X\to \left(F\left(a\underset{\dot{}}{·}b\right)=a\underset{\dot{}}{\times }F\left(b\right)\leftrightarrow F\left(X\underset{\dot{}}{·}b\right)=X\underset{\dot{}}{\times }F\left(b\right)\right)$$
13		oveq2	$$⊢b=Y\to X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}Y$$
14	13	fveq2d	$$⊢b=Y\to F\left(X\underset{\dot{}}{·}b\right)=F\left(X\underset{\dot{}}{·}Y\right)$$
15		fveq2	$$⊢b=Y\to F\left(b\right)=F\left(Y\right)$$
16	15	oveq2d	$$⊢b=Y\to X\underset{\dot{}}{\times }F\left(b\right)=X\underset{\dot{}}{\times }F\left(Y\right)$$
17	14 16	eqeq12d	$$⊢b=Y\to \left(F\left(X\underset{\dot{}}{·}b\right)=X\underset{\dot{}}{\times }F\left(b\right)\leftrightarrow F\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{\times }F\left(Y\right)\right)$$
18	12 17	rspc2v	$$⊢\left(X\in B\wedge Y\in E\right)\to \left(\forall a\in B\forall b\in EF\left(a\underset{\dot{}}{·}b\right)=a\underset{\dot{}}{\times }F\left(b\right)\to F\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{\times }F\left(Y\right)\right)$$
19	9 18	syl5com	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to \left(\left(X\in B\wedge Y\in E\right)\to F\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{\times }F\left(Y\right)\right)$$
20	19	3impib	$$⊢\left(F\in \left(S\mathrm{LMHom}T\right)\wedge X\in B\wedge Y\in E\right)\to F\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{\times }F\left(Y\right)$$