Metamath Proof Explorer


Theorem grpidinv

Description: A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006) (Revised by AV, 1-Sep-2021)

Ref Expression
Hypotheses grpidinv.b B = Base G
grpidinv.p + ˙ = + G
Assertion grpidinv G Grp u B x B u + ˙ x = x x + ˙ u = x y B y + ˙ x = u x + ˙ y = u

Proof

Step Hyp Ref Expression
1 grpidinv.b B = Base G
2 grpidinv.p + ˙ = + G
3 eqid 0 G = 0 G
4 1 3 grpidcl G Grp 0 G B
5 oveq1 u = 0 G u + ˙ x = 0 G + ˙ x
6 5 eqeq1d u = 0 G u + ˙ x = x 0 G + ˙ x = x
7 oveq2 u = 0 G x + ˙ u = x + ˙ 0 G
8 7 eqeq1d u = 0 G x + ˙ u = x x + ˙ 0 G = x
9 6 8 anbi12d u = 0 G u + ˙ x = x x + ˙ u = x 0 G + ˙ x = x x + ˙ 0 G = x
10 eqeq2 u = 0 G y + ˙ x = u y + ˙ x = 0 G
11 eqeq2 u = 0 G x + ˙ y = u x + ˙ y = 0 G
12 10 11 anbi12d u = 0 G y + ˙ x = u x + ˙ y = u y + ˙ x = 0 G x + ˙ y = 0 G
13 12 rexbidv u = 0 G y B y + ˙ x = u x + ˙ y = u y B y + ˙ x = 0 G x + ˙ y = 0 G
14 9 13 anbi12d u = 0 G u + ˙ x = x x + ˙ u = x y B y + ˙ x = u x + ˙ y = u 0 G + ˙ x = x x + ˙ 0 G = x y B y + ˙ x = 0 G x + ˙ y = 0 G
15 14 ralbidv u = 0 G x B u + ˙ x = x x + ˙ u = x y B y + ˙ x = u x + ˙ y = u x B 0 G + ˙ x = x x + ˙ 0 G = x y B y + ˙ x = 0 G x + ˙ y = 0 G
16 15 adantl G Grp u = 0 G x B u + ˙ x = x x + ˙ u = x y B y + ˙ x = u x + ˙ y = u x B 0 G + ˙ x = x x + ˙ 0 G = x y B y + ˙ x = 0 G x + ˙ y = 0 G
17 1 2 3 grpidinv2 G Grp x B 0 G + ˙ x = x x + ˙ 0 G = x y B y + ˙ x = 0 G x + ˙ y = 0 G
18 17 ralrimiva G Grp x B 0 G + ˙ x = x x + ˙ 0 G = x y B y + ˙ x = 0 G x + ˙ y = 0 G
19 4 16 18 rspcedvd G Grp u B x B u + ˙ x = x x + ˙ u = x y B y + ˙ x = u x + ˙ y = u