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 
|- X = ( Base ` S )
ghmlin.a 
|- .+ = ( +g ` S )
ghmlin.b 
|- .+^ = ( +g ` T )
Assertion ghmlin 
|- ( ( F e. ( S GrpHom T ) /\ U e. X /\ V e. X ) -> ( F ` ( U .+ V ) ) = ( ( F ` U ) .+^ ( F ` V ) ) )

Proof

Step Hyp Ref Expression
1 ghmlin.x 
 |-  X = ( Base ` S )
2 ghmlin.a 
 |-  .+ = ( +g ` S )
3 ghmlin.b 
 |-  .+^ = ( +g ` T )
4 eqid 
 |-  ( Base ` T ) = ( Base ` T )
5 1 4 2 3 isghm 
 |-  ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> ( Base ` T ) /\ A. a e. X A. b e. X ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) ) ) )
6 5 simprbi 
 |-  ( F e. ( S GrpHom T ) -> ( F : X --> ( Base ` T ) /\ A. a e. X A. b e. X ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) ) )
7 6 simprd 
 |-  ( F e. ( S GrpHom T ) -> A. a e. X A. b e. X ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) )
8 fvoveq1 
 |-  ( a = U -> ( F ` ( a .+ b ) ) = ( F ` ( U .+ b ) ) )
9 fveq2 
 |-  ( a = U -> ( F ` a ) = ( F ` U ) )
10 9 oveq1d 
 |-  ( a = U -> ( ( F ` a ) .+^ ( F ` b ) ) = ( ( F ` U ) .+^ ( F ` b ) ) )
11 8 10 eqeq12d 
 |-  ( a = U -> ( ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) <-> ( F ` ( U .+ b ) ) = ( ( F ` U ) .+^ ( F ` b ) ) ) )
12 oveq2 
 |-  ( b = V -> ( U .+ b ) = ( U .+ V ) )
13 12 fveq2d 
 |-  ( b = V -> ( F ` ( U .+ b ) ) = ( F ` ( U .+ V ) ) )
14 fveq2 
 |-  ( b = V -> ( F ` b ) = ( F ` V ) )
15 14 oveq2d 
 |-  ( b = V -> ( ( F ` U ) .+^ ( F ` b ) ) = ( ( F ` U ) .+^ ( F ` V ) ) )
16 13 15 eqeq12d 
 |-  ( b = V -> ( ( F ` ( U .+ b ) ) = ( ( F ` U ) .+^ ( F ` b ) ) <-> ( F ` ( U .+ V ) ) = ( ( F ` U ) .+^ ( F ` V ) ) ) )
17 11 16 rspc2v 
 |-  ( ( U e. X /\ V e. X ) -> ( A. a e. X A. b e. X ( F ` ( a .+ b ) ) = ( ( F ` a ) .+^ ( F ` b ) ) -> ( F ` ( U .+ V ) ) = ( ( F ` U ) .+^ ( F ` V ) ) ) )
18 7 17 mpan9 
 |-  ( ( F e. ( S GrpHom T ) /\ ( U e. X /\ V e. X ) ) -> ( F ` ( U .+ V ) ) = ( ( F ` U ) .+^ ( F ` V ) ) )
19 18 3impb 
 |-  ( ( F e. ( S GrpHom T ) /\ U e. X /\ V e. X ) -> ( F ` ( U .+ V ) ) = ( ( F ` U ) .+^ ( F ` V ) ) )