Metamath Proof Explorer

Theorem imasgrp

Description: The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses imasgrp.u 
|- ( ph -> U = ( F "s R ) )
imasgrp.v 
|- ( ph -> V = ( Base ` R ) )
imasgrp.p 
|- ( ph -> .+ = ( +g ` R ) )
imasgrp.f 
|- ( ph -> F : V -onto-> B )
imasgrp.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasgrp.r 
|- ( ph -> R e. Grp )
imasgrp.z 
|- .0. = ( 0g ` R )
Assertion imasgrp 
|- ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 imasgrp.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasgrp.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasgrp.p 
 |-  ( ph -> .+ = ( +g ` R ) )
4 imasgrp.f 
 |-  ( ph -> F : V -onto-> B )
5 imasgrp.e 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
6 imasgrp.r 
 |-  ( ph -> R e. Grp )
7 imasgrp.z 
 |-  .0. = ( 0g ` R )
8 6 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> R e. Grp )
9 simp2 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> x e. V )
10 2 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> V = ( Base ` R ) )
11 9 10 eleqtrd 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> x e. ( Base ` R ) )
12 simp3 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> y e. V )
13 12 10 eleqtrd 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> y e. ( Base ` R ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 eqid 
 |-  ( +g ` R ) = ( +g ` R )
16 14 15 grpcl 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
17 8 11 13 16 syl3anc 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
18 3 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> .+ = ( +g ` R ) )
19 18 oveqd 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) = ( x ( +g ` R ) y ) )
20 17 19 10 3eltr4d 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
21 6 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> R e. Grp )
22 11 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> x e. ( Base ` R ) )
23 13 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> y e. ( Base ` R ) )
24 simpr3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z e. V )
25 2 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> V = ( Base ` R ) )
26 24 25 eleqtrd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z e. ( Base ` R ) )
27 14 15 grpass 
 |-  ( ( R e. Grp /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) ( +g ` R ) z ) = ( x ( +g ` R ) ( y ( +g ` R ) z ) ) )
28 21 22 23 26 27 syl13anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x ( +g ` R ) y ) ( +g ` R ) z ) = ( x ( +g ` R ) ( y ( +g ` R ) z ) ) )
29 3 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> .+ = ( +g ` R ) )
30 19 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( x .+ y ) = ( x ( +g ` R ) y ) )
31 eqidd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z = z )
32 29 30 31 oveq123d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) = ( ( x ( +g ` R ) y ) ( +g ` R ) z ) )
33 eqidd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> x = x )
34 29 oveqd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( y .+ z ) = ( y ( +g ` R ) z ) )
35 29 33 34 oveq123d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( x .+ ( y .+ z ) ) = ( x ( +g ` R ) ( y ( +g ` R ) z ) ) )
36 28 32 35 3eqtr4d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
37 36 fveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )
38 14 7 grpidcl 
 |-  ( R e. Grp -> .0. e. ( Base ` R ) )
39 6 38 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
40 39 2 eleqtrrd 
 |-  ( ph -> .0. e. V )
41 3 adantr 
 |-  ( ( ph /\ x e. V ) -> .+ = ( +g ` R ) )
42 41 oveqd 
 |-  ( ( ph /\ x e. V ) -> ( .0. .+ x ) = ( .0. ( +g ` R ) x ) )
43 2 eleq2d 
 |-  ( ph -> ( x e. V <-> x e. ( Base ` R ) ) )
44 43 biimpa 
 |-  ( ( ph /\ x e. V ) -> x e. ( Base ` R ) )
45 14 15 7 grplid 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( .0. ( +g ` R ) x ) = x )
46 6 44 45 syl2an2r 
 |-  ( ( ph /\ x e. V ) -> ( .0. ( +g ` R ) x ) = x )
47 42 46 eqtrd 
 |-  ( ( ph /\ x e. V ) -> ( .0. .+ x ) = x )
48 47 fveq2d 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
49 eqid 
 |-  ( invg ` R ) = ( invg ` R )
50 14 49 grpinvcl 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( ( invg ` R ) ` x ) e. ( Base ` R ) )
51 6 44 50 syl2an2r 
 |-  ( ( ph /\ x e. V ) -> ( ( invg ` R ) ` x ) e. ( Base ` R ) )
52 2 adantr 
 |-  ( ( ph /\ x e. V ) -> V = ( Base ` R ) )
53 51 52 eleqtrrd 
 |-  ( ( ph /\ x e. V ) -> ( ( invg ` R ) ` x ) e. V )
54 41 oveqd 
 |-  ( ( ph /\ x e. V ) -> ( ( ( invg ` R ) ` x ) .+ x ) = ( ( ( invg ` R ) ` x ) ( +g ` R ) x ) )
55 14 15 7 49 grplinv 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( ( ( invg ` R ) ` x ) ( +g ` R ) x ) = .0. )
56 6 44 55 syl2an2r 
 |-  ( ( ph /\ x e. V ) -> ( ( ( invg ` R ) ` x ) ( +g ` R ) x ) = .0. )
57 54 56 eqtrd 
 |-  ( ( ph /\ x e. V ) -> ( ( ( invg ` R ) ` x ) .+ x ) = .0. )
58 57 fveq2d 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( ( ( invg ` R ) ` x ) .+ x ) ) = ( F ` .0. ) )
59 1 2 3 4 5 6 20 37 40 48 53 58 imasgrp2 
 |-  ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )