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

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 )