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 )