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

Theorem imasgrp 14627
 Description: The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
Hypotheses
Ref Expression
imasgrp.u s
imasgrp.v
imasgrp.p
imasgrp.f
imasgrp.e
imasgrp.r
imasgrp.z
Assertion
Ref Expression
imasgrp
Distinct variable groups:   ,,   ,,,,   ,,   ,,,,   ,,   ,,,,   ,,,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem imasgrp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasgrp.u . 2 s
2 imasgrp.v . 2
3 imasgrp.p . 2
4 imasgrp.f . 2
5 imasgrp.e . 2
6 imasgrp.r . 2
763ad2ant1 976 . . . 4
8 simp2 956 . . . . 5
923ad2ant1 976 . . . . 5
108, 9eleqtrd 2372 . . . 4
11 simp3 957 . . . . 5
1211, 9eleqtrd 2372 . . . 4
13 eqid 2296 . . . . 5
14 eqid 2296 . . . . 5
1513, 14grpcl 14511 . . . 4
167, 10, 12, 15syl3anc 1182 . . 3
1733ad2ant1 976 . . . . 5
1817oveqd 5891 . . . 4
1918, 9eleq12d 2364 . . 3
2016, 19mpbird 223 . 2
216adantr 451 . . . . 5
22103adant3r3 1162 . . . . 5
23123adant3r3 1162 . . . . 5
24 simpr3 963 . . . . . 6
252adantr 451 . . . . . 6
2624, 25eleqtrd 2372 . . . . 5
2713, 14grpass 14512 . . . . 5
2821, 22, 23, 26, 27syl13anc 1184 . . . 4
293adantr 451 . . . . 5
30183adant3r3 1162 . . . . 5
31 eqidd 2297 . . . . 5
3229, 30, 31oveq123d 5895 . . . 4
33 eqidd 2297 . . . . 5
3429oveqd 5891 . . . . 5
3529, 33, 34oveq123d 5895 . . . 4
3628, 32, 353eqtr4d 2338 . . 3
3736fveq2d 5545 . 2
38 imasgrp.z . . . . 5
3913, 38grpidcl 14526 . . . 4
406, 39syl 15 . . 3
4140, 2eleqtrrd 2373 . 2
423adantr 451 . . . . 5
4342oveqd 5891 . . . 4
446adantr 451 . . . . 5
452eleq2d 2363 . . . . . 6
4645biimpa 470 . . . . 5
4713, 14, 38grplid 14528 . . . . 5
4844, 46, 47syl2anc 642 . . . 4
4943, 48eqtrd 2328 . . 3
5049fveq2d 5545 . 2
51 eqid 2296 . . . . 5
5213, 51grpinvcl 14543 . . . 4
5344, 46, 52syl2anc 642 . . 3