Metamath Proof Explorer

Theorem grprida

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 grpinva.c 
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
grpinva.o 
|- ( ph -> O e. B )
grpinva.i 
|- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )
grpinva.a 
|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
grpinva.r 
|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )
Assertion grprida 
|- ( ( ph /\ x e. B ) -> ( x .+ O ) = x )

Proof

Step Hyp Ref Expression
1 grpinva.c 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
2 grpinva.o 
 |-  ( ph -> O e. B )
3 grpinva.i 
 |-  ( ( ph /\ x e. B ) -> ( O .+ x ) = x )
4 grpinva.a 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
5 grpinva.r 
 |-  ( ( 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 grpinva 
 |-  ( ( 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 )