Metamath Proof Explorer

Theorem mhmid

Description: A surjective monoid morphism preserves identity element. (Contributed 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 )
mhmmnd.3 
|- ( ph -> G e. Mnd )
mhmid.0 
|- .0. = ( 0g ` G )
Assertion mhmid 
|- ( ph -> ( F ` .0. ) = ( 0g ` H ) )

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 mhmmnd.3 
 |-  ( ph -> G e. Mnd )
8 mhmid.0 
 |-  .0. = ( 0g ` G )
9 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
10 fof 
 |-  ( F : X -onto-> Y -> F : X --> Y )
11 6 10 syl 
 |-  ( ph -> F : X --> Y )
12 2 8 mndidcl 
 |-  ( G e. Mnd -> .0. e. X )
13 7 12 syl 
 |-  ( ph -> .0. e. X )
14 11 13 ffvelcdmd 
 |-  ( ph -> ( F ` .0. ) e. Y )
15 simplll 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ph )
16 15 1 syl3an1 
 |-  ( ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
17 7 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> G e. Mnd )
18 17 12 syl 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> .0. e. X )
19 simplr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> i e. X )
20 16 18 19 mhmlem 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( .0. .+ i ) ) = ( ( F ` .0. ) .+^ ( F ` i ) ) )
21 2 4 8 mndlid 
 |-  ( ( G e. Mnd /\ i e. X ) -> ( .0. .+ i ) = i )
22 17 19 21 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( .0. .+ i ) = i )
23 22 fveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( .0. .+ i ) ) = ( F ` i ) )
24 20 23 eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` .0. ) .+^ ( F ` i ) ) = ( F ` i ) )
25 simpr 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` i ) = a )
26 25 oveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` .0. ) .+^ ( F ` i ) ) = ( ( F ` .0. ) .+^ a ) )
27 24 26 25 3eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` .0. ) .+^ a ) = a )
28 foelcdmi 
 |-  ( ( F : X -onto-> Y /\ a e. Y ) -> E. i e. X ( F ` i ) = a )
29 6 28 sylan 
 |-  ( ( ph /\ a e. Y ) -> E. i e. X ( F ` i ) = a )
30 27 29 r19.29a 
 |-  ( ( ph /\ a e. Y ) -> ( ( F ` .0. ) .+^ a ) = a )
31 16 19 18 mhmlem 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( i .+ .0. ) ) = ( ( F ` i ) .+^ ( F ` .0. ) ) )
32 2 4 8 mndrid 
 |-  ( ( G e. Mnd /\ i e. X ) -> ( i .+ .0. ) = i )
33 17 19 32 syl2anc 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( i .+ .0. ) = i )
34 33 fveq2d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( F ` ( i .+ .0. ) ) = ( F ` i ) )
35 31 34 eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` i ) .+^ ( F ` .0. ) ) = ( F ` i ) )
36 25 oveq1d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( ( F ` i ) .+^ ( F ` .0. ) ) = ( a .+^ ( F ` .0. ) ) )
37 35 36 25 3eqtr3d 
 |-  ( ( ( ( ph /\ a e. Y ) /\ i e. X ) /\ ( F ` i ) = a ) -> ( a .+^ ( F ` .0. ) ) = a )
38 37 29 r19.29a 
 |-  ( ( ph /\ a e. Y ) -> ( a .+^ ( F ` .0. ) ) = a )
39 3 9 5 14 30 38 ismgmid2 
 |-  ( ph -> ( F ` .0. ) = ( 0g ` H ) )