Metamath Proof Explorer

Theorem imasmnd

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

Ref Expression
Hypotheses imasmnd.u 
|- ( ph -> U = ( F "s R ) )
imasmnd.v 
|- ( ph -> V = ( Base ` R ) )
imasmnd.p 
|- .+ = ( +g ` R )
imasmnd.f 
|- ( ph -> F : V -onto-> B )
imasmnd.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 ) ) ) )
imasmnd.r 
|- ( ph -> R e. Mnd )
imasmnd.z 
|- .0. = ( 0g ` R )
Assertion imasmnd 
|- ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 imasmnd.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasmnd.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasmnd.p 
 |-  .+ = ( +g ` R )
4 imasmnd.f 
 |-  ( ph -> F : V -onto-> B )
5 imasmnd.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 imasmnd.r 
 |-  ( ph -> R e. Mnd )
7 imasmnd.z 
 |-  .0. = ( 0g ` R )
8 6 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> R e. Mnd )
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 14 3 mndcl 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x .+ y ) e. ( Base ` R ) )
16 8 11 13 15 syl3anc 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. ( Base ` R ) )
17 16 10 eleqtrrd 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
18 6 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> R e. Mnd )
19 11 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> x e. ( Base ` R ) )
20 13 3adant3r3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> y e. ( Base ` R ) )
21 simpr3 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z e. V )
22 2 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> V = ( Base ` R ) )
23 21 22 eleqtrd 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> z e. ( Base ` R ) )
24 14 3 mndass 
 |-  ( ( R e. Mnd /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
25 18 19 20 23 24 syl13anc 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
26 25 fveq2d 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( F ` ( ( x .+ y ) .+ z ) ) = ( F ` ( x .+ ( y .+ z ) ) ) )
27 14 7 mndidcl 
 |-  ( R e. Mnd -> .0. e. ( Base ` R ) )
28 6 27 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
29 28 2 eleqtrrd 
 |-  ( ph -> .0. e. V )
30 2 eleq2d 
 |-  ( ph -> ( x e. V <-> x e. ( Base ` R ) ) )
31 30 biimpa 
 |-  ( ( ph /\ x e. V ) -> x e. ( Base ` R ) )
32 14 3 7 mndlid 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) ) -> ( .0. .+ x ) = x )
33 6 31 32 syl2an2r 
 |-  ( ( ph /\ x e. V ) -> ( .0. .+ x ) = x )
34 33 fveq2d 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( .0. .+ x ) ) = ( F ` x ) )
35 14 3 7 mndrid 
 |-  ( ( R e. Mnd /\ x e. ( Base ` R ) ) -> ( x .+ .0. ) = x )
36 6 31 35 syl2an2r 
 |-  ( ( ph /\ x e. V ) -> ( x .+ .0. ) = x )
37 36 fveq2d 
 |-  ( ( ph /\ x e. V ) -> ( F ` ( x .+ .0. ) ) = ( F ` x ) )
38 1 2 3 4 5 6 17 26 29 34 37 imasmnd2 
 |-  ( ph -> ( U e. Mnd /\ ( F ` .0. ) = ( 0g ` U ) ) )