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 dfgrp2e 
|- ( 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 syl6bi 
 |-  ( ( Base ` G ) = (/) -> ( n e. ( Base ` G ) -> G e. _V ) )
11 6 10 syl5bi 
 |-  ( ( 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 ) ) )