Theorem grplrinv

Description: In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021)

	Ref	Expression
Hypotheses	grplrinv.b	|- B = ( Base ` G )
	grplrinv.p	|- .+ = ( +g ` G )
	grplrinv.i	|- .0. = ( 0g ` G )
Assertion	grplrinv	|- ( G e. Grp -> A. x e. B E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		grplrinv.b	|- B = ( Base ` G )
2		grplrinv.p	|- .+ = ( +g ` G )
3		grplrinv.i	|- .0. = ( 0g ` G )
4		eqid	|- ( invg ` G ) = ( invg ` G )
5	1 4	grpinvcl	|- ( ( G e. Grp /\ x e. B ) -> ( ( invg ` G ) ` x ) e. B )
6		oveq1	|- ( y = ( ( invg ` G ) ` x ) -> ( y .+ x ) = ( ( ( invg ` G ) ` x ) .+ x ) )
7	6	eqeq1d	|- ( y = ( ( invg ` G ) ` x ) -> ( ( y .+ x ) = .0. <-> ( ( ( invg ` G ) ` x ) .+ x ) = .0. ) )
8		oveq2	|- ( y = ( ( invg ` G ) ` x ) -> ( x .+ y ) = ( x .+ ( ( invg ` G ) ` x ) ) )
9	8	eqeq1d	|- ( y = ( ( invg ` G ) ` x ) -> ( ( x .+ y ) = .0. <-> ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) )
10	7 9	anbi12d	|- ( y = ( ( invg ` G ) ` x ) -> ( ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) <-> ( ( ( ( invg ` G ) ` x ) .+ x ) = .0. /\ ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) ) )
11	10	adantl	|- ( ( ( G e. Grp /\ x e. B ) /\ y = ( ( invg ` G ) ` x ) ) -> ( ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) <-> ( ( ( ( invg ` G ) ` x ) .+ x ) = .0. /\ ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) ) )
12	1 2 3 4	grplinv	|- ( ( G e. Grp /\ x e. B ) -> ( ( ( invg ` G ) ` x ) .+ x ) = .0. )
13	1 2 3 4	grprinv	|- ( ( G e. Grp /\ x e. B ) -> ( x .+ ( ( invg ` G ) ` x ) ) = .0. )
14	12 13	jca	|- ( ( G e. Grp /\ x e. B ) -> ( ( ( ( invg ` G ) ` x ) .+ x ) = .0. /\ ( x .+ ( ( invg ` G ) ` x ) ) = .0. ) )
15	5 11 14	rspcedvd	|- ( ( G e. Grp /\ x e. B ) -> E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )
16	15	ralrimiva	|- ( G e. Grp -> A. x e. B E. y e. B ( ( y .+ x ) = .0. /\ ( x .+ y ) = .0. ) )