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 ðŧ ) )