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 𝐻 ) )