This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mhmfmhm

Description: The function fulfilling the conditions of mhmmnd is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-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 )
Assertion mhmfmhm ( 𝜑 → 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) )

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 1 2 3 4 5 6 7 mhmmnd ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
9 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
10 6 9 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
11 1 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
12 11 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
13 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14 1 2 3 4 5 6 7 13 mhmid ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) )
15 10 12 14 3jca ⊢ ( 𝜑 → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) ) )
16 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
17 2 3 4 5 13 16 ismhm ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ↔ ( ( 𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) ) ) )
18 7 8 15 17 syl21anbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) )