Metamath Proof Explorer

Theorem imasgrpf1

Description: The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasgrpf1.u 
|- U = ( F "s R )
imasgrpf1.v 
|- V = ( Base ` R )
Assertion imasgrpf1 
|- ( ( F : V -1-1-> B /\ R e. Grp ) -> U e. Grp )

Proof

Step Hyp Ref Expression
1 imasgrpf1.u 
 |-  U = ( F "s R )
2 imasgrpf1.v 
 |-  V = ( Base ` R )
3 1 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> U = ( F "s R ) )
4 2 a1i 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> V = ( Base ` R ) )
5 eqidd 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> ( +g ` R ) = ( +g ` R ) )
6 f1f1orn 
 |-  ( F : V -1-1-> B -> F : V -1-1-onto-> ran F )
7 6 adantr 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> F : V -1-1-onto-> ran F )
8 f1ofo 
 |-  ( F : V -1-1-onto-> ran F -> F : V -onto-> ran F )
9 7 8 syl 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> F : V -onto-> ran F )
10 7 f1ocpbl 
 |-  ( ( ( F : V -1-1-> B /\ R e. Grp ) /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
11 simpr 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> R e. Grp )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 3 4 5 9 10 11 12 imasgrp 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> ( U e. Grp /\ ( F ` ( 0g ` R ) ) = ( 0g ` U ) ) )
14 13 simpld 
 |-  ( ( F : V -1-1-> B /\ R e. Grp ) -> U e. Grp )