Metamath Proof Explorer


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 )