Metamath Proof Explorer

Theorem grpinva

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 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 )
grpinva.x 
|- ( ( ph /\ ps ) -> X e. B )
grpinva.n 
|- ( ( ph /\ ps ) -> N e. B )
grpinva.e 
|- ( ( ph /\ ps ) -> ( N .+ X ) = O )
Assertion grpinva 
|- ( ( ph /\ ps ) -> ( X .+ N ) = O )

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 grpinva.x 
 |-  ( ( ph /\ ps ) -> X e. B )
7 grpinva.n 
 |-  ( ( ph /\ ps ) -> N e. B )
8 grpinva.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 grpinvalem 
 |-  ( ( ph /\ ps ) -> ( X .+ N ) = O )