Theorem idvalriota

Description: The unique value of the group identity element. (Contributed by FL, 12-Dec-2009) (Revised by AV, 24-Aug-2026)

	Ref	Expression
Hypotheses	grpidval.b	|- B = ( Base ` G )
	grpidval.p	|- .+ = ( +g ` G )
	grpidval.o	|- .0. = ( 0g ` G )
Assertion	idvalriota	|- .0. = ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )

Proof

Step	Hyp	Ref	Expression
1		grpidval.b	|- B = ( Base ` G )
2		grpidval.p	|- .+ = ( +g ` G )
3		grpidval.o	|- .0. = ( 0g ` G )
4	1 2 3	grpidval	|- .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
5		df-riota	|- ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
6	4 5	eqtr4i	|- .0. = ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )