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 âŠĒ ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋 ) → ( ðđ ‘ ( ð‘Ĩ + ð‘Ķ ) ) = ( ( ðđ ‘ ð‘Ĩ ) âĻĢ ( ðđ ‘ ð‘Ķ ) ) )
ghmgrp.x âŠĒ 𝑋 = ( Base ‘ 𝐚 )
ghmgrp.y âŠĒ 𝑌 = ( Base ‘ ðŧ )
ghmgrp.p âŠĒ + = ( +g ‘ 𝐚 )
ghmgrp.q âŠĒ âĻĢ = ( +g ‘ ðŧ )
ghmgrp.1 âŠĒ ( 𝜑 → ðđ : 𝑋 –onto→ 𝑌 )
mhmmnd.3 âŠĒ ( 𝜑 → 𝐚 ∈ Mnd )
mhmid.0 âŠĒ 0 = ( 0g ‘ 𝐚 )
Assertion mhmid ( 𝜑 → ( ðđ ‘ 0 ) = ( 0g ‘ ðŧ ) )

Proof

Step Hyp Ref Expression
1 ghmgrp.f âŠĒ ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋 ) → ( ðđ ‘ ( ð‘Ĩ + ð‘Ķ ) ) = ( ( ðđ ‘ ð‘Ĩ ) âĻĢ ( ðđ ‘ ð‘Ķ ) ) )
2 ghmgrp.x âŠĒ 𝑋 = ( Base ‘ 𝐚 )
3 ghmgrp.y âŠĒ 𝑌 = ( Base ‘ ðŧ )
4 ghmgrp.p âŠĒ + = ( +g ‘ 𝐚 )
5 ghmgrp.q âŠĒ âĻĢ = ( +g ‘ ðŧ )
6 ghmgrp.1 âŠĒ ( 𝜑 → ðđ : 𝑋 –onto→ 𝑌 )
7 mhmmnd.3 âŠĒ ( 𝜑 → 𝐚 ∈ Mnd )
8 mhmid.0 âŠĒ 0 = ( 0g ‘ 𝐚 )
9 eqid âŠĒ ( 0g ‘ ðŧ ) = ( 0g ‘ ðŧ )
10 fof âŠĒ ( ðđ : 𝑋 –onto→ 𝑌 → ðđ : 𝑋 âŸķ 𝑌 )
11 6 10 syl âŠĒ ( 𝜑 → ðđ : 𝑋 âŸķ 𝑌 )
12 2 8 mndidcl âŠĒ ( 𝐚 ∈ Mnd → 0 ∈ 𝑋 )
13 7 12 syl âŠĒ ( 𝜑 → 0 ∈ 𝑋 )
14 11 13 ffvelrnd âŠĒ ( 𝜑 → ( ðđ ‘ 0 ) ∈ 𝑌 )
15 simplll âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → 𝜑 )
16 15 1 syl3an1 âŠĒ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋 ) → ( ðđ ‘ ( ð‘Ĩ + ð‘Ķ ) ) = ( ( ðđ ‘ ð‘Ĩ ) âĻĢ ( ðđ ‘ ð‘Ķ ) ) )
17 7 ad3antrrr âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → 𝐚 ∈ Mnd )
18 17 12 syl âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → 0 ∈ 𝑋 )
19 simplr âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → 𝑖 ∈ 𝑋 )
20 16 18 19 mhmlem âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ðđ ‘ ( 0 + 𝑖 ) ) = ( ( ðđ ‘ 0 ) âĻĢ ( ðđ ‘ 𝑖 ) ) )
21 2 4 8 mndlid âŠĒ ( ( 𝐚 ∈ Mnd ∧ 𝑖 ∈ 𝑋 ) → ( 0 + 𝑖 ) = 𝑖 )
22 17 19 21 syl2anc âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( 0 + 𝑖 ) = 𝑖 )
23 22 fveq2d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ðđ ‘ ( 0 + 𝑖 ) ) = ( ðđ ‘ 𝑖 ) )
24 20 23 eqtr3d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ( ðđ ‘ 0 ) âĻĢ ( ðđ ‘ 𝑖 ) ) = ( ðđ ‘ 𝑖 ) )
25 simpr âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ðđ ‘ 𝑖 ) = 𝑎 )
26 25 oveq2d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ( ðđ ‘ 0 ) âĻĢ ( ðđ ‘ 𝑖 ) ) = ( ( ðđ ‘ 0 ) âĻĢ 𝑎 ) )
27 24 26 25 3eqtr3d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ( ðđ ‘ 0 ) âĻĢ 𝑎 ) = 𝑎 )
28 foelrni âŠĒ ( ( ðđ : 𝑋 –onto→ 𝑌 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑖 ∈ 𝑋 ( ðđ ‘ 𝑖 ) = 𝑎 )
29 6 28 sylan âŠĒ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑖 ∈ 𝑋 ( ðđ ‘ 𝑖 ) = 𝑎 )
30 27 29 r19.29a âŠĒ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ( ( ðđ ‘ 0 ) âĻĢ 𝑎 ) = 𝑎 )
31 16 19 18 mhmlem âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ðđ ‘ ( 𝑖 + 0 ) ) = ( ( ðđ ‘ 𝑖 ) âĻĢ ( ðđ ‘ 0 ) ) )
32 2 4 8 mndrid âŠĒ ( ( 𝐚 ∈ Mnd ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 + 0 ) = 𝑖 )
33 17 19 32 syl2anc âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( 𝑖 + 0 ) = 𝑖 )
34 33 fveq2d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ðđ ‘ ( 𝑖 + 0 ) ) = ( ðđ ‘ 𝑖 ) )
35 31 34 eqtr3d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ( ðđ ‘ 𝑖 ) âĻĢ ( ðđ ‘ 0 ) ) = ( ðđ ‘ 𝑖 ) )
36 25 oveq1d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( ( ðđ ‘ 𝑖 ) âĻĢ ( ðđ ‘ 0 ) ) = ( 𝑎 âĻĢ ( ðđ ‘ 0 ) ) )
37 35 36 25 3eqtr3d âŠĒ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( ðđ ‘ 𝑖 ) = 𝑎 ) → ( 𝑎 âĻĢ ( ðđ ‘ 0 ) ) = 𝑎 )
38 37 29 r19.29a âŠĒ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ( 𝑎 âĻĢ ( ðđ ‘ 0 ) ) = 𝑎 )
39 3 9 5 14 30 38 ismgmid2 âŠĒ ( 𝜑 → ( ðđ ‘ 0 ) = ( 0g ‘ ðŧ ) )