This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑇 ) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑈 + 𝑉 ) ) = ( ( 𝐹 ‘ 𝑈 ) ⨣ ( 𝐹 ‘ 𝑉 ) ) )