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

Theorem imasrng 15715
 Description: The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
Hypotheses
Ref Expression
imasrng.u s
imasrng.v
imasrng.p
imasrng.t
imasrng.o
imasrng.f
imasrng.e1
imasrng.e2
imasrng.r
Assertion
Ref Expression
imasrng
Distinct variable groups:   ,,   ,,,,   ,,,,   ,,   ,,   ,,,,   ,,   ,,,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)

Proof of Theorem imasrng
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasrng.u . . . 4 s
2 imasrng.v . . . 4
3 imasrng.f . . . 4
4 imasrng.r . . . 4
51, 2, 3, 4imasbas 13728 . . 3
6 eqidd 2436 . . 3
7 eqidd 2436 . . 3
8 imasrng.p . . . . . 6
98a1i 11 . . . . 5
10 imasrng.e1 . . . . 5
11 rnggrp 15659 . . . . . 6
124, 11syl 16 . . . . 5
13 eqid 2435 . . . . 5
141, 2, 9, 3, 10, 12, 13imasgrp 14924 . . . 4
1514simpld 446 . . 3
16 imasrng.e2 . . . . 5
17 imasrng.t . . . . 5
18 eqid 2435 . . . . 5
194adantr 452 . . . . . . . 8
20 simprl 733 . . . . . . . . 9
212adantr 452 . . . . . . . . 9
2220, 21eleqtrd 2511 . . . . . . . 8
23 simprr 734 . . . . . . . . 9
2423, 21eleqtrd 2511 . . . . . . . 8
25 eqid 2435 . . . . . . . . 9
2625, 17rngcl 15667 . . . . . . . 8
2719, 22, 24, 26syl3anc 1184 . . . . . . 7
2827, 21eleqtrrd 2512 . . . . . 6
2928caovclg 6231 . . . . 5
303, 16, 1, 2, 4, 17, 18, 29imasmulf 13751 . . . 4
31 fovrn 6208 . . . 4
3230, 31syl3an1 1217 . . 3
33 forn 5648 . . . . . . . . . 10
343, 33syl 16 . . . . . . . . 9
3534eleq2d 2502 . . . . . . . 8
3634eleq2d 2502 . . . . . . . 8
3734eleq2d 2502 . . . . . . . 8
3835, 36, 373anbi123d 1254 . . . . . . 7
39 fofn 5647 . . . . . . . . 9
403, 39syl 16 . . . . . . . 8
41 fvelrnb 5766 . . . . . . . . 9
42 fvelrnb 5766 . . . . . . . . 9
43 fvelrnb 5766 . . . . . . . . 9
4441, 42, 433anbi123d 1254 . . . . . . . 8
4540, 44syl 16 . . . . . . 7
4638, 45bitr3d 247 . . . . . 6
47 3reeanv 2868 . . . . . 6
4846, 47syl6bbr 255 . . . . 5
494adantr 452 . . . . . . . . . . . . . 14
50 simp2 958 . . . . . . . . . . . . . . . 16
5123ad2ant1 978 . . . . . . . . . . . . . . . 16
5250, 51eleqtrd 2511 . . . . . . . . . . . . . . 15
53523adant3r3 1164 . . . . . . . . . . . . . 14
54 simp3 959 . . . . . . . . . . . . . . . 16
5554, 51eleqtrd 2511 . . . . . . . . . . . . . . 15
56553adant3r3 1164 . . . . . . . . . . . . . 14
57 simpr3 965 . . . . . . . . . . . . . . 15
582adantr 452 . . . . . . . . . . . . . . 15
5957, 58eleqtrd 2511 . . . . . . . . . . . . . 14
6025, 17rngass 15670 . . . . . . . . . . . . . 14
6149, 53, 56, 59, 60syl13anc 1186 . . . . . . . . . . . . 13
6261fveq2d 5724 . . . . . . . . . . . 12
63 simpl 444 . . . . . . . . . . . . 13
6428caovclg 6231 . . . . . . . . . . . . . 14
65643adantr3 1118 . . . . . . . . . . . . 13
663, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
6763, 65, 57, 66syl3anc 1184 . . . . . . . . . . . 12
68 simpr1 963 . . . . . . . . . . . . 13
6928caovclg 6231 . . . . . . . . . . . . . 14
70693adantr1 1116 . . . . . . . . . . . . 13
713, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
7263, 68, 70, 71syl3anc 1184 . . . . . . . . . . . 12
7362, 67, 723eqtr4d 2477 . . . . . . . . . . 11
743, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
75743adant3r3 1164 . . . . . . . . . . . 12
7675oveq1d 6088 . . . . . . . . . . 11
773, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
78773adant3r1 1162 . . . . . . . . . . . 12
7978oveq2d 6089 . . . . . . . . . . 11
8073, 76, 793eqtr4d 2477 . . . . . . . . . 10
81 simp1 957 . . . . . . . . . . . . 13
82 simp2 958 . . . . . . . . . . . . 13
8381, 82oveq12d 6091 . . . . . . . . . . . 12
84 simp3 959 . . . . . . . . . . . 12
8583, 84oveq12d 6091 . . . . . . . . . . 11
8682, 84oveq12d 6091 . . . . . . . . . . . 12
8781, 86oveq12d 6091 . . . . . . . . . . 11
8885, 87eqeq12d 2449 . . . . . . . . . 10
8980, 88syl5ibcom 212 . . . . . . . . 9
90893exp2 1171 . . . . . . . 8
9190imp32 423 . . . . . . 7
9291rexlimdv 2821 . . . . . 6
9392rexlimdvva 2829 . . . . 5
9448, 93sylbid 207 . . . 4
9594imp 419 . . 3
9625, 8, 17rngdi 15672 . . . . . . . . . . . . . 14
9749, 53, 56, 59, 96syl13anc 1186 . . . . . . . . . . . . 13
9897fveq2d 5724 . . . . . . . . . . . 12
9925, 8rngacl 15681 . . . . . . . . . . . . . . . . 17
10019, 22, 24, 99syl3anc 1184 . . . . . . . . . . . . . . . 16
101100, 21eleqtrrd 2512 . . . . . . . . . . . . . . 15
102101caovclg 6231 . . . . . . . . . . . . . 14
1031023adantr1 1116 . . . . . . . . . . . . 13
1043, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
10563, 68, 103, 104syl3anc 1184 . . . . . . . . . . . 12
10628caovclg 6231 . . . . . . . . . . . . . 14
1071063adantr2 1117 . . . . . . . . . . . . 13
108 eqid 2435 . . . . . . . . . . . . . 14
1093, 10, 1, 2, 4, 8, 108imasaddval 13747 . . . . . . . . . . . . 13
11063, 65, 107, 109syl3anc 1184 . . . . . . . . . . . 12
11198, 105, 1103eqtr4d 2477 . . . . . . . . . . 11
1123, 10, 1, 2, 4, 8, 108imasaddval 13747 . . . . . . . . . . . . 13
1131123adant3r1 1162 . . . . . . . . . . . 12
114113oveq2d 6089 . . . . . . . . . . 11
1153, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
1161153adant3r2 1163 . . . . . . . . . . . 12
11775, 116oveq12d 6091 . . . . . . . . . . 11
118111, 114, 1173eqtr4d 2477 . . . . . . . . . 10
11982, 84oveq12d 6091 . . . . . . . . . . . 12
12081, 119oveq12d 6091 . . . . . . . . . . 11
12181, 84oveq12d 6091 . . . . . . . . . . . 12
12283, 121oveq12d 6091 . . . . . . . . . . 11
123120, 122eqeq12d 2449 . . . . . . . . . 10
124118, 123syl5ibcom 212 . . . . . . . . 9
1251243exp2 1171 . . . . . . . 8
126125imp32 423 . . . . . . 7
127126rexlimdv 2821 . . . . . 6
128127rexlimdvva 2829 . . . . 5
12948, 128sylbid 207 . . . 4
130129imp 419 . . 3
13125, 8, 17rngdir 15673 . . . . . . . . . . . . . 14
13249, 53, 56, 59, 131syl13anc 1186 . . . . . . . . . . . . 13
133132fveq2d 5724 . . . . . . . . . . . 12
134101caovclg 6231 . . . . . . . . . . . . . 14
1351343adantr3 1118 . . . . . . . . . . . . 13
1363, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . . . . . 13
13763, 135, 57, 136syl3anc 1184 . . . . . . . . . . . 12
1383, 10, 1, 2, 4, 8, 108imasaddval 13747 . . . . . . . . . . . . 13
13963, 107, 70, 138syl3anc 1184 . . . . . . . . . . . 12
140133, 137, 1393eqtr4d 2477 . . . . . . . . . . 11
1413, 10, 1, 2, 4, 8, 108imasaddval 13747 . . . . . . . . . . . . 13
1421413adant3r3 1164 . . . . . . . . . . . 12
143142oveq1d 6088 . . . . . . . . . . 11
144116, 78oveq12d 6091 . . . . . . . . . . 11
145140, 143, 1443eqtr4d 2477 . . . . . . . . . 10
14681, 82oveq12d 6091 . . . . . . . . . . . 12
147146, 84oveq12d 6091 . . . . . . . . . . 11
148121, 86oveq12d 6091 . . . . . . . . . . 11
149147, 148eqeq12d 2449 . . . . . . . . . 10
150145, 149syl5ibcom 212 . . . . . . . . 9
1511503exp2 1171 . . . . . . . 8
152151imp32 423 . . . . . . 7
153152rexlimdv 2821 . . . . . 6
154153rexlimdvva 2829 . . . . 5
15548, 154sylbid 207 . . . 4
156155imp 419 . . 3
157 fof 5645 . . . . 5
1583, 157syl 16 . . . 4
159 imasrng.o . . . . . . 7
16025, 159rngidcl 15674 . . . . . 6
1614, 160syl 16 . . . . 5
162161, 2eleqtrrd 2512 . . . 4
163158, 162ffvelrnd 5863 . . 3
16440, 41syl 16 . . . . . 6
16535, 164bitr3d 247 . . . . 5
166 simpl 444 . . . . . . . . 9
167162adantr 452 . . . . . . . . 9
168 simpr 448 . . . . . . . . 9
1693, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . 9
170166, 167, 168, 169syl3anc 1184 . . . . . . . 8
1714adantr 452 . . . . . . . . . 10
1722eleq2d 2502 . . . . . . . . . . 11
173172biimpa 471 . . . . . . . . . 10
17425, 17, 159rnglidm 15677 . . . . . . . . . 10
175171, 173, 174syl2anc 643 . . . . . . . . 9
176175fveq2d 5724 . . . . . . . 8
177170, 176eqtrd 2467 . . . . . . 7
178 oveq2 6081 . . . . . . . 8
179 id 20 . . . . . . . 8
180178, 179eqeq12d 2449 . . . . . . 7
181177, 180syl5ibcom 212 . . . . . 6
182181rexlimdva 2822 . . . . 5
183165, 182sylbid 207 . . . 4
184183imp 419 . . 3
1853, 16, 1, 2, 4, 17, 18imasmulval 13750 . . . . . . . . 9
186167, 185mpd3an3 1280 . . . . . . . 8
18725, 17, 159rngridm 15678 . . . . . . . . . 10
188171, 173, 187syl2anc 643 . . . . . . . . 9
189188fveq2d 5724 . . . . . . . 8
190186, 189eqtrd 2467 . . . . . . 7
191 oveq1 6080 . . . . . . . 8
192191, 179eqeq12d 2449 . . . . . . 7
193190, 192syl5ibcom 212 . . . . . 6
194193rexlimdva 2822 . . . . 5
195165, 194sylbid 207 . . . 4
196195imp 419 . . 3
1975, 6, 7, 15, 32, 95, 130, 156, 163, 184, 196isrngd 15688 . 2
198163, 5eleqtrd 2511 . . . 4
1995eleq2d 2502 . . . . . 6
200183, 195jcad 520 . . . . . 6
201199, 200sylbird 227 . . . . 5
202201ralrimiv 2780 . . . 4
203 eqid 2435 . . . . . 6
204 eqid 2435 . . . . . 6
205203, 18, 204isrngid 15679 . . . . 5
206197, 205syl 16 . . . 4
207198, 202, 206mpbi2and 888 . . 3
208207eqcomd 2440 . 2
209197, 208jca 519 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2697  wrex 2698   cxp 4868   crn 4871   wfn 5441  wf 5442  wfo 5444  cfv 5446  (class class class)co 6073  cbs 13459   cplusg 13519  cmulr 13520  c0g 13713   s cimas 13720  cgrp 14675  crg 15650  cur 15652 This theorem is referenced by:  divsrng2  15716 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9036  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056  ax-pre-mulgt0 9057 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-oadd 6720  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-sup 7438  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116  df-sub 9283  df-neg 9284  df-nn 9991  df-2 10048  df-3 10049  df-4 10050  df-5 10051  df-6 10052  df-7 10053  df-8 10054  df-9 10055  df-10 10056  df-n0 10212  df-z 10273  df-dec 10373  df-uz 10479  df-fz 11034  df-struct 13461  df-ndx 13462  df-slot 13463  df-base 13464  df-sets 13465  df-plusg 13532  df-mulr 13533  df-sca 13535  df-vsca 13536  df-tset 13538  df-ple 13539  df-ds 13541  df-0g 13717  df-imas 13724  df-mnd 14680  df-grp 14802  df-minusg 14803  df-mgp 15639  df-rng 15653  df-ur 15655
 Copyright terms: Public domain W3C validator