Metamath Proof Explorer


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
grpinv.u 0 ˙ = 0 G
grpinv.n N = inv g G
Assertion grplinv G Grp X B N X + ˙ X = 0 ˙

Proof

Step Hyp Ref Expression
1 grpinv.b B = Base G
2 grpinv.p + ˙ = + G
3 grpinv.u 0 ˙ = 0 G
4 grpinv.n N = inv g G
5 1 2 3 4 grpinvval X B N X = ι y B | y + ˙ X = 0 ˙
6 5 adantl G Grp X B N X = ι y B | y + ˙ X = 0 ˙
7 1 2 3 grpinveu G Grp X B ∃! y B y + ˙ X = 0 ˙
8 riotacl2 ∃! y B y + ˙ X = 0 ˙ ι y B | y + ˙ X = 0 ˙ y B | y + ˙ X = 0 ˙
9 7 8 syl G Grp X B ι y B | y + ˙ X = 0 ˙ y B | y + ˙ X = 0 ˙
10 6 9 eqeltrd G Grp X B N X y 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 y B | y + ˙ X = 0 ˙ N X B N X + ˙ X = 0 ˙
14 13 simprbi N X y B | y + ˙ X = 0 ˙ N X + ˙ X = 0 ˙
15 10 14 syl G Grp X B N X + ˙ X = 0 ˙