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	|- .+ = ( +g ` S )
	ismhmd.q	|- .+^ = ( +g ` T )
	ismhmd.0	|- .0. = ( 0g ` S )
	ismhmd.z	|- Z = ( 0g ` T )
	ismhmd.s	|- ( ph -> S e. Mnd )
	ismhmd.t	|- ( ph -> T e. Mnd )
	ismhmd.f	|- ( ph -> F : B --> C )
	ismhmd.a	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
	ismhmd.h	|- ( ph -> ( F ` .0. ) = Z )
Assertion	ismhmd	|- ( ph -> F e. ( S MndHom T ) )

Proof

Step	Hyp	Ref	Expression
1		ismhmd.b	|- B = ( Base ` S )
2		ismhmd.c	|- C = ( Base ` T )
3		ismhmd.p	|- .+ = ( +g ` S )
4		ismhmd.q	|- .+^ = ( +g ` T )
5		ismhmd.0	|- .0. = ( 0g ` S )
6		ismhmd.z	|- Z = ( 0g ` T )
7		ismhmd.s	|- ( ph -> S e. Mnd )
8		ismhmd.t	|- ( ph -> T e. Mnd )
9		ismhmd.f	|- ( ph -> F : B --> C )
10		ismhmd.a	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
11		ismhmd.h	|- ( ph -> ( F ` .0. ) = Z )
12	10	ralrimivva	|- ( ph -> A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
13	9 12 11	3jca	|- ( ph -> ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Z ) )
14	1 2 3 4 5 6	ismhm	|- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Z ) ) )
15	7 8 13 14	syl21anbrc	|- ( ph -> F e. ( S MndHom T ) )