Metamath Proof Explorer


Theorem grpridd

Description: Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013) (Proof shortened by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses grprinvlem.c φ x B y B x + ˙ y B
grprinvlem.o φ O B
grprinvlem.i φ x B O + ˙ x = x
grprinvlem.a φ x B y B z B x + ˙ y + ˙ z = x + ˙ y + ˙ z
grprinvlem.n φ x B y B y + ˙ x = O
Assertion grpridd φ x B x + ˙ O = x

Proof

Step Hyp Ref Expression
1 grprinvlem.c φ x B y B x + ˙ y B
2 grprinvlem.o φ O B
3 grprinvlem.i φ x B O + ˙ x = x
4 grprinvlem.a φ x B y B z B x + ˙ y + ˙ z = x + ˙ y + ˙ z
5 grprinvlem.n φ x B y B y + ˙ x = O
6 oveq1 y = n y + ˙ x = n + ˙ x
7 6 eqeq1d y = n y + ˙ x = O n + ˙ x = O
8 7 cbvrexvw y B y + ˙ x = O n B n + ˙ x = O
9 5 8 sylib φ x B n B n + ˙ x = O
10 4 caovassg φ u B v B w B u + ˙ v + ˙ w = u + ˙ v + ˙ w
11 10 adantlr φ x B n B n + ˙ x = O u B v B w B u + ˙ v + ˙ w = u + ˙ v + ˙ w
12 simprl φ x B n B n + ˙ x = O x B
13 simprrl φ x B n B n + ˙ x = O n B
14 11 12 13 12 caovassd φ x B n B n + ˙ x = O x + ˙ n + ˙ x = x + ˙ n + ˙ x
15 simprrr φ x B n B n + ˙ x = O n + ˙ x = O
16 1 2 3 4 5 12 13 15 grprinvd φ x B n B n + ˙ x = O x + ˙ n = O
17 16 oveq1d φ x B n B n + ˙ x = O x + ˙ n + ˙ x = O + ˙ x
18 15 oveq2d φ x B n B n + ˙ x = O x + ˙ n + ˙ x = x + ˙ O
19 14 17 18 3eqtr3d φ x B n B n + ˙ x = O O + ˙ x = x + ˙ O
20 19 anassrs φ x B n B n + ˙ x = O O + ˙ x = x + ˙ O
21 9 20 rexlimddv φ x B O + ˙ x = x + ˙ O
22 21 3 eqtr3d φ x B x + ˙ O = x