Metamath Proof Explorer

Theorem ghomlinOLD

Description: Obsolete version of ghmlin as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis ghomlinOLD.1 
|- X = ran G
Assertion ghomlinOLD 
|- ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) H ( F ` B ) ) = ( F ` ( A G B ) ) )

Proof

Step Hyp Ref Expression
1 ghomlinOLD.1 
 |-  X = ran G
2 eqid 
 |-  ran H = ran H
3 1 2 elghomOLD 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : X --> ran H /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
4 3 biimp3a 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F : X --> ran H /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) )
5 4 simprd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) )
6 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
7 6 oveq1d 
 |-  ( x = A -> ( ( F ` x ) H ( F ` y ) ) = ( ( F ` A ) H ( F ` y ) ) )
8 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
9 8 fveq2d 
 |-  ( x = A -> ( F ` ( x G y ) ) = ( F ` ( A G y ) ) )
10 7 9 eqeq12d 
 |-  ( x = A -> ( ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) <-> ( ( F ` A ) H ( F ` y ) ) = ( F ` ( A G y ) ) ) )
11 fveq2 
 |-  ( y = B -> ( F ` y ) = ( F ` B ) )
12 11 oveq2d 
 |-  ( y = B -> ( ( F ` A ) H ( F ` y ) ) = ( ( F ` A ) H ( F ` B ) ) )
13 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
14 13 fveq2d 
 |-  ( y = B -> ( F ` ( A G y ) ) = ( F ` ( A G B ) ) )
15 12 14 eqeq12d 
 |-  ( y = B -> ( ( ( F ` A ) H ( F ` y ) ) = ( F ` ( A G y ) ) <-> ( ( F ` A ) H ( F ` B ) ) = ( F ` ( A G B ) ) ) )
16 10 15 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) -> ( ( F ` A ) H ( F ` B ) ) = ( F ` ( A G B ) ) ) )
17 5 16 mpan9 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) H ( F ` B ) ) = ( F ` ( A G B ) ) )