Metamath Proof Explorer


Theorem grprinvlem

Description: Lemma for grprinvd . (Contributed by NM, 9-Aug-2013)

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
grprinvlem.x φ ψ X B
grprinvlem.e φ ψ X + ˙ X = X
Assertion grprinvlem φ ψ X = O

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 grprinvlem.x φ ψ X B
7 grprinvlem.e φ ψ X + ˙ X = X
8 5 ralrimiva φ x B y B y + ˙ x = O
9 oveq2 x = z y + ˙ x = y + ˙ z
10 9 eqeq1d x = z y + ˙ x = O y + ˙ z = O
11 10 rexbidv x = z y B y + ˙ x = O y B y + ˙ z = O
12 11 cbvralvw x B y B y + ˙ x = O z B y B y + ˙ z = O
13 8 12 sylib φ z B y B y + ˙ z = O
14 oveq2 z = X y + ˙ z = y + ˙ X
15 14 eqeq1d z = X y + ˙ z = O y + ˙ X = O
16 15 rexbidv z = X y B y + ˙ z = O y B y + ˙ X = O
17 16 rspccva z B y B y + ˙ z = O X B y B y + ˙ X = O
18 13 6 17 syl2an2r φ ψ y B y + ˙ X = O
19 7 oveq2d φ ψ y + ˙ X + ˙ X = y + ˙ X
20 19 adantr φ ψ y B y + ˙ X = O y + ˙ X + ˙ X = y + ˙ X
21 simprr φ ψ y B y + ˙ X = O y + ˙ X = O
22 21 oveq1d φ ψ y B y + ˙ X = O y + ˙ X + ˙ X = O + ˙ X
23 4 caovassg φ u B v B w B u + ˙ v + ˙ w = u + ˙ v + ˙ w
24 23 ad4ant14 φ ψ y B y + ˙ X = O u B v B w B u + ˙ v + ˙ w = u + ˙ v + ˙ w
25 simprl φ ψ y B y + ˙ X = O y B
26 6 adantr φ ψ y B y + ˙ X = O X B
27 24 25 26 26 caovassd φ ψ y B y + ˙ X = O y + ˙ X + ˙ X = y + ˙ X + ˙ X
28 oveq2 y = X O + ˙ y = O + ˙ X
29 id y = X y = X
30 28 29 eqeq12d y = X O + ˙ y = y O + ˙ X = X
31 3 ralrimiva φ x B O + ˙ x = x
32 oveq2 x = y O + ˙ x = O + ˙ y
33 id x = y x = y
34 32 33 eqeq12d x = y O + ˙ x = x O + ˙ y = y
35 34 cbvralvw x B O + ˙ x = x y B O + ˙ y = y
36 31 35 sylib φ y B O + ˙ y = y
37 36 adantr φ ψ y B O + ˙ y = y
38 30 37 6 rspcdva φ ψ O + ˙ X = X
39 38 adantr φ ψ y B y + ˙ X = O O + ˙ X = X
40 22 27 39 3eqtr3d φ ψ y B y + ˙ X = O y + ˙ X + ˙ X = X
41 20 40 21 3eqtr3d φ ψ y B y + ˙ X = O X = O
42 18 41 rexlimddv φ ψ X = O