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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 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 foelcdmi ⊢ ( ( 𝐹 : 𝑋 –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 ‘ 𝐻 ) )