This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )