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

Theorem ig1pval 23124
 Description: Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.)
Hypotheses
Ref Expression
ig1pval.p Poly1
ig1pval.g idlGen1p
ig1pval.z
ig1pval.u LIdeal
ig1pval.d deg1
ig1pval.m Monic1p
Assertion
Ref Expression
ig1pval inf
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()

Proof of Theorem ig1pval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ig1pval.g . . . 4 idlGen1p
2 elex 3054 . . . . 5
3 fveq2 5865 . . . . . . . . . 10 Poly1 Poly1
4 ig1pval.p . . . . . . . . . 10 Poly1
53, 4syl6eqr 2503 . . . . . . . . 9 Poly1
65fveq2d 5869 . . . . . . . 8 LIdealPoly1 LIdeal
7 ig1pval.u . . . . . . . 8 LIdeal
86, 7syl6eqr 2503 . . . . . . 7 LIdealPoly1
95fveq2d 5869 . . . . . . . . . . 11 Poly1
10 ig1pval.z . . . . . . . . . . 11
119, 10syl6eqr 2503 . . . . . . . . . 10 Poly1
1211sneqd 3980 . . . . . . . . 9 Poly1
1312eqeq2d 2461 . . . . . . . 8 Poly1
14 fveq2 5865 . . . . . . . . . . 11 Monic1p Monic1p
15 ig1pval.m . . . . . . . . . . 11 Monic1p
1614, 15syl6eqr 2503 . . . . . . . . . 10 Monic1p
1716ineq2d 3634 . . . . . . . . 9 Monic1p
18 fveq2 5865 . . . . . . . . . . . 12 deg1 deg1
19 ig1pval.d . . . . . . . . . . . 12 deg1
2018, 19syl6eqr 2503 . . . . . . . . . . 11 deg1
2120fveq1d 5867 . . . . . . . . . 10 deg1
2212difeq2d 3551 . . . . . . . . . . . 12 Poly1
2320, 22imaeq12d 5169 . . . . . . . . . . 11 deg1 Poly1
2423infeq1d 7993 . . . . . . . . . 10 inf deg1 Poly1 inf
2521, 24eqeq12d 2466 . . . . . . . . 9 deg1 inf deg1 Poly1 inf
2617, 25riotaeqbidv 6255 . . . . . . . 8 Monic1p deg1 inf deg1 Poly1 inf
2713, 11, 26ifbieq12d 3908 . . . . . . 7 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 inf
288, 27mpteq12dv 4481 . . . . . 6 LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1 inf
29 df-ig1p 23084 . . . . . 6 idlGen1p LIdealPoly1 Poly1 Poly1 Monic1p deg1 inf deg1 Poly1
30 fvex 5875 . . . . . . . 8 LIdeal
317, 30eqeltri 2525 . . . . . . 7
3231mptex 6136 . . . . . 6 inf
3328, 29, 32fvmpt 5948 . . . . 5 idlGen1p inf
342, 33syl 17 . . . 4 idlGen1p inf
351, 34syl5eq 2497 . . 3 inf
3635fveq1d 5867 . 2 inf
37 eqeq1 2455 . . . 4
38 ineq1 3627 . . . . 5
39 difeq1 3544 . . . . . . . 8
4039imaeq2d 5168 . . . . . . 7
4140infeq1d 7993 . . . . . 6 inf inf
4241eqeq2d 2461 . . . . 5 inf inf
4338, 42riotaeqbidv 6255 . . . 4 inf inf
4437, 43ifbieq2d 3906 . . 3 inf inf
45 eqid 2451 . . 3 inf inf
46 fvex 5875 . . . . 5
4710, 46eqeltri 2525 . . . 4
48 riotaex 6256 . . . 4 inf
4947, 48ifex 3949 . . 3 inf
5044, 45, 49fvmpt 5948 . 2 inf inf
5136, 50sylan9eq 2505 1 inf
 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  cima 4837  cfv 5582  crio 6251  infcinf 7955  cr 9538   clt 9675  c0g 15338  LIdealclidl 18393  Poly1cpl1 18770   deg1 cdg1 23003  Monic1pcmn1 23074  idlGen1pcig1p 23078 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-inf 7957  df-ig1p 23084 This theorem is referenced by:  ig1pval2  23125  ig1pval3  23126
 Copyright terms: Public domain W3C validator