Theorem ghmlin

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

	Ref	Expression
Hypotheses	ghmlin.x	⊢ 𝑋 = ( Base ‘ 𝑆 )
	ghmlin.a	⊢ + = ( +g ‘ 𝑆 )
	ghmlin.b	⊢ ⨣ = ( +g ‘ 𝑇 )
Assertion	ghmlin	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ghmlin.x	⊢ 𝑋 = ( Base ‘ 𝑆 )
2		ghmlin.a	⊢ + = ( +g ‘ 𝑆 )
3		ghmlin.b	⊢ ⨣ = ( +g ‘ 𝑇 )
4		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
5	1 4 2 3	isghm	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) ) ) )
6	5	simprbi	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : 𝑋 ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) ) )
7	6	simprd	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) )
8		fvoveq1	⊢ ( 𝑎 = 𝑈 → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑈 + 𝑏 ) ) )
9		fveq2	⊢ ( 𝑎 = 𝑈 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑈 ) )
10	9	oveq1d	⊢ ( 𝑎 = 𝑈 → ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) )
11	8 10	eqeq12d	⊢ ( 𝑎 = 𝑈 → ( ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝐹 ‘ ( 𝑈 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) ) )
12		oveq2	⊢ ( 𝑏 = 𝑉 → ( 𝑈 + 𝑏 ) = ( 𝑈 + 𝑉 ) )
13	12	fveq2d	⊢ ( 𝑏 = 𝑉 → ( 𝐹 ‘ ( 𝑈 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) )
14		fveq2	⊢ ( 𝑏 = 𝑉 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑉 ) )
15	14	oveq2d	⊢ ( 𝑏 = 𝑉 → ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) )
16	13 15	eqeq12d	⊢ ( 𝑏 = 𝑉 → ( ( 𝐹 ‘ ( 𝑈 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) ↔ ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) ) )
17	11 16	rspc2v	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) ) )
18	7 17	mpan9	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) )
19	18	3impb	⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) )