Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  grprinvlem Unicode version

Theorem grprinvlem 6074
 Description: Lemma for grprinvd 6075. (Contributed by NM, 9-Aug-2013.)
Hypotheses
Ref Expression
grprinvlem.c
grprinvlem.o
grprinvlem.i
grprinvlem.a
grprinvlem.n
grprinvlem.x
grprinvlem.e
Assertion
Ref Expression
grprinvlem
Distinct variable groups:   ,,,   ,,,   ,,,   , ,,   ,,   ,
Allowed substitution hints:   (,)   ()

Proof of Theorem grprinvlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grprinvlem.x . . 3
2 grprinvlem.n . . . . . 6
32ralrimiva 2639 . . . . 5
4 oveq2 5882 . . . . . . . 8
54eqeq1d 2304 . . . . . . 7
65rexbidv 2577 . . . . . 6
76cbvralv 2777 . . . . 5
83, 7sylib 188 . . . 4
9 oveq2 5882 . . . . . . 7
109eqeq1d 2304 . . . . . 6
1110rexbidv 2577 . . . . 5
1211rspccva 2896 . . . 4
138, 12sylan 457 . . 3
141, 13syldan 456 . 2
15 grprinvlem.e . . . . . . 7
1615oveq2d 5890 . . . . . 6
1716adantr 451 . . . . 5
18 simprr 733 . . . . . . 7
1918oveq1d 5889 . . . . . 6
20 simpll 730 . . . . . . . 8
21 grprinvlem.a . . . . . . . . 9
2221caovassg 6034 . . . . . . . 8
2320, 22sylan 457 . . . . . . 7
24 simprl 732 . . . . . . 7
251adantr 451 . . . . . . 7
2623, 24, 25, 25caovassd 6035 . . . . . 6
27 grprinvlem.i . . . . . . . . . . 11
2827ralrimiva 2639 . . . . . . . . . 10
29 oveq2 5882 . . . . . . . . . . . 12
30 id 19 . . . . . . . . . . . 12
3129, 30eqeq12d 2310 . . . . . . . . . . 11
3231cbvralv 2777 . . . . . . . . . 10
3328, 32sylib 188 . . . . . . . . 9
3433adantr 451 . . . . . . . 8
35 oveq2 5882 . . . . . . . . . 10
36 id 19 . . . . . . . . . 10
3735, 36eqeq12d 2310 . . . . . . . . 9
3837rspcv 2893 . . . . . . . 8
391, 34, 38sylc 56 . . . . . . 7
4039adantr 451 . . . . . 6
4119, 26, 403eqtr3d 2336 . . . . 5
4217, 41, 183eqtr3d 2336 . . . 4
4342expr 598 . . 3
4443rexlimdva 2680 . 2
4514, 44mpd 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   w3a 934   wceq 1632   wcel 1696  wral 2556  wrex 2557  (class class class)co 5874 This theorem is referenced by:  grprinvd  6075 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
 Copyright terms: Public domain W3C validator