Theorem opifismgm

Description: A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020)

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

Proof

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