Metamath Proof Explorer

Theorem ismhm0

Description: Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020)

		Ref	Expression
	Hypotheses	ismhm0.b	\|- B = ( Base ` S )
		ismhm0.c	\|- C = ( Base ` T )
		ismhm0.p	\|- .+ = ( +g ` S )
		ismhm0.q	\|- .+^ = ( +g ` T )
		ismhm0.z	\|- .0. = ( 0g ` S )
		ismhm0.y	\|- Y = ( 0g ` T )
	Assertion	ismhm0	\|- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismhm0.b	\|- B = ( Base ` S )
2		ismhm0.c	\|- C = ( Base ` T )
3		ismhm0.p	\|- .+ = ( +g ` S )
4		ismhm0.q	\|- .+^ = ( +g ` T )
5		ismhm0.z	\|- .0. = ( 0g ` S )
6		ismhm0.y	\|- Y = ( 0g ` T )
7	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. ) = Y ) ) )
8		df-3an	\|- ( ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` .0. ) = Y ) <-> ( ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) /\ ( F ` .0. ) = Y ) )
9		mndmgm	\|- ( S e. Mnd -> S e. Mgm )
10		mndmgm	\|- ( T e. Mnd -> T e. Mgm )
11	9 10	anim12i	\|- ( ( S e. Mnd /\ T e. Mnd ) -> ( S e. Mgm /\ T e. Mgm ) )
12	11	biantrurd	\|- ( ( S e. Mnd /\ T e. Mnd ) -> ( ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) ) )
13	1 2 3 4	ismgmhm	\|- ( F e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : B --> C /\ A. x e. B A. y e. B ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) )
14	12 13	bitr4di	\|- ( ( 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 e. ( S MgmHom T ) ) )
15	14	anbi1d	\|- ( ( 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. ) = Y ) <-> ( F e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )
16	8 15	syl5bb	\|- ( ( 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. ) = Y ) <-> ( F e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )
17	16	pm5.32i	\|- ( ( ( 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. ) = Y ) ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )
18	7 17	bitri	\|- ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( F e. ( S MgmHom T ) /\ ( F ` .0. ) = Y ) ) )