Theorem ghmlin

Description: A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Hypotheses	ghmlin.x	$$⊢X={\mathrm{Base}}_S$$
	ghmlin.a	$$⊢\underset{\dot{}}{+}={+}_S$$
	ghmlin.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	ghmlin	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in X\wedge V\in X\right)\to F\left(U\underset{\dot{}}{+}V\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		ghmlin.x	$$⊢X={\mathrm{Base}}_S$$
2		ghmlin.a	$$⊢\underset{\dot{}}{+}={+}_S$$
3		ghmlin.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
4		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
5	1 4 2 3	isghm	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\wedge \left(F:X⟶{\mathrm{Base}}_T\wedge \forall a\in X\forall b\in XF\left(a\underset{\dot{}}{+}b\right)=F\left(a\right)\underset{\dot{}}{⨣}F\left(b\right)\right)\right)$$
6	5	simprbi	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \left(F:X⟶{\mathrm{Base}}_T\wedge \forall a\in X\forall b\in XF\left(a\underset{\dot{}}{+}b\right)=F\left(a\right)\underset{\dot{}}{⨣}F\left(b\right)\right)$$
7	6	simprd	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \forall a\in X\forall b\in XF\left(a\underset{\dot{}}{+}b\right)=F\left(a\right)\underset{\dot{}}{⨣}F\left(b\right)$$
8		fvoveq1	$$⊢a=U\to F\left(a\underset{\dot{}}{+}b\right)=F\left(U\underset{\dot{}}{+}b\right)$$
9		fveq2	$$⊢a=U\to F\left(a\right)=F\left(U\right)$$
10	9	oveq1d	$$⊢a=U\to F\left(a\right)\underset{\dot{}}{⨣}F\left(b\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(b\right)$$
11	8 10	eqeq12d	$$⊢a=U\to \left(F\left(a\underset{\dot{}}{+}b\right)=F\left(a\right)\underset{\dot{}}{⨣}F\left(b\right)\leftrightarrow F\left(U\underset{\dot{}}{+}b\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(b\right)\right)$$
12		oveq2	$$⊢b=V\to U\underset{\dot{}}{+}b=U\underset{\dot{}}{+}V$$
13	12	fveq2d	$$⊢b=V\to F\left(U\underset{\dot{}}{+}b\right)=F\left(U\underset{\dot{}}{+}V\right)$$
14		fveq2	$$⊢b=V\to F\left(b\right)=F\left(V\right)$$
15	14	oveq2d	$$⊢b=V\to F\left(U\right)\underset{\dot{}}{⨣}F\left(b\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(V\right)$$
16	13 15	eqeq12d	$$⊢b=V\to \left(F\left(U\underset{\dot{}}{+}b\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(b\right)\leftrightarrow F\left(U\underset{\dot{}}{+}V\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(V\right)\right)$$
17	11 16	rspc2v	$$⊢\left(U\in X\wedge V\in X\right)\to \left(\forall a\in X\forall b\in XF\left(a\underset{\dot{}}{+}b\right)=F\left(a\right)\underset{\dot{}}{⨣}F\left(b\right)\to F\left(U\underset{\dot{}}{+}V\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(V\right)\right)$$
18	7 17	mpan9	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \left(U\in X\wedge V\in X\right)\right)\to F\left(U\underset{\dot{}}{+}V\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(V\right)$$
19	18	3impb	$$⊢\left(F\in \left(S\mathrm{GrpHom}T\right)\wedge U\in X\wedge V\in X\right)\to F\left(U\underset{\dot{}}{+}V\right)=F\left(U\right)\underset{\dot{}}{⨣}F\left(V\right)$$