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

Theorem imasgrp 16744
 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 1026 . . . 4
8 simp2 1006 . . . . 5
923ad2ant1 1026 . . . . 5
108, 9eleqtrd 2519 . . . 4
11 simp3 1007 . . . . 5
1211, 9eleqtrd 2519 . . . 4
13 eqid 2429 . . . . 5
14 eqid 2429 . . . . 5
1513, 14grpcl 16621 . . . 4
167, 10, 12, 15syl3anc 1264 . . 3
1733ad2ant1 1026 . . . 4
1817oveqd 6322 . . 3
1916, 18, 93eltr4d 2532 . 2
206adantr 466 . . . . 5
21103adant3r3 1216 . . . . 5
22123adant3r3 1216 . . . . 5
23 simpr3 1013 . . . . . 6
242adantr 466 . . . . . 6
2523, 24eleqtrd 2519 . . . . 5
2613, 14grpass 16622 . . . . 5
2720, 21, 22, 25, 26syl13anc 1266 . . . 4
283adantr 466 . . . . 5
29183adant3r3 1216 . . . . 5
30 eqidd 2430 . . . . 5
3128, 29, 30oveq123d 6326 . . . 4
32 eqidd 2430 . . . . 5
3328oveqd 6322 . . . . 5
3428, 32, 33oveq123d 6326 . . . 4
3527, 31, 343eqtr4d 2480 . . 3
3635fveq2d 5885 . 2
37 imasgrp.z . . . . 5
3813, 37grpidcl 16636 . . . 4
396, 38syl 17 . . 3
4039, 2eleqtrrd 2520 . 2
413adantr 466 . . . . 5
4241oveqd 6322 . . . 4
436adantr 466 . . . . 5
442eleq2d 2499 . . . . . 6
4544biimpa 486 . . . . 5
4613, 14, 37grplid 16638 . . . . 5
4743, 45, 46syl2anc 665 . . . 4
4842, 47eqtrd 2470 . . 3
4948fveq2d 5885 . 2
50 eqid 2429 . . . . 5
5113, 50grpinvcl 16653 . . . 4
5243, 45, 51syl2anc 665 . . 3