Metamath Proof Explorer


Theorem ismhmd

Description: Deduction version of ismhm . (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses ismhmd.b B = Base S
ismhmd.c C = Base T
ismhmd.p + ˙ = + S
ismhmd.q ˙ = + T
ismhmd.0 0 ˙ = 0 S
ismhmd.z Z = 0 T
ismhmd.s φ S Mnd
ismhmd.t φ T Mnd
ismhmd.f φ F : B C
ismhmd.a φ x B y B F x + ˙ y = F x ˙ F y
ismhmd.h φ F 0 ˙ = Z
Assertion ismhmd φ F S MndHom T

Proof

Step Hyp Ref Expression
1 ismhmd.b B = Base S
2 ismhmd.c C = Base T
3 ismhmd.p + ˙ = + S
4 ismhmd.q ˙ = + T
5 ismhmd.0 0 ˙ = 0 S
6 ismhmd.z Z = 0 T
7 ismhmd.s φ S Mnd
8 ismhmd.t φ T Mnd
9 ismhmd.f φ F : B C
10 ismhmd.a φ x B y B F x + ˙ y = F x ˙ F y
11 ismhmd.h φ F 0 ˙ = Z
12 10 ralrimivva φ x B y B F x + ˙ y = F x ˙ F y
13 9 12 11 3jca φ F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Z
14 1 2 3 4 5 6 ismhm F S MndHom T S Mnd T Mnd F : B C x B y B F x + ˙ y = F x ˙ F y F 0 ˙ = Z
15 7 8 13 14 syl21anbrc φ F S MndHom T