Theorem opmpoismgm

Description: A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020)

	Ref	Expression
Hypotheses	opmpoismgm.b	|- B = ( Base ` M )
	opmpoismgm.p	|- ( +g ` M ) = ( x e. B , y e. B |-> C )
	opmpoismgm.n	|- ( ph -> B =/= (/) )
	opmpoismgm.c	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )
Assertion	opmpoismgm	|- ( ph -> M e. Mgm )

Proof

Step	Hyp	Ref	Expression
1		opmpoismgm.b	|- B = ( Base ` M )
2		opmpoismgm.p	|- ( +g ` M ) = ( x e. B , y e. B |-> C )
3		opmpoismgm.n	|- ( ph -> B =/= (/) )
4		opmpoismgm.c	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. B )
5	4	ralrimivva	|- ( ph -> A. x e. B A. y e. B C e. B )
6	5	adantr	|- ( ( ph /\ ( a e. B /\ b e. B ) ) -> A. x e. B A. y e. B C e. B )
7		simprl	|- ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. B )
8		simprr	|- ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. B )
9		eqid	|- ( x e. B , y e. B |-> C ) = ( x e. B , y e. B |-> C )
10	9	ovmpoelrn	|- ( ( A. x e. B A. y e. B C e. B /\ a e. B /\ b e. B ) -> ( a ( x e. B , y e. B |-> C ) b ) e. B )
11	6 7 8 10	syl3anc	|- ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( x e. B , y e. B |-> C ) b ) e. B )
12	11	ralrimivva	|- ( ph -> A. a e. B A. b e. B ( a ( x e. B , y e. B |-> C ) b ) e. B )
13		n0	|- ( B =/= (/) <-> E. e e e. B )
14	2	eqcomi	|- ( x e. B , y e. B |-> C ) = ( +g ` M )
15	1 14	ismgmn0	|- ( e e. B -> ( M e. Mgm <-> A. a e. B A. b e. B ( a ( x e. B , y e. B |-> C ) b ) e. B ) )
16	15	exlimiv	|- ( E. e e e. B -> ( M e. Mgm <-> A. a e. B A. b e. B ( a ( x e. B , y e. B |-> C ) b ) e. B ) )
17	13 16	sylbi	|- ( B =/= (/) -> ( M e. Mgm <-> A. a e. B A. b e. B ( a ( x e. B , y e. B |-> C ) b ) e. B ) )
18	3 17	syl	|- ( ph -> ( M e. Mgm <-> A. a e. B A. b e. B ( a ( x e. B , y e. B |-> C ) b ) e. B ) )
19	12 18	mpbird	|- ( ph -> M e. Mgm )