Theorem grpidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by AV, 1-Sep-2021)

	Ref	Expression
Hypotheses	grplrinv.b	|- B = ( Base ` G )
	grplrinv.p	|- .+ = ( +g ` G )
	grplrinv.i	|- .0. = ( 0g ` G )
Assertion	grpidinv2	|- ( ( G e. Grp /\ A e. B ) -> ( ( ( .0. .+ A ) = A /\ ( A .+ .0. ) = A ) /\ E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ 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	1 2 3	grplid	|- ( ( G e. Grp /\ A e. B ) -> ( .0. .+ A ) = A )
5	1 2 3	grprid	|- ( ( G e. Grp /\ A e. B ) -> ( A .+ .0. ) = A )
6	1 2 3	grplrinv	|- ( G e. Grp -> A. z e. B E. y e. B ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) )
7		oveq2	|- ( z = A -> ( y .+ z ) = ( y .+ A ) )
8	7	eqeq1d	|- ( z = A -> ( ( y .+ z ) = .0. <-> ( y .+ A ) = .0. ) )
9		oveq1	|- ( z = A -> ( z .+ y ) = ( A .+ y ) )
10	9	eqeq1d	|- ( z = A -> ( ( z .+ y ) = .0. <-> ( A .+ y ) = .0. ) )
11	8 10	anbi12d	|- ( z = A -> ( ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) <-> ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
12	11	rexbidv	|- ( z = A -> ( E. y e. B ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) <-> E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
13	12	rspcv	|- ( A e. B -> ( A. z e. B E. y e. B ( ( y .+ z ) = .0. /\ ( z .+ y ) = .0. ) -> E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )
14	6 13	mpan9	|- ( ( G e. Grp /\ A e. B ) -> E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) )
15	4 5 14	jca31	|- ( ( G e. Grp /\ A e. B ) -> ( ( ( .0. .+ A ) = A /\ ( A .+ .0. ) = A ) /\ E. y e. B ( ( y .+ A ) = .0. /\ ( A .+ y ) = .0. ) ) )