Metamath Proof Explorer

Theorem ghmgrp

Description: The image of a group G under a group homomorphism F is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator O in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f 
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
ghmgrp.x 
|- X = ( Base ` G )
ghmgrp.y 
|- Y = ( Base ` H )
ghmgrp.p 
|- .+ = ( +g ` G )
ghmgrp.q 
|- .+^ = ( +g ` H )
ghmgrp.1 
|- ( ph -> F : X -onto-> Y )
ghmgrp.3 
|- ( ph -> G e. Grp )
Assertion ghmgrp 
|- ( ph -> H e. Grp )

Proof

Step Hyp Ref Expression
1 ghmgrp.f 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
2 ghmgrp.x 
 |-  X = ( Base ` G )
3 ghmgrp.y 
 |-  Y = ( Base ` H )
4 ghmgrp.p 
 |-  .+ = ( +g ` G )
5 ghmgrp.q 
 |-  .+^ = ( +g ` H )
6 ghmgrp.1 
 |-  ( ph -> F : X -onto-> Y )
7 ghmgrp.3 
 |-  ( ph -> G e. Grp )
8 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
9 7 8 syl 
 |-  ( ph -> G e. Mnd )
10 1 2 3 4 5 6 9 mhmmnd 
 |-  ( ph -> H e. Mnd )
11 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
12 6 11 syl 
 |-  ( ph -> F : X --> Y )
13 12 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> F : X --> Y )
14 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> G e. Grp )
15 simplr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> i e. X )
16 eqid 
 |-  ( invg ` G ) = ( invg ` G )
17 2 16 grpinvcl 
 |-  ( ( G e. Grp /\ i e. X ) -> ( ( invg ` G ) ` i ) e. X )
18 14 15 17 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( invg ` G ) ` i ) e. X )
19 13 18 ffvelrnd 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( invg ` G ) ` i ) ) e. Y )
20 1 3adant1r 
 |-  ( ( ( ph /\ i e. X ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
21 7 17 sylan 
 |-  ( ( ph /\ i e. X ) -> ( ( invg ` G ) ` i ) e. X )
22 simpr 
 |-  ( ( ph /\ i e. X ) -> i e. X )
23 20 21 22 mhmlem 
 |-  ( ( ph /\ i e. X ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ ( F ` i ) ) )
24 23 ad4ant13 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ ( F ` i ) ) )
25 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
26 2 4 25 16 grplinv 
 |-  ( ( G e. Grp /\ i e. X ) -> ( ( ( invg ` G ) ` i ) .+ i ) = ( 0g ` G ) )
27 26 fveq2d 
 |-  ( ( G e. Grp /\ i e. X ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( F ` ( 0g ` G ) ) )
28 14 15 27 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( F ` ( 0g ` G ) ) )
29 1 2 3 4 5 6 9 25 mhmid 
 |-  ( ph -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) )
30 29 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( 0g ` G ) ) = ( 0g ` H ) )
31 28 30 eqtrd 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( ( ( invg ` G ) ` i ) .+ i ) ) = ( 0g ` H ) )
32 simpr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` i ) = a )
33 32 oveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( ( invg ` G ) ` i ) ) .+^ ( F ` i ) ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) )
34 24 31 33 3eqtr3rd 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) = ( 0g ` H ) )
35 oveq1 
 |-  ( f = ( F ` ( ( invg ` G ) ` i ) ) -> ( f .+^ a ) = ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) )
36 35 eqeq1d 
 |-  ( f = ( F ` ( ( invg ` G ) ` i ) ) -> ( ( f .+^ a ) = ( 0g ` H ) <-> ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) = ( 0g ` H ) ) )
37 36 rspcev 
 |-  ( ( ( F ` ( ( invg ` G ) ` i ) ) e. Y /\ ( ( F ` ( ( invg ` G ) ` i ) ) .+^ a ) = ( 0g ` H ) ) -> E. f e. Y ( f .+^ a ) = ( 0g ` H ) )
38 19 34 37 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> E. f e. Y ( f .+^ a ) = ( 0g ` H ) )
39 foelrni 
 |-  ( ( F : X -onto-> Y /\ a e. Y ) -> E. i e. X ( F ` i ) = a )
40 6 39 sylan 
 |-  ( ( ph /\ a e. Y ) -> E. i e. X ( F ` i ) = a )
41 38 40 r19.29a 
 |-  ( ( ph /\ a e. Y ) -> E. f e. Y ( f .+^ a ) = ( 0g ` H ) )
42 41 ralrimiva 
 |-  ( ph -> A. a e. Y E. f e. Y ( f .+^ a ) = ( 0g ` H ) )
43 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
44 3 5 43 isgrp 
 |-  ( H e. Grp <-> ( H e. Mnd /\ A. a e. Y E. f e. Y ( f .+^ a ) = ( 0g ` H ) ) )
45 10 42 44 sylanbrc 
 |-  ( ph -> H e. Grp )