Metamath Proof Explorer

Theorem ghomidOLD

Description: Obsolete version of ghmid as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ghomidOLD.1 
|- U = ( GId ` G )
ghomidOLD.2 
|- T = ( GId ` H )
Assertion ghomidOLD 
|- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` U ) = T )

Proof

Step Hyp Ref Expression
1 ghomidOLD.1 
 |-  U = ( GId ` G )
2 ghomidOLD.2 
 |-  T = ( GId ` H )
3 eqid 
 |-  ran G = ran G
4 3 1 grpoidcl 
 |-  ( G e. GrpOp -> U e. ran G )
5 4 3ad2ant1 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> U e. ran G )
6 5 5 jca 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( U e. ran G /\ U e. ran G ) )
7 3 ghomlinOLD 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( U e. ran G /\ U e. ran G ) ) -> ( ( F ` U ) H ( F ` U ) ) = ( F ` ( U G U ) ) )
8 6 7 mpdan 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( ( F ` U ) H ( F ` U ) ) = ( F ` ( U G U ) ) )
9 3 1 grpolid 
 |-  ( ( G e. GrpOp /\ U e. ran G ) -> ( U G U ) = U )
10 4 9 mpdan 
 |-  ( G e. GrpOp -> ( U G U ) = U )
11 10 fveq2d 
 |-  ( G e. GrpOp -> ( F ` ( U G U ) ) = ( F ` U ) )
12 11 3ad2ant1 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` ( U G U ) ) = ( F ` U ) )
13 8 12 eqtrd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( ( F ` U ) H ( F ` U ) ) = ( F ` U ) )
14 eqid 
 |-  ran H = ran H
15 3 14 elghomOLD 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
16 15 biimp3a 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) )
17 16 simpld 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F : ran G --> ran H )
18 17 5 ffvelrnd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` U ) e. ran H )
19 14 2 grpoid 
 |-  ( ( H e. GrpOp /\ ( F ` U ) e. ran H ) -> ( ( F ` U ) = T <-> ( ( F ` U ) H ( F ` U ) ) = ( F ` U ) ) )
20 19 ex 
 |-  ( H e. GrpOp -> ( ( F ` U ) e. ran H -> ( ( F ` U ) = T <-> ( ( F ` U ) H ( F ` U ) ) = ( F ` U ) ) ) )
21 20 3ad2ant2 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( ( F ` U ) e. ran H -> ( ( F ` U ) = T <-> ( ( F ` U ) H ( F ` U ) ) = ( F ` U ) ) ) )
22 18 21 mpd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( ( F ` U ) = T <-> ( ( F ` U ) H ( F ` U ) ) = ( F ` U ) ) )
23 13 22 mpbird 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` U ) = T )