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

Theorem ghgrp 25074
 Description: The image of a group under a group homomorphism is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
ghgrp.1
ghgrp.2
ghgrp.3
ghgrp.4
ghgrp.5
ghgrp.6
ghgrp.7
Assertion
Ref Expression
ghgrp
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem ghgrp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ghgrp.4 . . . 4
2 ghgrp.7 . . . . 5
3 rnexg 6716 . . . . 5
42, 3syl 16 . . . 4
51, 4syl5eqel 2559 . . 3
6 ghgrp.1 . . 3
7 fornex 6753 . . 3
85, 6, 7sylc 60 . 2
9 fof 5795 . . . . 5
106, 9syl 16 . . . 4
11 eqid 2467 . . . . . 6 GId GId
121, 11grpoidcl 24923 . . . . 5 GId
132, 12syl 16 . . . 4 GId
1410, 13ffvelrnd 6022 . . 3 GId
15 ne0i 3791 . . 3 GId
1614, 15syl 16 . 2
17 ghgrp.6 . . . . 5
18 ghgrp.5 . . . . . 6
19 xpss12 5108 . . . . . 6
2018, 18, 19syl2anc 661 . . . . 5
21 fnssres 5694 . . . . 5
2217, 20, 21syl2anc 661 . . . 4
23 ghgrp.3 . . . . 5
2423fneq1i 5675 . . . 4
2522, 24sylibr 212 . . 3
266adantr 465 . . . . . . 7
27 ghgrp.2 . . . . . . . . . 10
286, 27, 23ghgrplem2 25073 . . . . . . . . 9
291grpocl 24906 . . . . . . . . . . . 12
30293expb 1197 . . . . . . . . . . 11
312, 30sylan 471 . . . . . . . . . 10
3210ffvelrnda 6021 . . . . . . . . . 10
3331, 32syldan 470 . . . . . . . . 9
3428, 33eqeltrrd 2556 . . . . . . . 8
3534anassrs 648 . . . . . . 7
36 oveq2 6292 . . . . . . . 8
3736eleq1d 2536 . . . . . . 7
3826, 35, 37ghgrplem1 25072 . . . . . 6
3938ralrimiva 2878 . . . . 5
40 oveq1 6291 . . . . . . 7
4140eleq1d 2536 . . . . . 6
4241ralbidv 2903 . . . . 5
436, 39, 42ghgrplem1 25072 . . . 4
4443ralrimiva 2878 . . 3
45 ffnov 6390 . . 3
4625, 44, 45sylanbrc 664 . 2
472adantr 465 . . . . . . . . . . . . . . . . 17
48 simprll 761 . . . . . . . . . . . . . . . . 17
49 simprlr 762 . . . . . . . . . . . . . . . . 17
50 simprr 756 . . . . . . . . . . . . . . . . 17
511grpoass 24909 . . . . . . . . . . . . . . . . 17
5247, 48, 49, 50, 51syl13anc 1230 . . . . . . . . . . . . . . . 16
5352fveq2d 5870 . . . . . . . . . . . . . . 15
54 simpl 457 . . . . . . . . . . . . . . . 16
5531adantrr 716 . . . . . . . . . . . . . . . 16
566, 27, 23ghgrplem2 25073 . . . . . . . . . . . . . . . 16
5754, 55, 50, 56syl12anc 1226 . . . . . . . . . . . . . . 15
581grpocl 24906 . . . . . . . . . . . . . . . . 17
5947, 49, 50, 58syl3anc 1228 . . . . . . . . . . . . . . . 16
606, 27, 23ghgrplem2 25073 . . . . . . . . . . . . . . . 16
6154, 48, 59, 60syl12anc 1226 . . . . . . . . . . . . . . 15
6253, 57, 613eqtr3d 2516 . . . . . . . . . . . . . 14
6328adantrr 716 . . . . . . . . . . . . . . 15
6463oveq1d 6299 . . . . . . . . . . . . . 14
656, 27, 23ghgrplem2 25073 . . . . . . . . . . . . . . . 16
6654, 49, 50, 65syl12anc 1226 . . . . . . . . . . . . . . 15
6766oveq2d 6300 . . . . . . . . . . . . . 14
6862, 64, 673eqtr3d 2516 . . . . . . . . . . . . 13
6968expr 615 . . . . . . . . . . . 12
7069impancom 440 . . . . . . . . . . 11
71 oveq2 6292 . . . . . . . . . . . . 13
72 oveq2 6292 . . . . . . . . . . . . . 14
7372oveq2d 6300 . . . . . . . . . . . . 13
7471, 73eqeq12d 2489 . . . . . . . . . . . 12
7574imbi2d 316 . . . . . . . . . . 11
766, 70, 75ghgrplem1 25072 . . . . . . . . . 10
7776impancom 440 . . . . . . . . 9
7877expr 615 . . . . . . . 8
7978impancom 440 . . . . . . 7
8036oveq1d 6299 . . . . . . . . . 10
81 oveq1 6291 . . . . . . . . . . 11
8281oveq2d 6300 . . . . . . . . . 10
8380, 82eqeq12d 2489 . . . . . . . . 9
8483imbi2d 316 . . . . . . . 8
8584imbi2d 316 . . . . . . 7
866, 79, 85ghgrplem1 25072 . . . . . 6
8786impancom 440 . . . . 5
8840oveq1d 6299 . . . . . . . 8
89 oveq1 6291 . . . . . . . 8
9088, 89eqeq12d 2489 . . . . . . 7
9190imbi2d 316 . . . . . 6
9291imbi2d 316 . . . . 5
936, 87, 92ghgrplem1 25072 . . . 4
9493ex 434 . . 3
95943imp2 1211 . 2
9610adantr 465 . . . . . . . . . . . 12
972adantr 465 . . . . . . . . . . . . 13
98 simprr 756 . . . . . . . . . . . . 13
99 simprl 755 . . . . . . . . . . . . 13
100 eqid 2467 . . . . . . . . . . . . . 14
1011, 100grpodivcl 24953 . . . . . . . . . . . . 13
10297, 98, 99, 101syl3anc 1228 . . . . . . . . . . . 12
10396, 102ffvelrnd 6022 . . . . . . . . . . 11
104 simpl 457 . . . . . . . . . . . . 13
1056, 27, 23ghgrplem2 25073 . . . . . . . . . . . . 13
106104, 102, 99, 105syl12anc 1226 . . . . . . . . . . . 12
1071, 100grponpcan 24958 . . . . . . . . . . . . . 14
10897, 98, 99, 107syl3anc 1228 . . . . . . . . . . . . 13
109108fveq2d 5870 . . . . . . . . . . . 12
110106, 109eqtr3d 2510 . . . . . . . . . . 11
111 oveq1 6291 . . . . . . . . . . . . 13
112111eqeq1d 2469 . . . . . . . . . . . 12
113112rspcev 3214 . . . . . . . . . . 11
114103, 110, 113syl2anc 661 . . . . . . . . . 10
115 eqid 2467 . . . . . . . . . . . . . . 15
1161, 115grpoinvcl 24932 . . . . . . . . . . . . . 14
11797, 99, 116syl2anc 661 . . . . . . . . . . . . 13
1181grpocl 24906 . . . . . . . . . . . . 13
11997, 117, 98, 118syl3anc 1228 . . . . . . . . . . . 12
12096, 119ffvelrnd 6022 . . . . . . . . . . 11
1216, 27, 23ghgrplem2 25073 . . . . . . . . . . . . 13
122104, 99, 119, 121syl12anc 1226 . . . . . . . . . . . 12
1231, 115grpoasscan1 24943 . . . . . . . . . . . . . 14
12497, 99, 98, 123syl3anc 1228 . . . . . . . . . . . . 13
125124fveq2d 5870 . . . . . . . . . . . 12
126122, 125eqtr3d 2510 . . . . . . . . . . 11
127 oveq2 6292 . . . . . . . . . . . . 13
128127eqeq1d 2469 . . . . . . . . . . . 12
129128rspcev 3214 . . . . . . . . . . 11
130120, 126, 129syl2anc 661 . . . . . . . . . 10
131114, 130jca 532 . . . . . . . . 9
132131expr 615 . . . . . . . 8
133132impancom 440 . . . . . . 7
134 eqeq2 2482 . . . . . . . . . 10
135134rexbidv 2973 . . . . . . . . 9
136 eqeq2 2482 . . . . . . . . . 10
137136rexbidv 2973 . . . . . . . . 9
138135, 137anbi12d 710 . . . . . . . 8
139138imbi2d 316 . . . . . . 7
1406, 133, 139ghgrplem1 25072 . . . . . 6
141140impancom 440 . . . . 5
142 oveq2 6292 . . . . . . . . 9
143142eqeq1d 2469 . . . . . . . 8
144143rexbidv 2973 . . . . . . 7
145 oveq1 6291 . . . . . . . . 9
146145eqeq1d 2469 . . . . . . . 8
147146rexbidv 2973 . . . . . . 7
148144, 147anbi12d 710 . . . . . 6
149148imbi2d 316 . . . . 5
1506, 141, 149ghgrplem1 25072 . . . 4
151150impr 619 . . 3
152151simpld 459 . 2
153151simprd 463 . 2
1548, 16, 46, 95, 152, 153isgrp2d 24941 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767   wne 2662  wral 2814  wrex 2815  cvv 3113   wss 3476  c0 3785   cxp 4997   crn 5000   cres 5001   wfn 5583  wf 5584  wfo 5586  cfv 5588  (class class class)co 6284  cgr 24892  GIdcgi 24893  cgn 24894   cgs 24895 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-1st 6784  df-2nd 6785  df-grpo 24897  df-gid 24898  df-ginv 24899  df-gdiv 24900 This theorem is referenced by:  ghablo  25075  ghsubgolem  25076
 Copyright terms: Public domain W3C validator