Metamath Proof Explorer


Theorem grpridd

Description: Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013) (Proof shortened by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grprinvlem.c
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
grprinvlem.o
|- ( ph -> O e. B )
grprinvlem.i
|- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )
grprinvlem.a
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
grprinvlem.n
|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )
Assertion grpridd
|- ( ( ph /\ x e. B ) -> ( x .+ O ) = x )

Proof

Step Hyp Ref Expression
1 grprinvlem.c
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
2 grprinvlem.o
 |-  ( ph -> O e. B )
3 grprinvlem.i
 |-  ( ( ph /\ x e. B ) -> ( O .+ x ) = x )
4 grprinvlem.a
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
5 grprinvlem.n
 |-  ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )
6 oveq1
 |-  ( y = n -> ( y .+ x ) = ( n .+ x ) )
7 6 eqeq1d
 |-  ( y = n -> ( ( y .+ x ) = O <-> ( n .+ x ) = O ) )
8 7 cbvrexvw
 |-  ( E. y e. B ( y .+ x ) = O <-> E. n e. B ( n .+ x ) = O )
9 5 8 sylib
 |-  ( ( ph /\ x e. B ) -> E. n e. B ( n .+ x ) = O )
10 4 caovassg
 |-  ( ( ph /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
11 10 adantlr
 |-  ( ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
12 simprl
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> x e. B )
13 simprrl
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> n e. B )
14 11 12 13 12 caovassd
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( ( x .+ n ) .+ x ) = ( x .+ ( n .+ x ) ) )
15 simprrr
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( n .+ x ) = O )
16 1 2 3 4 5 12 13 15 grprinvd
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( x .+ n ) = O )
17 16 oveq1d
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( ( x .+ n ) .+ x ) = ( O .+ x ) )
18 15 oveq2d
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( x .+ ( n .+ x ) ) = ( x .+ O ) )
19 14 17 18 3eqtr3d
 |-  ( ( ph /\ ( x e. B /\ ( n e. B /\ ( n .+ x ) = O ) ) ) -> ( O .+ x ) = ( x .+ O ) )
20 19 anassrs
 |-  ( ( ( ph /\ x e. B ) /\ ( n e. B /\ ( n .+ x ) = O ) ) -> ( O .+ x ) = ( x .+ O ) )
21 9 20 rexlimddv
 |-  ( ( ph /\ x e. B ) -> ( O .+ x ) = ( x .+ O ) )
22 21 3 eqtr3d
 |-  ( ( ph /\ x e. B ) -> ( x .+ O ) = x )