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

Theorem ghgrpOLD 26079
 Description: Obsolete version of ghmgrp 16795 as of 14-Mar-2020. 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.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ghgrpOLD.1
ghgrpOLD.2
ghgrpOLD.3
ghgrpOLD.4
ghgrpOLD.5
ghgrpOLD.6
ghgrpOLD.7
Assertion
Ref Expression
ghgrpOLD
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem ghgrpOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ghgrpOLD.4 . . . 4
2 ghgrpOLD.7 . . . . 5
3 rnexg 6735 . . . . 5
42, 3syl 17 . . . 4
51, 4syl5eqel 2514 . . 3
6 ghgrpOLD.1 . . 3
7 fornex 6772 . . 3
85, 6, 7sylc 62 . 2
9 fof 5806 . . . . 5
106, 9syl 17 . . . 4
11 eqid 2422 . . . . . 6 GId GId
121, 11grpoidcl 25928 . . . . 5 GId
132, 12syl 17 . . . 4 GId
1410, 13ffvelrnd 6034 . . 3 GId
15 ne0i 3767 . . 3 GId
1614, 15syl 17 . 2
17 ghgrpOLD.6 . . . . 5
18 ghgrpOLD.5 . . . . . 6
19 xpss12 4955 . . . . . 6
2018, 18, 19syl2anc 665 . . . . 5
21 fnssres 5703 . . . . 5
2217, 20, 21syl2anc 665 . . . 4
23 ghgrpOLD.3 . . . . 5
2423fneq1i 5684 . . . 4
2522, 24sylibr 215 . . 3
266adantr 466 . . . . . . 7
27 ghgrpOLD.2 . . . . . . . . . 10
286, 27, 23ghgrplem2OLD 26078 . . . . . . . . 9
291grpocl 25911 . . . . . . . . . . . 12
30293expb 1206 . . . . . . . . . . 11
312, 30sylan 473 . . . . . . . . . 10
3210ffvelrnda 6033 . . . . . . . . . 10
3331, 32syldan 472 . . . . . . . . 9
3428, 33eqeltrrd 2511 . . . . . . . 8
3534anassrs 652 . . . . . . 7
36 oveq2 6309 . . . . . . . 8
3736eleq1d 2491 . . . . . . 7
3826, 35, 37ghgrplem1OLD 26077 . . . . . 6
3938ralrimiva 2839 . . . . 5
40 oveq1 6308 . . . . . . 7
4140eleq1d 2491 . . . . . 6
4241ralbidv 2864 . . . . 5
436, 39, 42ghgrplem1OLD 26077 . . . 4
4443ralrimiva 2839 . . 3
45 ffnov 6410 . . 3
4625, 44, 45sylanbrc 668 . 2
472adantr 466 . . . . . . . . . . . . . . . . 17
48 simprll 770 . . . . . . . . . . . . . . . . 17
49 simprlr 771 . . . . . . . . . . . . . . . . 17
50 simprr 764 . . . . . . . . . . . . . . . . 17
511grpoass 25914 . . . . . . . . . . . . . . . . 17
5247, 48, 49, 50, 51syl13anc 1266 . . . . . . . . . . . . . . . 16
5352fveq2d 5881 . . . . . . . . . . . . . . 15
54 simpl 458 . . . . . . . . . . . . . . . 16
5531adantrr 721 . . . . . . . . . . . . . . . 16
566, 27, 23ghgrplem2OLD 26078 . . . . . . . . . . . . . . . 16
5754, 55, 50, 56syl12anc 1262 . . . . . . . . . . . . . . 15
581grpocl 25911 . . . . . . . . . . . . . . . . 17
5947, 49, 50, 58syl3anc 1264 . . . . . . . . . . . . . . . 16
606, 27, 23ghgrplem2OLD 26078 . . . . . . . . . . . . . . . 16
6154, 48, 59, 60syl12anc 1262 . . . . . . . . . . . . . . 15
6253, 57, 613eqtr3d 2471 . . . . . . . . . . . . . 14
6328adantrr 721 . . . . . . . . . . . . . . 15
6463oveq1d 6316 . . . . . . . . . . . . . 14
656, 27, 23ghgrplem2OLD 26078 . . . . . . . . . . . . . . . 16
6654, 49, 50, 65syl12anc 1262 . . . . . . . . . . . . . . 15
6766oveq2d 6317 . . . . . . . . . . . . . 14
6862, 64, 673eqtr3d 2471 . . . . . . . . . . . . 13
6968expr 618 . . . . . . . . . . . 12
7069impancom 441 . . . . . . . . . . 11
71 oveq2 6309 . . . . . . . . . . . . 13
72 oveq2 6309 . . . . . . . . . . . . . 14
7372oveq2d 6317 . . . . . . . . . . . . 13
7471, 73eqeq12d 2444 . . . . . . . . . . . 12
7574imbi2d 317 . . . . . . . . . . 11
766, 70, 75ghgrplem1OLD 26077 . . . . . . . . . 10
7776impancom 441 . . . . . . . . 9
7877expr 618 . . . . . . . 8
7978impancom 441 . . . . . . 7
8036oveq1d 6316 . . . . . . . . . 10
81 oveq1 6308 . . . . . . . . . . 11
8281oveq2d 6317 . . . . . . . . . 10
8380, 82eqeq12d 2444 . . . . . . . . 9
8483imbi2d 317 . . . . . . . 8
8584imbi2d 317 . . . . . . 7
866, 79, 85ghgrplem1OLD 26077 . . . . . 6
8786impancom 441 . . . . 5
8840oveq1d 6316 . . . . . . . 8
89 oveq1 6308 . . . . . . . 8
9088, 89eqeq12d 2444 . . . . . . 7
9190imbi2d 317 . . . . . 6
9291imbi2d 317 . . . . 5
936, 87, 92ghgrplem1OLD 26077 . . . 4
9493ex 435 . . 3
95943imp2 1220 . 2
9610adantr 466 . . . . . . . . . . . 12
972adantr 466 . . . . . . . . . . . . 13
98 simprr 764 . . . . . . . . . . . . 13
99 simprl 762 . . . . . . . . . . . . 13
100 eqid 2422 . . . . . . . . . . . . . 14
1011, 100grpodivcl 25958 . . . . . . . . . . . . 13
10297, 98, 99, 101syl3anc 1264 . . . . . . . . . . . 12
10396, 102ffvelrnd 6034 . . . . . . . . . . 11
104 simpl 458 . . . . . . . . . . . . 13
1056, 27, 23ghgrplem2OLD 26078 . . . . . . . . . . . . 13
106104, 102, 99, 105syl12anc 1262 . . . . . . . . . . . 12
1071, 100grponpcan 25963 . . . . . . . . . . . . . 14
10897, 98, 99, 107syl3anc 1264 . . . . . . . . . . . . 13
109108fveq2d 5881 . . . . . . . . . . . 12
110106, 109eqtr3d 2465 . . . . . . . . . . 11
111 oveq1 6308 . . . . . . . . . . . . 13
112111eqeq1d 2424 . . . . . . . . . . . 12
113112rspcev 3182 . . . . . . . . . . 11
114103, 110, 113syl2anc 665 . . . . . . . . . 10
115 eqid 2422 . . . . . . . . . . . . . . 15
1161, 115grpoinvcl 25937 . . . . . . . . . . . . . 14
11797, 99, 116syl2anc 665 . . . . . . . . . . . . 13
1181grpocl 25911 . . . . . . . . . . . . 13
11997, 117, 98, 118syl3anc 1264 . . . . . . . . . . . 12
12096, 119ffvelrnd 6034 . . . . . . . . . . 11
1216, 27, 23ghgrplem2OLD 26078 . . . . . . . . . . . . 13
122104, 99, 119, 121syl12anc 1262 . . . . . . . . . . . 12
1231, 115grpoasscan1 25948 . . . . . . . . . . . . . 14
12497, 99, 98, 123syl3anc 1264 . . . . . . . . . . . . 13
125124fveq2d 5881 . . . . . . . . . . . 12
126122, 125eqtr3d 2465 . . . . . . . . . . 11
127 oveq2 6309 . . . . . . . . . . . . 13
128127eqeq1d 2424 . . . . . . . . . . . 12
129128rspcev 3182 . . . . . . . . . . 11
130120, 126, 129syl2anc 665 . . . . . . . . . 10
131114, 130jca 534 . . . . . . . . 9
132131expr 618 . . . . . . . 8
133132impancom 441 . . . . . . 7
134 eqeq2 2437 . . . . . . . . . 10
135134rexbidv 2939 . . . . . . . . 9
136 eqeq2 2437 . . . . . . . . . 10
137136rexbidv 2939 . . . . . . . . 9
138135, 137anbi12d 715 . . . . . . . 8
139138imbi2d 317 . . . . . . 7
1406, 133, 139ghgrplem1OLD 26077 . . . . . 6
141140impancom 441 . . . . 5
142 oveq2 6309 . . . . . . . . 9
143142eqeq1d 2424 . . . . . . . 8
144143rexbidv 2939 . . . . . . 7
145 oveq1 6308 . . . . . . . . 9
146145eqeq1d 2424 . . . . . . . 8
147146rexbidv 2939 . . . . . . 7
148144, 147anbi12d 715 . . . . . 6
149148imbi2d 317 . . . . 5
1506, 141, 149ghgrplem1OLD 26077 . . . 4
151150impr 623 . . 3
152151simpld 460 . 2
153151simprd 464 . 2
1548, 16, 46, 95, 152, 153isgrp2d 25946 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   wceq 1437   wcel 1868   wne 2618  wral 2775  wrex 2776  cvv 3081   wss 3436  c0 3761   cxp 4847   crn 4850   cres 4851   wfn 5592  wf 5593  wfo 5595  cfv 5597  (class class class)co 6301  cgr 25897  GIdcgi 25898  cgn 25899   cgs 25900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-1st 6803  df-2nd 6804  df-grpo 25902  df-gid 25903  df-ginv 25904  df-gdiv 25905 This theorem is referenced by:  ghabloOLD  26080  ghsubgolemOLD  26081
 Copyright terms: Public domain W3C validator