Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  exidresid Structured version   Visualization version   Unicode version

Theorem exidresid 32170
 Description: The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
Hypotheses
Ref Expression
exidres.1
exidres.2 GId
exidres.3
Assertion
Ref Expression
exidresid GId

Proof of Theorem exidresid
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exidres.3 . . . . . 6
2 resexg 5146 . . . . . 6
31, 2syl5eqel 2532 . . . . 5
4 eqid 2450 . . . . . 6
54gidval 25934 . . . . 5 GId
63, 5syl 17 . . . 4 GId
763ad2ant1 1028 . . 3 GId
9 exidres.1 . . . . . . 7
10 exidres.2 . . . . . . 7 GId
119, 10, 1exidreslem 32168 . . . . . 6
1211simprd 465 . . . . 5
1312adantr 467 . . . 4
149, 10, 1exidres 32169 . . . . . 6
15 elin 3616 . . . . . . . 8
16 rngopidOLD 26044 . . . . . . . 8
1715, 16sylbir 217 . . . . . . 7
1817ancoms 455 . . . . . 6
1914, 18sylan 474 . . . . 5
2019raleqdv 2992 . . . 4
2113, 20mpbird 236 . . 3
2211simpld 461 . . . . . 6
2322adantr 467 . . . . 5
2423, 19eleqtrrd 2531 . . . 4
254exidu1 26047 . . . . . . 7
2615, 25sylbir 217 . . . . . 6
2726ancoms 455 . . . . 5
2814, 27sylan 474 . . . 4
29 oveq1 6295 . . . . . . . 8
3029eqeq1d 2452 . . . . . . 7
31 oveq2 6296 . . . . . . . 8
3231eqeq1d 2452 . . . . . . 7
3330, 32anbi12d 716 . . . . . 6
3433ralbidv 2826 . . . . 5
3534riota2 6272 . . . 4
3624, 28, 35syl2anc 666 . . 3
3721, 36mpbid 214 . 2
388, 37eqtrd 2484 1 GId
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 984   wceq 1443   wcel 1886  wral 2736  wreu 2738  cvv 3044   cin 3402   wss 3403   cxp 4831   cdm 4833   crn 4834   cres 4835  cfv 5581  crio 6249  (class class class)co 6288  GIdcgi 25908   cexid 26035  cmagm 26039 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-un 6580 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-fo 5587  df-fv 5589  df-riota 6250  df-ov 6291  df-gid 25913  df-exid 26036  df-mgmOLD 26040 This theorem is referenced by:  isdrngo2  32190
 Copyright terms: Public domain W3C validator