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

Theorem hbtlem1 40064
 Description: Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015.)
Hypotheses
Ref Expression
hbtlem.p 𝑃 = (Poly1𝑅)
hbtlem.u 𝑈 = (LIdeal‘𝑃)
hbtlem.s 𝑆 = (ldgIdlSeq‘𝑅)
hbtlem.d 𝐷 = ( deg1𝑅)
Assertion
Ref Expression
hbtlem1 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → ((𝑆𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))})
Distinct variable groups:   𝑗,𝐼,𝑘   𝑅,𝑗,𝑘   𝑗,𝑋,𝑘
Allowed substitution hints:   𝐷(𝑗,𝑘)   𝑃(𝑗,𝑘)   𝑆(𝑗,𝑘)   𝑈(𝑗,𝑘)   𝑉(𝑗,𝑘)

Proof of Theorem hbtlem1
Dummy variables 𝑖 𝑟 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hbtlem.s . . . . . 6 𝑆 = (ldgIdlSeq‘𝑅)
2 elex 3462 . . . . . . 7 (𝑅𝑉𝑅 ∈ V)
3 fveq2 6649 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (Poly1𝑟) = (Poly1𝑅))
4 hbtlem.p . . . . . . . . . . . 12 𝑃 = (Poly1𝑅)
53, 4eqtr4di 2854 . . . . . . . . . . 11 (𝑟 = 𝑅 → (Poly1𝑟) = 𝑃)
65fveq2d 6653 . . . . . . . . . 10 (𝑟 = 𝑅 → (LIdeal‘(Poly1𝑟)) = (LIdeal‘𝑃))
7 hbtlem.u . . . . . . . . . 10 𝑈 = (LIdeal‘𝑃)
86, 7eqtr4di 2854 . . . . . . . . 9 (𝑟 = 𝑅 → (LIdeal‘(Poly1𝑟)) = 𝑈)
9 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑅 → ( deg1𝑟) = ( deg1𝑅))
10 hbtlem.d . . . . . . . . . . . . . . . 16 𝐷 = ( deg1𝑅)
119, 10eqtr4di 2854 . . . . . . . . . . . . . . 15 (𝑟 = 𝑅 → ( deg1𝑟) = 𝐷)
1211fveq1d 6651 . . . . . . . . . . . . . 14 (𝑟 = 𝑅 → (( deg1𝑟)‘𝑘) = (𝐷𝑘))
1312breq1d 5043 . . . . . . . . . . . . 13 (𝑟 = 𝑅 → ((( deg1𝑟)‘𝑘) ≤ 𝑥 ↔ (𝐷𝑘) ≤ 𝑥))
1413anbi1d 632 . . . . . . . . . . . 12 (𝑟 = 𝑅 → (((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥)) ↔ ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))))
1514rexbidv 3259 . . . . . . . . . . 11 (𝑟 = 𝑅 → (∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥)) ↔ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))))
1615abbidv 2865 . . . . . . . . . 10 (𝑟 = 𝑅 → {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))} = {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})
1716mpteq2dv 5129 . . . . . . . . 9 (𝑟 = 𝑅 → (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}) = (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))
188, 17mpteq12dv 5118 . . . . . . . 8 (𝑟 = 𝑅 → (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})) = (𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
19 df-ldgis 40063 . . . . . . . 8 ldgIdlSeq = (𝑟 ∈ V ↦ (𝑖 ∈ (LIdeal‘(Poly1𝑟)) ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((( deg1𝑟)‘𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
2018, 19, 7mptfvmpt 6972 . . . . . . 7 (𝑅 ∈ V → (ldgIdlSeq‘𝑅) = (𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
212, 20syl 17 . . . . . 6 (𝑅𝑉 → (ldgIdlSeq‘𝑅) = (𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
221, 21syl5eq 2848 . . . . 5 (𝑅𝑉𝑆 = (𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})))
2322fveq1d 6651 . . . 4 (𝑅𝑉 → (𝑆𝐼) = ((𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))‘𝐼))
2423fveq1d 6651 . . 3 (𝑅𝑉 → ((𝑆𝐼)‘𝑋) = (((𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))‘𝐼)‘𝑋))
25243ad2ant1 1130 . 2 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → ((𝑆𝐼)‘𝑋) = (((𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))‘𝐼)‘𝑋))
26 rexeq 3362 . . . . . . 7 (𝑖 = 𝐼 → (∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥)) ↔ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))))
2726abbidv 2865 . . . . . 6 (𝑖 = 𝐼 → {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))} = {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})
2827mpteq2dv 5129 . . . . 5 (𝑖 = 𝐼 → (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}) = (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))
29 eqid 2801 . . . . 5 (𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})) = (𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))
30 nn0ex 11895 . . . . . 6 0 ∈ V
3130mptex 6967 . . . . 5 (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}) ∈ V
3228, 29, 31fvmpt 6749 . . . 4 (𝐼𝑈 → ((𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))‘𝐼) = (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))
3332fveq1d 6651 . . 3 (𝐼𝑈 → (((𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))‘𝐼)‘𝑋) = ((𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})‘𝑋))
34333ad2ant2 1131 . 2 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → (((𝑖𝑈 ↦ (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝑖 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}))‘𝐼)‘𝑋) = ((𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})‘𝑋))
35 eqid 2801 . . 3 (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))}) = (𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})
36 breq2 5037 . . . . . 6 (𝑥 = 𝑋 → ((𝐷𝑘) ≤ 𝑥 ↔ (𝐷𝑘) ≤ 𝑋))
37 fveq2 6649 . . . . . . 7 (𝑥 = 𝑋 → ((coe1𝑘)‘𝑥) = ((coe1𝑘)‘𝑋))
3837eqeq2d 2812 . . . . . 6 (𝑥 = 𝑋 → (𝑗 = ((coe1𝑘)‘𝑥) ↔ 𝑗 = ((coe1𝑘)‘𝑋)))
3936, 38anbi12d 633 . . . . 5 (𝑥 = 𝑋 → (((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥)) ↔ ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))))
4039rexbidv 3259 . . . 4 (𝑥 = 𝑋 → (∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥)) ↔ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))))
4140abbidv 2865 . . 3 (𝑥 = 𝑋 → {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))} = {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))})
42 simp3 1135 . . 3 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → 𝑋 ∈ ℕ0)
43 simpr 488 . . . . . 6 (((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋)) → 𝑗 = ((coe1𝑘)‘𝑋))
4443reximi 3209 . . . . 5 (∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋)) → ∃𝑘𝐼 𝑗 = ((coe1𝑘)‘𝑋))
4544ss2abi 3997 . . . 4 {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))} ⊆ {𝑗 ∣ ∃𝑘𝐼 𝑗 = ((coe1𝑘)‘𝑋)}
46 abrexexg 7648 . . . . 5 (𝐼𝑈 → {𝑗 ∣ ∃𝑘𝐼 𝑗 = ((coe1𝑘)‘𝑋)} ∈ V)
47463ad2ant2 1131 . . . 4 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → {𝑗 ∣ ∃𝑘𝐼 𝑗 = ((coe1𝑘)‘𝑋)} ∈ V)
48 ssexg 5194 . . . 4 (({𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))} ⊆ {𝑗 ∣ ∃𝑘𝐼 𝑗 = ((coe1𝑘)‘𝑋)} ∧ {𝑗 ∣ ∃𝑘𝐼 𝑗 = ((coe1𝑘)‘𝑋)} ∈ V) → {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))} ∈ V)
4945, 47, 48sylancr 590 . . 3 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))} ∈ V)
5035, 41, 42, 49fvmptd3 6772 . 2 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → ((𝑥 ∈ ℕ0 ↦ {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑥𝑗 = ((coe1𝑘)‘𝑥))})‘𝑋) = {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))})
5125, 34, 503eqtrd 2840 1 ((𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0) → ((𝑆𝐼)‘𝑋) = {𝑗 ∣ ∃𝑘𝐼 ((𝐷𝑘) ≤ 𝑋𝑗 = ((coe1𝑘)‘𝑋))})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2112  {cab 2779  ∃wrex 3110  Vcvv 3444   ⊆ wss 3884   class class class wbr 5033   ↦ cmpt 5113  ‘cfv 6328   ≤ cle 10669  ℕ0cn0 11889  LIdealclidl 19939  Poly1cpl1 20810  coe1cco1 20811   deg1 cdg1 24659  ldgIdlSeqcldgis 40062 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-1cn 10588  ax-addcl 10590 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630  df-n0 11890  df-ldgis 40063 This theorem is referenced by:  hbtlem2  40065  hbtlem4  40067  hbtlem3  40068  hbtlem5  40069  hbtlem6  40070
 Copyright terms: Public domain W3C validator