Theorem ismgmd

Description: Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	ismgmd.b	|- ( ph -> B = ( Base ` G ) )
	ismgmd.0	|- ( ph -> G e. V )
	ismgmd.p	|- ( ph -> .+ = ( +g ` G ) )
	ismgmd.c	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
Assertion	ismgmd	|- ( ph -> G e. Mgm )

Proof

Step	Hyp	Ref	Expression
1		ismgmd.b	|- ( ph -> B = ( Base ` G ) )
2		ismgmd.0	|- ( ph -> G e. V )
3		ismgmd.p	|- ( ph -> .+ = ( +g ` G ) )
4		ismgmd.c	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
5	4	3expb	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
6	5	ralrimivva	|- ( ph -> A. x e. B A. y e. B ( x .+ y ) e. B )
7	3	oveqd	|- ( ph -> ( x .+ y ) = ( x ( +g ` G ) y ) )
8	7 1	eleq12d	|- ( ph -> ( ( x .+ y ) e. B <-> ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
9	1 8	raleqbidv	|- ( ph -> ( A. y e. B ( x .+ y ) e. B <-> A. y e. ( Base ` G ) ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
10	1 9	raleqbidv	|- ( ph -> ( A. x e. B A. y e. B ( x .+ y ) e. B <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
11	6 10	mpbid	|- ( ph -> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) e. ( Base ` G ) )
12		eqid	|- ( Base ` G ) = ( Base ` G )
13		eqid	|- ( +g ` G ) = ( +g ` G )
14	12 13	ismgm	|- ( G e. V -> ( G e. Mgm <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
15	2 14	syl	|- ( ph -> ( G e. Mgm <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( x ( +g ` G ) y ) e. ( Base ` G ) ) )
16	11 15	mpbird	|- ( ph -> G e. Mgm )