Metamath Proof Explorer

Theorem ghmfghm

Description: The function fulfilling the conditions of ghmgrp is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020)

Ref Expression
Hypotheses ghmabl.x âŠĒ 𝑋 = ( Base ‘ 𝐚 )
ghmabl.y âŠĒ 𝑌 = ( Base ‘ ðŧ )
ghmabl.p âŠĒ + = ( +g ‘ 𝐚 )
ghmabl.q âŠĒ âĻĢ = ( +g ‘ ðŧ )
ghmabl.f âŠĒ ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋 ) → ( ðđ ‘ ( ð‘Ĩ + ð‘Ķ ) ) = ( ( ðđ ‘ ð‘Ĩ ) âĻĢ ( ðđ ‘ ð‘Ķ ) ) )
ghmabl.1 âŠĒ ( 𝜑 → ðđ : 𝑋 –onto→ 𝑌 )
ghmfghm.3 âŠĒ ( 𝜑 → 𝐚 ∈ Grp )
Assertion ghmfghm ( 𝜑 → ðđ ∈ ( 𝐚 GrpHom ðŧ ) )

Proof

Step Hyp Ref Expression
1 ghmabl.x âŠĒ 𝑋 = ( Base ‘ 𝐚 )
2 ghmabl.y âŠĒ 𝑌 = ( Base ‘ ðŧ )
3 ghmabl.p âŠĒ + = ( +g ‘ 𝐚 )
4 ghmabl.q âŠĒ âĻĢ = ( +g ‘ ðŧ )
5 ghmabl.f âŠĒ ( ( 𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋 ) → ( ðđ ‘ ( ð‘Ĩ + ð‘Ķ ) ) = ( ( ðđ ‘ ð‘Ĩ ) âĻĢ ( ðđ ‘ ð‘Ķ ) ) )
6 ghmabl.1 âŠĒ ( 𝜑 → ðđ : 𝑋 –onto→ 𝑌 )
7 ghmfghm.3 âŠĒ ( 𝜑 → 𝐚 ∈ Grp )
8 5 1 2 3 4 6 7 ghmgrp âŠĒ ( 𝜑 → ðŧ ∈ Grp )
9 fof âŠĒ ( ðđ : 𝑋 –onto→ 𝑌 → ðđ : 𝑋 âŸķ 𝑌 )
10 6 9 syl âŠĒ ( 𝜑 → ðđ : 𝑋 âŸķ 𝑌 )
11 5 3expb âŠĒ ( ( 𝜑 ∧ ( ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋 ) ) → ( ðđ ‘ ( ð‘Ĩ + ð‘Ķ ) ) = ( ( ðđ ‘ ð‘Ĩ ) âĻĢ ( ðđ ‘ ð‘Ķ ) ) )
12 1 2 3 4 7 8 10 11 isghmd âŠĒ ( 𝜑 → ðđ ∈ ( 𝐚 GrpHom ðŧ ) )