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

Metamath Proof Explorer

Theorem dfgrp2e

Description: Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in Lang p. 7. (Contributed by NM, 10-Oct-2006) (Revised by AV, 28-Aug-2021)

Ref

Expression

Hypotheses

dfgrp2.b

|- B = ( Base ` G )

dfgrp2.p

|- .+ = ( +g ` G )

Assertion

|- ( G e. Grp <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfgrp2.b	\|- B = ( Base ` G )
2		dfgrp2.p	\|- .+ = ( +g ` G )
3	1 2	dfgrp2	\|- ( G e. Grp <-> ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
4		ax-1	\|- ( G e. _V -> ( n e. B -> G e. _V ) )
5		fvprc	\|- ( -. G e. _V -> ( Base ` G ) = (/) )
6	1	eleq2i	\|- ( n e. B <-> n e. ( Base ` G ) )
7		eleq2	\|- ( ( Base ` G ) = (/) -> ( n e. ( Base ` G ) <-> n e. (/) ) )
8		noel	\|- -. n e. (/)
9	8	pm2.21i	\|- ( n e. (/) -> G e. _V )
10	7 9	biimtrdi	\|- ( ( Base ` G ) = (/) -> ( n e. ( Base ` G ) -> G e. _V ) )
11	6 10	biimtrid	\|- ( ( Base ` G ) = (/) -> ( n e. B -> G e. _V ) )
12	5 11	syl	\|- ( -. G e. _V -> ( n e. B -> G e. _V ) )
13	4 12	pm2.61i	\|- ( n e. B -> G e. _V )
14	13	a1d	\|- ( n e. B -> ( A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> G e. _V ) )
15	14	rexlimiv	\|- ( E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> G e. _V )
16	1 2	issgrpv	\|- ( G e. _V -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) )
17	15 16	syl	\|- ( E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) -> ( G e. Smgrp <-> A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) ) )
18	17	pm5.32ri	\|- ( ( G e. Smgrp /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )
19	3 18	bitri	\|- ( G e. Grp <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. n e. B A. x e. B ( ( n .+ x ) = x /\ E. i e. B ( i .+ x ) = n ) ) )