Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngohomco Structured version   Unicode version

Theorem rngohomco 32175
 Description: The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
rngohomco

Proof of Theorem rngohomco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2423 . . . . . . 7
2 eqid 2423 . . . . . . 7
3 eqid 2423 . . . . . . 7
4 eqid 2423 . . . . . . 7
51, 2, 3, 4rngohomf 32167 . . . . . 6
653expa 1206 . . . . 5
763adantl1 1162 . . . 4
9 eqid 2423 . . . . . . 7
10 eqid 2423 . . . . . . 7
119, 10, 1, 2rngohomf 32167 . . . . . 6
12113expa 1206 . . . . 5
13123adantl3 1164 . . . 4
15 fco 5755 . . 3
168, 14, 15syl2anc 666 . 2
17 eqid 2423 . . . . . . 7
18 eqid 2423 . . . . . . 7 GId GId
1910, 17, 18rngo1cl 26153 . . . . . 6 GId
20193ad2ant1 1027 . . . . 5 GId
2120adantr 467 . . . 4 GId
22 fvco3 5957 . . . 4 GId GId GId
2314, 21, 22syl2anc 666 . . 3 GId GId
24 eqid 2423 . . . . . . . . 9
25 eqid 2423 . . . . . . . . 9 GId GId
2617, 18, 24, 25rngohom1 32169 . . . . . . . 8 GId GId
27263expa 1206 . . . . . . 7 GId GId
28273adantl3 1164 . . . . . 6 GId GId
2928adantrr 722 . . . . 5 GId GId
3029fveq2d 5884 . . . 4 GId GId
31 eqid 2423 . . . . . . . 8
32 eqid 2423 . . . . . . . 8 GId GId
3324, 25, 31, 32rngohom1 32169 . . . . . . 7 GId GId
34333expa 1206 . . . . . 6 GId GId
35343adantl1 1162 . . . . 5 GId GId
3635adantrl 721 . . . 4 GId GId
3730, 36eqtrd 2464 . . 3 GId GId
3823, 37eqtrd 2464 . 2 GId GId
399, 10, 1rngohomadd 32170 . . . . . . . . . . . 12
4039ex 436 . . . . . . . . . . 11
41403expa 1206 . . . . . . . . . 10
42413adantl3 1164 . . . . . . . . 9
4342imp 431 . . . . . . . 8
4443adantlrr 726 . . . . . . 7
4544fveq2d 5884 . . . . . 6
469, 10, 1, 2rngohomcl 32168 . . . . . . . . . . . . 13
479, 10, 1, 2rngohomcl 32168 . . . . . . . . . . . . 13
4846, 47anim12da 32000 . . . . . . . . . . . 12
4948ex 436 . . . . . . . . . . 11
50493expa 1206 . . . . . . . . . 10
51503adantl3 1164 . . . . . . . . 9
5251imp 431 . . . . . . . 8
5352adantlrr 726 . . . . . . 7
541, 2, 3rngohomadd 32170 . . . . . . . . . . . 12
5554ex 436 . . . . . . . . . . 11
56553expa 1206 . . . . . . . . . 10
57563adantl1 1162 . . . . . . . . 9
5857imp 431 . . . . . . . 8
5958adantlrl 725 . . . . . . 7
6053, 59syldan 473 . . . . . 6
6145, 60eqtrd 2464 . . . . 5
629, 10rngogcl 26115 . . . . . . . . 9
63623expb 1207 . . . . . . . 8
64633ad2antl1 1168 . . . . . . 7
6564adantlr 720 . . . . . 6
66 fvco3 5957 . . . . . . 7
6714, 66sylan 474 . . . . . 6
6865, 67syldan 473 . . . . 5
69 fvco3 5957 . . . . . . . 8
7014, 69sylan 474 . . . . . . 7
71 fvco3 5957 . . . . . . . 8
7214, 71sylan 474 . . . . . . 7
7370, 72anim12da 32000 . . . . . 6
74 oveq12 6313 . . . . . 6
7573, 74syl 17 . . . . 5
7661, 68, 753eqtr4d 2474 . . . 4
779, 10, 17, 24rngohommul 32171 . . . . . . . . . . . 12
7877ex 436 . . . . . . . . . . 11
79783expa 1206 . . . . . . . . . 10
80793adantl3 1164 . . . . . . . . 9
8180imp 431 . . . . . . . 8
8281adantlrr 726 . . . . . . 7
8382fveq2d 5884 . . . . . 6
841, 2, 24, 31rngohommul 32171 . . . . . . . . . . . 12
8584ex 436 . . . . . . . . . . 11
86853expa 1206 . . . . . . . . . 10
87863adantl1 1162 . . . . . . . . 9
8887imp 431 . . . . . . . 8
8988adantlrl 725 . . . . . . 7
9053, 89syldan 473 . . . . . 6
9183, 90eqtrd 2464 . . . . 5
929, 17, 10rngocl 26106 . . . . . . . . 9
93923expb 1207 . . . . . . . 8
94933ad2antl1 1168 . . . . . . 7
9594adantlr 720 . . . . . 6
96 fvco3 5957 . . . . . . 7
9714, 96sylan 474 . . . . . 6
9895, 97syldan 473 . . . . 5
99 oveq12 6313 . . . . . 6
10073, 99syl 17 . . . . 5
10191, 98, 1003eqtr4d 2474 . . . 4
10276, 101jca 535 . . 3
103102ralrimivva 2847 . 2
1049, 17, 10, 18, 3, 31, 4, 32isrngohom 32166 . . . 4 GId GId
1051043adant2 1025 . . 3 GId GId
106105adantr 467 . 2 GId GId
10716, 38, 103, 106mpbir3and 1189 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 983   wceq 1438   wcel 1869  wral 2776   crn 4853   ccom 4856  wf 5596  cfv 5600  (class class class)co 6304  c1st 6804  c2nd 6805  GIdcgi 25911  crngo 26099   crnghom 32161 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4219  df-iun 4300  df-br 4423  df-opab 4482  df-mpt 4483  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-fo 5606  df-fv 5608  df-riota 6266  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-1st 6806  df-2nd 6807  df-map 7484  df-grpo 25915  df-gid 25916  df-ablo 26006  df-ass 26037  df-exid 26039  df-mgmOLD 26043  df-sgrOLD 26055  df-mndo 26062  df-rngo 26100  df-rngohom 32164 This theorem is referenced by:  rngoisoco  32183
 Copyright terms: Public domain W3C validator