Theorem linvh

Description: If an element has a unique left inverse, then the value satisfies the left inverse value equation. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	linvh.1	|- ( ph -> X e. ( Base ` R ) )
	linvh.2	|- ( ph -> E! i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) )
Assertion	linvh	|- ( ph -> ( ( ( invg ` R ) ` X ) ( +g ` R ) X ) = ( 0g ` R ) )

Proof

Step	Hyp	Ref	Expression
1		linvh.1	|- ( ph -> X e. ( Base ` R ) )
2		linvh.2	|- ( ph -> E! i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) )
3		eqid	|- ( Base ` R ) = ( Base ` R )
4		eqid	|- ( +g ` R ) = ( +g ` R )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6		eqid	|- ( invg ` R ) = ( invg ` R )
7	3 4 5 6	grpinvval	|- ( X e. ( Base ` R ) -> ( ( invg ` R ) ` X ) = ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) ) )
8	1 7	syl	|- ( ph -> ( ( invg ` R ) ` X ) = ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) ) )
9		riotacl2	|- ( E! i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) -> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) ) e. { i e. ( Base ` R ) | ( i ( +g ` R ) X ) = ( 0g ` R ) } )
10	2 9	syl	|- ( ph -> ( iota_ i e. ( Base ` R ) ( i ( +g ` R ) X ) = ( 0g ` R ) ) e. { i e. ( Base ` R ) | ( i ( +g ` R ) X ) = ( 0g ` R ) } )
11	8 10	eqeltrd	|- ( ph -> ( ( invg ` R ) ` X ) e. { i e. ( Base ` R ) | ( i ( +g ` R ) X ) = ( 0g ` R ) } )
12		oveq1	|- ( i = ( ( invg ` R ) ` X ) -> ( i ( +g ` R ) X ) = ( ( ( invg ` R ) ` X ) ( +g ` R ) X ) )
13	12	eqeq1d	|- ( i = ( ( invg ` R ) ` X ) -> ( ( i ( +g ` R ) X ) = ( 0g ` R ) <-> ( ( ( invg ` R ) ` X ) ( +g ` R ) X ) = ( 0g ` R ) ) )
14	13	elrab	|- ( ( ( invg ` R ) ` X ) e. { i e. ( Base ` R ) | ( i ( +g ` R ) X ) = ( 0g ` R ) } <-> ( ( ( invg ` R ) ` X ) e. ( Base ` R ) /\ ( ( ( invg ` R ) ` X ) ( +g ` R ) X ) = ( 0g ` R ) ) )
15	14	simprbi	|- ( ( ( invg ` R ) ` X ) e. { i e. ( Base ` R ) | ( i ( +g ` R ) X ) = ( 0g ` R ) } -> ( ( ( invg ` R ) ` X ) ( +g ` R ) X ) = ( 0g ` R ) )
16	11 15	syl	|- ( ph -> ( ( ( invg ` R ) ` X ) ( +g ` R ) X ) = ( 0g ` R ) )