Theorem grplinv

Description: The left inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpinv.b	|- B = ( Base ` G )
	grpinv.p	|- .+ = ( +g ` G )
	grpinv.u	|- .0. = ( 0g ` G )
	grpinv.n	|- N = ( invg ` G )
Assertion	grplinv	|- ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		grpinv.b	|- B = ( Base ` G )
2		grpinv.p	|- .+ = ( +g ` G )
3		grpinv.u	|- .0. = ( 0g ` G )
4		grpinv.n	|- N = ( invg ` G )
5	1 2 3 4	grpinvval	|- ( X e. B -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
6	5	adantl	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) = ( iota_ y e. B ( y .+ X ) = .0. ) )
7	1 2 3	grpinveu	|- ( ( G e. Grp /\ X e. B ) -> E! y e. B ( y .+ X ) = .0. )
8		riotacl2	|- ( E! y e. B ( y .+ X ) = .0. -> ( iota_ y e. B ( y .+ X ) = .0. ) e. { y e. B | ( y .+ X ) = .0. } )
9	7 8	syl	|- ( ( G e. Grp /\ X e. B ) -> ( iota_ y e. B ( y .+ X ) = .0. ) e. { y e. B | ( y .+ X ) = .0. } )
10	6 9	eqeltrd	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. { y e. B | ( y .+ X ) = .0. } )
11		oveq1	|- ( y = ( N ` X ) -> ( y .+ X ) = ( ( N ` X ) .+ X ) )
12	11	eqeq1d	|- ( y = ( N ` X ) -> ( ( y .+ X ) = .0. <-> ( ( N ` X ) .+ X ) = .0. ) )
13	12	elrab	|- ( ( N ` X ) e. { y e. B | ( y .+ X ) = .0. } <-> ( ( N ` X ) e. B /\ ( ( N ` X ) .+ X ) = .0. ) )
14	13	simprbi	|- ( ( N ` X ) e. { y e. B | ( y .+ X ) = .0. } -> ( ( N ` X ) .+ X ) = .0. )
15	10 14	syl	|- ( ( G e. Grp /\ X e. B ) -> ( ( N ` X ) .+ X ) = .0. )