Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mzpsubst Structured version   Unicode version

Theorem mzpsubst 26819
 Description: Substituting polynomials for the variables of a polynomial results in a polynomial. is expected to depend on and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014.)
Assertion
Ref Expression
mzpsubst mzPoly mzPoly mzPoly
Distinct variable groups:   ,,   ,   ,,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem mzpsubst
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 958 . 2 mzPoly mzPoly
2 elfvex 5761 . . 3 mzPoly
323ad2ant2 980 . 2 mzPoly mzPoly
4 simp3 960 . 2 mzPoly mzPoly mzPoly
5 simp2 959 . 2 mzPoly mzPoly mzPoly
6 simpr 449 . . . . . . 7 mzPoly
7 simpll3 999 . . . . . . 7 mzPoly mzPoly
8 simpll2 998 . . . . . . 7 mzPoly
9 mzpf 26807 . . . . . . . . . . . . . 14 mzPoly
109ffvelrnda 5873 . . . . . . . . . . . . 13 mzPoly
1110expcom 426 . . . . . . . . . . . 12 mzPoly
1211ralimdv 2787 . . . . . . . . . . 11 mzPoly
1312imp 420 . . . . . . . . . 10 mzPoly
14 eqid 2438 . . . . . . . . . . 11
1514fmpt 5893 . . . . . . . . . 10
1613, 15sylib 190 . . . . . . . . 9 mzPoly
1716adantr 453 . . . . . . . 8 mzPoly
18 zex 10296 . . . . . . . . 9
19 simpr 449 . . . . . . . . 9 mzPoly
20 elmapg 7034 . . . . . . . . 9
2118, 19, 20sylancr 646 . . . . . . . 8 mzPoly
2217, 21mpbird 225 . . . . . . 7 mzPoly
236, 7, 8, 22syl21anc 1184 . . . . . 6 mzPoly
24 vex 2961 . . . . . . 7
2524fvconst2 5950 . . . . . 6
2623, 25syl 16 . . . . 5 mzPoly
2726mpteq2dva 4298 . . . 4 mzPoly
28 mzpconstmpt 26811 . . . . 5 mzPoly
29283ad2antl1 1120 . . . 4 mzPoly mzPoly
3027, 29eqeltrd 2512 . . 3 mzPoly mzPoly
31 simpr 449 . . . . . . . . 9 mzPoly
32 simpll3 999 . . . . . . . . 9 mzPoly mzPoly
33 simpll2 998 . . . . . . . . 9 mzPoly
3431, 32, 33, 22syl21anc 1184 . . . . . . . 8 mzPoly
35 fveq1 5730 . . . . . . . . 9
36 eqid 2438 . . . . . . . . 9
37 fvex 5745 . . . . . . . . 9
3835, 36, 37fvmpt 5809 . . . . . . . 8
3934, 38syl 16 . . . . . . 7 mzPoly
40 simplr 733 . . . . . . . 8 mzPoly
41 fvex 5745 . . . . . . . 8
42 csbeq1 3256 . . . . . . . . . 10
4342fveq1d 5733 . . . . . . . . 9
44 nfcv 2574 . . . . . . . . . 10
45 nfcsb1v 3285 . . . . . . . . . . 11
46 nfcv 2574 . . . . . . . . . . 11
4745, 46nffv 5738 . . . . . . . . . 10
48 csbeq1a 3261 . . . . . . . . . . 11
4948fveq1d 5733 . . . . . . . . . 10
5044, 47, 49cbvmpt 4302 . . . . . . . . 9
5143, 50fvmptg 5807 . . . . . . . 8
5240, 41, 51sylancl 645 . . . . . . 7 mzPoly
5339, 52eqtrd 2470 . . . . . 6 mzPoly
5453mpteq2dva 4298 . . . . 5 mzPoly
55 simpr 449 . . . . . . . 8 mzPoly
56 simpl3 963 . . . . . . . 8 mzPoly mzPoly
57 nfcsb1v 3285 . . . . . . . . . 10
5857nfel1 2584 . . . . . . . . 9 mzPoly
59 csbeq1a 3261 . . . . . . . . . 10
6059eleq1d 2504 . . . . . . . . 9 mzPoly mzPoly
6158, 60rspc 3048 . . . . . . . 8 mzPoly mzPoly
6255, 56, 61sylc 59 . . . . . . 7 mzPoly mzPoly
63 mzpf 26807 . . . . . . 7 mzPoly
6462, 63syl 16 . . . . . 6 mzPoly
6564feqmptd 5782 . . . . 5 mzPoly
6654, 65eqtr4d 2473 . . . 4 mzPoly
6766, 62eqeltrd 2512 . . 3 mzPoly mzPoly
68 simp2l 984 . . . . . 6 mzPoly mzPoly mzPoly
69 ffn 5594 . . . . . 6
7068, 69syl 16 . . . . 5 mzPoly mzPoly mzPoly
71 simp3l 986 . . . . . 6 mzPoly mzPoly mzPoly
72 ffn 5594 . . . . . 6
7371, 72syl 16 . . . . 5 mzPoly mzPoly mzPoly
74 simp13 990 . . . . 5 mzPoly mzPoly mzPoly mzPoly
75 simp12 989 . . . . 5 mzPoly mzPoly mzPoly
76 simplll 736 . . . . . . 7 mzPoly
77 simpllr 737 . . . . . . 7 mzPoly
78 ovex 6109 . . . . . . . 8
7978a1i 11 . . . . . . 7 mzPoly
80 simpr 449 . . . . . . . . . 10 mzPoly
81 simplrl 738 . . . . . . . . . 10 mzPoly mzPoly
8280, 81, 12sylc 59 . . . . . . . . 9 mzPoly
8382, 15sylib 190 . . . . . . . 8 mzPoly
84 simplrr 739 . . . . . . . . 9 mzPoly
8518, 84, 20sylancr 646 . . . . . . . 8 mzPoly
8683, 85mpbird 225 . . . . . . 7 mzPoly
87 fnfvof 6320 . . . . . . 7
8876, 77, 79, 86, 87syl22anc 1186 . . . . . 6 mzPoly
8988mpteq2dva 4298 . . . . 5 mzPoly
9070, 73, 74, 75, 89syl22anc 1186 . . . 4 mzPoly mzPoly mzPoly
91 simp2r 985 . . . . 5 mzPoly mzPoly mzPoly mzPoly
92 simp3r 987 . . . . 5 mzPoly mzPoly mzPoly mzPoly
93 mzpaddmpt 26812 . . . . 5 mzPoly mzPoly mzPoly
9491, 92, 93syl2anc 644 . . . 4 mzPoly mzPoly mzPoly mzPoly
9590, 94eqeltrd 2512 . . 3 mzPoly mzPoly mzPoly mzPoly
96 fnfvof 6320 . . . . . . 7
9776, 77, 79, 86, 96syl22anc 1186 . . . . . 6 mzPoly
9897mpteq2dva 4298 . . . . 5 mzPoly
9970, 73, 74, 75, 98syl22anc 1186 . . . 4 mzPoly mzPoly mzPoly
100 mzpmulmpt 26813 . . . . 5 mzPoly mzPoly mzPoly
10191, 92, 100syl2anc 644 . . . 4 mzPoly mzPoly mzPoly mzPoly
10299, 101eqeltrd 2512 . . 3 mzPoly mzPoly mzPoly mzPoly
103 fveq1 5730 . . . . 5
104103mpteq2dv 4299 . . . 4
105104eleq1d 2504 . . 3 mzPoly mzPoly
106 fveq1 5730 . . . . 5
107106mpteq2dv 4299 . . . 4
108107eleq1d 2504 . . 3 mzPoly mzPoly
109 fveq1 5730 . . . . 5
110109mpteq2dv 4299 . . . 4
111110eleq1d 2504 . . 3 mzPoly mzPoly
112 fveq1 5730 . . . . 5
113112mpteq2dv 4299 . . . 4
114113eleq1d 2504 . . 3 mzPoly mzPoly
115 fveq1 5730 . . . . 5
116115mpteq2dv 4299 . . . 4
117116eleq1d 2504 . . 3 mzPoly mzPoly
118 fveq1 5730 . . . . 5
119118mpteq2dv 4299 . . . 4
120119eleq1d 2504 . . 3 mzPoly mzPoly
121 fveq1 5730 . . . . 5
122121mpteq2dv 4299 . . . 4
123122eleq1d 2504 . . 3 mzPoly mzPoly
12430, 67, 95, 102, 105, 108, 111, 114, 117, 120, 123mzpindd 26817 . 2 mzPoly mzPoly mzPoly
1251, 3, 4, 5, 124syl31anc 1188 1 mzPoly mzPoly mzPoly
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   w3a 937   wceq 1653   wcel 1726  wral 2707  cvv 2958  csb 3253  csn 3816   cmpt 4269   cxp 4879   wfn 5452  wf 5453  cfv 5457  (class class class)co 6084   cof 6306   cmap 7021   caddc 8998   cmul 9000  cz 10287  mzPolycmzp 26793 This theorem is referenced by:  mzprename  26820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6308  df-riota 6552  df-recs 6636  df-rdg 6671  df-er 6908  df-map 7023  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-nn 10006  df-n0 10227  df-z 10288  df-mzpcl 26794  df-mzp 26795
 Copyright terms: Public domain W3C validator