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

Theorem ig1pvalOLD 23130
 Description: Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) Obsolete version of ig1pval 23124 as of 25-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ig1pvalOLD.p Poly1
ig1pvalOLD.g idlGen1p
ig1pvalOLD.z
ig1pvalOLD.u LIdeal
ig1pvalOLD.d deg1
ig1pvalOLD.m Monic1p
Assertion
Ref Expression
ig1pvalOLD
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()

Proof of Theorem ig1pvalOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ig1pvalOLD.g . . . 4 idlGen1p
2 elex 3054 . . . . 5
3 fveq2 5865 . . . . . . . . . 10 Poly1 Poly1
4 ig1pvalOLD.p . . . . . . . . . 10 Poly1
53, 4syl6eqr 2503 . . . . . . . . 9 Poly1
65fveq2d 5869 . . . . . . . 8 LIdealPoly1 LIdeal
7 ig1pvalOLD.u . . . . . . . 8 LIdeal
86, 7syl6eqr 2503 . . . . . . 7 LIdealPoly1
95fveq2d 5869 . . . . . . . . . . 11 Poly1
10 ig1pvalOLD.z . . . . . . . . . . 11
119, 10syl6eqr 2503 . . . . . . . . . 10 Poly1
1211sneqd 3980 . . . . . . . . 9 Poly1
1312eqeq2d 2461 . . . . . . . 8 Poly1
14 fveq2 5865 . . . . . . . . . . 11 Monic1p Monic1p
15 ig1pvalOLD.m . . . . . . . . . . 11 Monic1p
1614, 15syl6eqr 2503 . . . . . . . . . 10 Monic1p
1716ineq2d 3634 . . . . . . . . 9 Monic1p
18 fveq2 5865 . . . . . . . . . . . 12 deg1 deg1
19 ig1pvalOLD.d . . . . . . . . . . . 12 deg1
2018, 19syl6eqr 2503 . . . . . . . . . . 11 deg1
2120fveq1d 5867 . . . . . . . . . 10 deg1
2212difeq2d 3551 . . . . . . . . . . . 12 Poly1
2320, 22imaeq12d 5169 . . . . . . . . . . 11 deg1 Poly1
2423supeq1d 7960 . . . . . . . . . 10 deg1 Poly1
2521, 24eqeq12d 2466 . . . . . . . . 9 deg1 deg1 Poly1
2617, 25riotaeqbidv 6255 . . . . . . . 8 Monic1p deg1 deg1 Poly1
2713, 11, 26ifbieq12d 3908 . . . . . . 7 Poly1 Poly1 Monic1p deg1 deg1 Poly1
288, 27mpteq12dv 4481 . . . . . 6 LIdealPoly1 Poly1 Poly1 Monic1p deg1 deg1 Poly1
29 df-ig1pOLD 23085 . . . . . 6 idlGen1p LIdealPoly1 Poly1 Poly1 Monic1p deg1 deg1 Poly1
30 fvex 5875 . . . . . . . 8 LIdeal
317, 30eqeltri 2525 . . . . . . 7
3231mptex 6136 . . . . . 6
3328, 29, 32fvmpt 5948 . . . . 5 idlGen1p
342, 33syl 17 . . . 4 idlGen1p
351, 34syl5eq 2497 . . 3
3635fveq1d 5867 . 2
37 eqeq1 2455 . . . 4
38 ineq1 3627 . . . . 5
39 difeq1 3544 . . . . . . . 8
4039imaeq2d 5168 . . . . . . 7
4140supeq1d 7960 . . . . . 6
4241eqeq2d 2461 . . . . 5
4338, 42riotaeqbidv 6255 . . . 4
4437, 43ifbieq2d 3906 . . 3
45 eqid 2451 . . 3
46 fvex 5875 . . . . 5
4710, 46eqeltri 2525 . . . 4
48 riotaex 6256 . . . 4
4947, 48ifex 3949 . . 3
5044, 45, 49fvmpt 5948 . 2
5136, 50sylan9eq 2505 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1444   wcel 1887  cvv 3045   cdif 3401   cin 3403  cif 3881  csn 3968   cmpt 4461  ccnv 4833  cima 4837  cfv 5582  crio 6251  csup 7954  cr 9538   clt 9675  c0g 15338  LIdealclidl 18393  Poly1cpl1 18770   deg1 cdg1 23003  Monic1pcmn1 23074  idlGen1pcig1pold 23079 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pr 4639 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-sup 7956  df-ig1pOLD 23085 This theorem is referenced by:  ig1pval2OLD  23131  ig1pval3OLD  23132
 Copyright terms: Public domain W3C validator