Metamath Proof Explorer

Theorem grprinvd

Description: Deduce right inverse 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 )
grprinvd.x 
|- ( ( ph /\ ps ) -> X e. B )
grprinvd.n 
|- ( ( ph /\ ps ) -> N e. B )
grprinvd.e 
|- ( ( ph /\ ps ) -> ( N .+ X ) = O )
Assertion grprinvd 
|- ( ( ph /\ ps ) -> ( X .+ N ) = O )

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 grprinvd.x 
 |-  ( ( ph /\ ps ) -> X e. B )
7 grprinvd.n 
 |-  ( ( ph /\ ps ) -> N e. B )
8 grprinvd.e 
 |-  ( ( ph /\ ps ) -> ( N .+ X ) = O )
9 1 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
10 9 caovclg 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u .+ v ) e. B )
11 10 adantlr 
 |-  ( ( ( ph /\ ps ) /\ ( u e. B /\ v e. B ) ) -> ( u .+ v ) e. B )
12 11 6 7 caovcld 
 |-  ( ( ph /\ ps ) -> ( X .+ N ) e. B )
13 4 caovassg 
 |-  ( ( ph /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
14 13 adantlr 
 |-  ( ( ( ph /\ ps ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .+ v ) .+ w ) = ( u .+ ( v .+ w ) ) )
15 14 6 7 12 caovassd 
 |-  ( ( ph /\ ps ) -> ( ( X .+ N ) .+ ( X .+ N ) ) = ( X .+ ( N .+ ( X .+ N ) ) ) )
16 8 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( N .+ X ) .+ N ) = ( O .+ N ) )
17 14 7 6 7 caovassd 
 |-  ( ( ph /\ ps ) -> ( ( N .+ X ) .+ N ) = ( N .+ ( X .+ N ) ) )
18 oveq2 
 |-  ( y = N -> ( O .+ y ) = ( O .+ N ) )
19 id 
 |-  ( y = N -> y = N )
20 18 19 eqeq12d 
 |-  ( y = N -> ( ( O .+ y ) = y <-> ( O .+ N ) = N ) )
21 3 ralrimiva 
 |-  ( ph -> A. x e. B ( O .+ x ) = x )
22 oveq2 
 |-  ( x = y -> ( O .+ x ) = ( O .+ y ) )
23 id 
 |-  ( x = y -> x = y )
24 22 23 eqeq12d 
 |-  ( x = y -> ( ( O .+ x ) = x <-> ( O .+ y ) = y ) )
25 24 cbvralvw 
 |-  ( A. x e. B ( O .+ x ) = x <-> A. y e. B ( O .+ y ) = y )
26 21 25 sylib 
 |-  ( ph -> A. y e. B ( O .+ y ) = y )
27 26 adantr 
 |-  ( ( ph /\ ps ) -> A. y e. B ( O .+ y ) = y )
28 20 27 7 rspcdva 
 |-  ( ( ph /\ ps ) -> ( O .+ N ) = N )
29 16 17 28 3eqtr3d 
 |-  ( ( ph /\ ps ) -> ( N .+ ( X .+ N ) ) = N )
30 29 oveq2d 
 |-  ( ( ph /\ ps ) -> ( X .+ ( N .+ ( X .+ N ) ) ) = ( X .+ N ) )
31 15 30 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( X .+ N ) .+ ( X .+ N ) ) = ( X .+ N ) )
32 1 2 3 4 5 12 31 grprinvlem 
 |-  ( ( ph /\ ps ) -> ( X .+ N ) = O )