# Metamath Proof Explorer

## Theorem grpoidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1
`|- X = ran G`
Assertion grpoidinv
`|- ( G e. GrpOp -> E. u e. X A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )`

### Proof

Step Hyp Ref Expression
1 grpfo.1
` |-  X = ran G`
2 simpl
` |-  ( ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> ( u G z ) = z )`
3 2 ralimi
` |-  ( A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> A. z e. X ( u G z ) = z )`
4 oveq2
` |-  ( z = x -> ( u G z ) = ( u G x ) )`
5 id
` |-  ( z = x -> z = x )`
6 4 5 eqeq12d
` |-  ( z = x -> ( ( u G z ) = z <-> ( u G x ) = x ) )`
7 6 rspccva
` |-  ( ( A. z e. X ( u G z ) = z /\ x e. X ) -> ( u G x ) = x )`
8 3 7 sylan
` |-  ( ( A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) /\ x e. X ) -> ( u G x ) = x )`
` |-  ( ( ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) /\ x e. X ) -> ( u G x ) = x )`
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( u G x ) = x )`
11 simpl
` |-  ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) -> G e. GrpOp )`
12 11 anim1i
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( G e. GrpOp /\ x e. X ) )`
13 id
` |-  ( ( G e. GrpOp /\ u e. X ) -> ( G e. GrpOp /\ u e. X ) )`
` |-  ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) -> ( G e. GrpOp /\ u e. X ) )`
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( G e. GrpOp /\ u e. X ) )`
` |-  ( ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) -> A. z e. X ( u G z ) = z )`
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> A. z e. X ( u G z ) = z )`
18 simpr
` |-  ( ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> E. w e. X ( w G z ) = u )`
19 18 ralimi
` |-  ( A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> A. z e. X E. w e. X ( w G z ) = u )`
` |-  ( ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) -> A. z e. X E. w e. X ( w G z ) = u )`
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> A. z e. X E. w e. X ( w G z ) = u )`
22 15 17 21 jca32
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( ( G e. GrpOp /\ u e. X ) /\ ( A. z e. X ( u G z ) = z /\ A. z e. X E. w e. X ( w G z ) = u ) ) )`
23 biid
` |-  ( A. z e. X ( u G z ) = z <-> A. z e. X ( u G z ) = z )`
24 biid
` |-  ( A. z e. X E. w e. X ( w G z ) = u <-> A. z e. X E. w e. X ( w G z ) = u )`
25 1 23 24 grpoidinvlem3
` |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ ( A. z e. X ( u G z ) = z /\ A. z e. X E. w e. X ( w G z ) = u ) ) /\ x e. X ) -> E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) )`
26 22 25 sylancom
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) )`
27 1 grpoidinvlem4
` |-  ( ( ( G e. GrpOp /\ x e. X ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> ( x G u ) = ( u G x ) )`
28 12 26 27 syl2anc
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( x G u ) = ( u G x ) )`
29 28 10 eqtrd
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( x G u ) = x )`
30 10 29 26 jca31
` |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )`
31 30 ralrimiva
` |-  ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) -> A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )`
32 1 grpolidinv
` |-  ( G e. GrpOp -> E. u e. X A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) )`
33 31 32 reximddv
` |-  ( G e. GrpOp -> E. u e. X A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )`