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

Theorem hbtlem6 41856
Description: There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015.)
Hypotheses
Ref Expression
hbtlem.p 𝑃 = (Poly1β€˜π‘…)
hbtlem.u π‘ˆ = (LIdealβ€˜π‘ƒ)
hbtlem.s 𝑆 = (ldgIdlSeqβ€˜π‘…)
hbtlem6.n 𝑁 = (RSpanβ€˜π‘ƒ)
hbtlem6.r (πœ‘ β†’ 𝑅 ∈ LNoeR)
hbtlem6.i (πœ‘ β†’ 𝐼 ∈ π‘ˆ)
hbtlem6.x (πœ‘ β†’ 𝑋 ∈ β„•0)
Assertion
Ref Expression
hbtlem6 (πœ‘ β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
Distinct variable groups:   πœ‘,π‘˜   π‘˜,𝐼   𝑅,π‘˜   𝑆,π‘˜   π‘˜,𝑋
Allowed substitution hints:   𝑃(π‘˜)   π‘ˆ(π‘˜)   𝑁(π‘˜)

Proof of Theorem hbtlem6
Dummy variables π‘Ž 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hbtlem6.r . . 3 (πœ‘ β†’ 𝑅 ∈ LNoeR)
2 lnrring 41839 . . . . 5 (𝑅 ∈ LNoeR β†’ 𝑅 ∈ Ring)
31, 2syl 17 . . . 4 (πœ‘ β†’ 𝑅 ∈ Ring)
4 hbtlem6.i . . . 4 (πœ‘ β†’ 𝐼 ∈ π‘ˆ)
5 hbtlem6.x . . . 4 (πœ‘ β†’ 𝑋 ∈ β„•0)
6 hbtlem.p . . . . 5 𝑃 = (Poly1β€˜π‘…)
7 hbtlem.u . . . . 5 π‘ˆ = (LIdealβ€˜π‘ƒ)
8 hbtlem.s . . . . 5 𝑆 = (ldgIdlSeqβ€˜π‘…)
9 eqid 2732 . . . . 5 (LIdealβ€˜π‘…) = (LIdealβ€˜π‘…)
106, 7, 8, 9hbtlem2 41851 . . . 4 ((𝑅 ∈ Ring ∧ 𝐼 ∈ π‘ˆ ∧ 𝑋 ∈ β„•0) β†’ ((π‘†β€˜πΌ)β€˜π‘‹) ∈ (LIdealβ€˜π‘…))
113, 4, 5, 10syl3anc 1371 . . 3 (πœ‘ β†’ ((π‘†β€˜πΌ)β€˜π‘‹) ∈ (LIdealβ€˜π‘…))
12 eqid 2732 . . . 4 (RSpanβ€˜π‘…) = (RSpanβ€˜π‘…)
139, 12lnr2i 41843 . . 3 ((𝑅 ∈ LNoeR ∧ ((π‘†β€˜πΌ)β€˜π‘‹) ∈ (LIdealβ€˜π‘…)) β†’ βˆƒπ‘Ž ∈ (𝒫 ((π‘†β€˜πΌ)β€˜π‘‹) ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) = ((RSpanβ€˜π‘…)β€˜π‘Ž))
141, 11, 13syl2anc 584 . 2 (πœ‘ β†’ βˆƒπ‘Ž ∈ (𝒫 ((π‘†β€˜πΌ)β€˜π‘‹) ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) = ((RSpanβ€˜π‘…)β€˜π‘Ž))
15 elfpw 9350 . . . . 5 (π‘Ž ∈ (𝒫 ((π‘†β€˜πΌ)β€˜π‘‹) ∩ Fin) ↔ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin))
16 fvex 6901 . . . . . . . . 9 ((coe1β€˜π‘)β€˜π‘‹) ∈ V
17 eqid 2732 . . . . . . . . 9 (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) = (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹))
1816, 17fnmpti 6690 . . . . . . . 8 (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) Fn {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}
1918a1i 11 . . . . . . 7 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) Fn {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋})
20 simprl 769 . . . . . . . 8 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹))
21 eqid 2732 . . . . . . . . . . . 12 ( deg1 β€˜π‘…) = ( deg1 β€˜π‘…)
226, 7, 8, 21hbtlem1 41850 . . . . . . . . . . 11 ((𝑅 ∈ LNoeR ∧ 𝐼 ∈ π‘ˆ ∧ 𝑋 ∈ β„•0) β†’ ((π‘†β€˜πΌ)β€˜π‘‹) = {𝑑 ∣ βˆƒπ‘ ∈ 𝐼 ((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑑 = ((coe1β€˜π‘)β€˜π‘‹))})
231, 4, 5, 22syl3anc 1371 . . . . . . . . . 10 (πœ‘ β†’ ((π‘†β€˜πΌ)β€˜π‘‹) = {𝑑 ∣ βˆƒπ‘ ∈ 𝐼 ((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑑 = ((coe1β€˜π‘)β€˜π‘‹))})
2417rnmpt 5952 . . . . . . . . . . 11 ran (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) = {𝑑 ∣ βˆƒπ‘ ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}𝑑 = ((coe1β€˜π‘)β€˜π‘‹)}
25 fveq2 6888 . . . . . . . . . . . . . 14 (𝑐 = 𝑏 β†’ (( deg1 β€˜π‘…)β€˜π‘) = (( deg1 β€˜π‘…)β€˜π‘))
2625breq1d 5157 . . . . . . . . . . . . 13 (𝑐 = 𝑏 β†’ ((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ↔ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋))
2726rexrab 3691 . . . . . . . . . . . 12 (βˆƒπ‘ ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}𝑑 = ((coe1β€˜π‘)β€˜π‘‹) ↔ βˆƒπ‘ ∈ 𝐼 ((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑑 = ((coe1β€˜π‘)β€˜π‘‹)))
2827abbii 2802 . . . . . . . . . . 11 {𝑑 ∣ βˆƒπ‘ ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}𝑑 = ((coe1β€˜π‘)β€˜π‘‹)} = {𝑑 ∣ βˆƒπ‘ ∈ 𝐼 ((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑑 = ((coe1β€˜π‘)β€˜π‘‹))}
2924, 28eqtri 2760 . . . . . . . . . 10 ran (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) = {𝑑 ∣ βˆƒπ‘ ∈ 𝐼 ((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑑 = ((coe1β€˜π‘)β€˜π‘‹))}
3023, 29eqtr4di 2790 . . . . . . . . 9 (πœ‘ β†’ ((π‘†β€˜πΌ)β€˜π‘‹) = ran (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
3130adantr 481 . . . . . . . 8 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ ((π‘†β€˜πΌ)β€˜π‘‹) = ran (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
3220, 31sseqtrd 4021 . . . . . . 7 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ π‘Ž βŠ† ran (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
33 simprr 771 . . . . . . 7 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ π‘Ž ∈ Fin)
34 fipreima 9354 . . . . . . 7 (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) Fn {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘Ž βŠ† ran (𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) ∧ π‘Ž ∈ Fin) β†’ βˆƒπ‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin)((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž)
3519, 32, 33, 34syl3anc 1371 . . . . . 6 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ βˆƒπ‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin)((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž)
36 elfpw 9350 . . . . . . . . . 10 (π‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin) ↔ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin))
37 ssrab2 4076 . . . . . . . . . . . . . . . . 17 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} βŠ† 𝐼
38 sstr2 3988 . . . . . . . . . . . . . . . . 17 (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} β†’ ({𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} βŠ† 𝐼 β†’ π‘˜ βŠ† 𝐼))
3937, 38mpi 20 . . . . . . . . . . . . . . . 16 (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} β†’ π‘˜ βŠ† 𝐼)
4039adantl 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}) β†’ π‘˜ βŠ† 𝐼)
41 velpw 4606 . . . . . . . . . . . . . . 15 (π‘˜ ∈ 𝒫 𝐼 ↔ π‘˜ βŠ† 𝐼)
4240, 41sylibr 233 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}) β†’ π‘˜ ∈ 𝒫 𝐼)
4342adantrr 715 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ ∈ 𝒫 𝐼)
44 simprr 771 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ ∈ Fin)
4543, 44elind 4193 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ ∈ (𝒫 𝐼 ∩ Fin))
463adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ 𝑅 ∈ Ring)
476ply1ring 21761 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ Ring β†’ 𝑃 ∈ Ring)
483, 47syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑃 ∈ Ring)
4948adantr 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ 𝑃 ∈ Ring)
50 simprl 769 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋})
5150, 37sstrdi 3993 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ βŠ† 𝐼)
52 eqid 2732 . . . . . . . . . . . . . . . . . . 19 (Baseβ€˜π‘ƒ) = (Baseβ€˜π‘ƒ)
5352, 7lidlss 20825 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ π‘ˆ β†’ 𝐼 βŠ† (Baseβ€˜π‘ƒ))
544, 53syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐼 βŠ† (Baseβ€˜π‘ƒ))
5554adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ 𝐼 βŠ† (Baseβ€˜π‘ƒ))
5651, 55sstrd 3991 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ βŠ† (Baseβ€˜π‘ƒ))
57 hbtlem6.n . . . . . . . . . . . . . . . 16 𝑁 = (RSpanβ€˜π‘ƒ)
5857, 52, 7rspcl 20839 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Ring ∧ π‘˜ βŠ† (Baseβ€˜π‘ƒ)) β†’ (π‘β€˜π‘˜) ∈ π‘ˆ)
5949, 56, 58syl2anc 584 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ (π‘β€˜π‘˜) ∈ π‘ˆ)
605adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ 𝑋 ∈ β„•0)
616, 7, 8, 9hbtlem2 41851 . . . . . . . . . . . . . 14 ((𝑅 ∈ Ring ∧ (π‘β€˜π‘˜) ∈ π‘ˆ ∧ 𝑋 ∈ β„•0) β†’ ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) ∈ (LIdealβ€˜π‘…))
6246, 59, 60, 61syl3anc 1371 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) ∈ (LIdealβ€˜π‘…))
63 df-ima 5688 . . . . . . . . . . . . . . 15 ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = ran ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜)
6457, 52rspssid 20840 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ Ring ∧ π‘˜ βŠ† (Baseβ€˜π‘ƒ)) β†’ π‘˜ βŠ† (π‘β€˜π‘˜))
6549, 56, 64syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ βŠ† (π‘β€˜π‘˜))
66 ssrab 4069 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↔ (π‘˜ βŠ† 𝐼 ∧ βˆ€π‘ ∈ π‘˜ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋))
6766simprbi 497 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} β†’ βˆ€π‘ ∈ π‘˜ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋)
6867ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ βˆ€π‘ ∈ π‘˜ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋)
69 ssrab 4069 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ βŠ† {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↔ (π‘˜ βŠ† (π‘β€˜π‘˜) ∧ βˆ€π‘ ∈ π‘˜ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋))
7065, 68, 69sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ π‘˜ βŠ† {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋})
7170resmptd 6038 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) = (𝑏 ∈ π‘˜ ↦ ((coe1β€˜π‘)β€˜π‘‹)))
72 resmpt 6035 . . . . . . . . . . . . . . . . . . 19 (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} β†’ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) = (𝑏 ∈ π‘˜ ↦ ((coe1β€˜π‘)β€˜π‘‹)))
7372ad2antrl 726 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) = (𝑏 ∈ π‘˜ ↦ ((coe1β€˜π‘)β€˜π‘‹)))
7471, 73eqtr4d 2775 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) = ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜))
75 resss 6004 . . . . . . . . . . . . . . . . 17 ((𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) βŠ† (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹))
7674, 75eqsstrrdi 4036 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) βŠ† (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
77 rnss 5936 . . . . . . . . . . . . . . . 16 (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) βŠ† (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†’ ran ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) βŠ† ran (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
7876, 77syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ran ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β†Ύ π‘˜) βŠ† ran (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
7963, 78eqsstrid 4029 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) βŠ† ran (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
806, 7, 8, 21hbtlem1 41850 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Ring ∧ (π‘β€˜π‘˜) ∈ π‘ˆ ∧ 𝑋 ∈ β„•0) β†’ ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) = {𝑒 ∣ βˆƒπ‘ ∈ (π‘β€˜π‘˜)((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑒 = ((coe1β€˜π‘)β€˜π‘‹))})
8146, 59, 60, 80syl3anc 1371 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) = {𝑒 ∣ βˆƒπ‘ ∈ (π‘β€˜π‘˜)((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑒 = ((coe1β€˜π‘)β€˜π‘‹))})
82 eqid 2732 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) = (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹))
8382rnmpt 5952 . . . . . . . . . . . . . . . 16 ran (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) = {𝑒 ∣ βˆƒπ‘ ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}𝑒 = ((coe1β€˜π‘)β€˜π‘‹)}
8426rexrab 3691 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘ ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}𝑒 = ((coe1β€˜π‘)β€˜π‘‹) ↔ βˆƒπ‘ ∈ (π‘β€˜π‘˜)((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑒 = ((coe1β€˜π‘)β€˜π‘‹)))
8584abbii 2802 . . . . . . . . . . . . . . . 16 {𝑒 ∣ βˆƒπ‘ ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋}𝑒 = ((coe1β€˜π‘)β€˜π‘‹)} = {𝑒 ∣ βˆƒπ‘ ∈ (π‘β€˜π‘˜)((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑒 = ((coe1β€˜π‘)β€˜π‘‹))}
8683, 85eqtri 2760 . . . . . . . . . . . . . . 15 ran (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) = {𝑒 ∣ βˆƒπ‘ ∈ (π‘β€˜π‘˜)((( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋 ∧ 𝑒 = ((coe1β€˜π‘)β€˜π‘‹))}
8781, 86eqtr4di 2790 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) = ran (𝑏 ∈ {𝑐 ∈ (π‘β€˜π‘˜) ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)))
8879, 87sseqtrrd 4022 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
8912, 9rspssp 20843 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) ∈ (LIdealβ€˜π‘…) ∧ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)) β†’ ((RSpanβ€˜π‘…)β€˜((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜)) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
9046, 62, 88, 89syl3anc 1371 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ ((RSpanβ€˜π‘…)β€˜((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜)) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
9145, 90jca 512 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ (π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜)) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
92 fveq2 6888 . . . . . . . . . . . . 13 (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž β†’ ((RSpanβ€˜π‘…)β€˜((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜)) = ((RSpanβ€˜π‘…)β€˜π‘Ž))
9392sseq1d 4012 . . . . . . . . . . . 12 (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž β†’ (((RSpanβ€˜π‘…)β€˜((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜)) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) ↔ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
9493anbi2d 629 . . . . . . . . . . 11 (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž β†’ ((π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜)) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)) ↔ (π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))))
9591, 94syl5ibcom 244 . . . . . . . . . 10 ((πœ‘ ∧ (π‘˜ βŠ† {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∧ π‘˜ ∈ Fin)) β†’ (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž β†’ (π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))))
9636, 95sylan2b 594 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin)) β†’ (((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž β†’ (π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))))
9796expimpd 454 . . . . . . . 8 (πœ‘ β†’ ((π‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin) ∧ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž) β†’ (π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))))
9897adantr 481 . . . . . . 7 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ ((π‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin) ∧ ((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž) β†’ (π‘˜ ∈ (𝒫 𝐼 ∩ Fin) ∧ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))))
9998reximdv2 3164 . . . . . 6 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ (βˆƒπ‘˜ ∈ (𝒫 {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ∩ Fin)((𝑏 ∈ {𝑐 ∈ 𝐼 ∣ (( deg1 β€˜π‘…)β€˜π‘) ≀ 𝑋} ↦ ((coe1β€˜π‘)β€˜π‘‹)) β€œ π‘˜) = π‘Ž β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
10035, 99mpd 15 . . . . 5 ((πœ‘ ∧ (π‘Ž βŠ† ((π‘†β€˜πΌ)β€˜π‘‹) ∧ π‘Ž ∈ Fin)) β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
10115, 100sylan2b 594 . . . 4 ((πœ‘ ∧ π‘Ž ∈ (𝒫 ((π‘†β€˜πΌ)β€˜π‘‹) ∩ Fin)) β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
102 sseq1 4006 . . . . 5 (((π‘†β€˜πΌ)β€˜π‘‹) = ((RSpanβ€˜π‘…)β€˜π‘Ž) β†’ (((π‘†β€˜πΌ)β€˜π‘‹) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) ↔ ((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
103102rexbidv 3178 . . . 4 (((π‘†β€˜πΌ)β€˜π‘‹) = ((RSpanβ€˜π‘…)β€˜π‘Ž) β†’ (βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹) ↔ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((RSpanβ€˜π‘…)β€˜π‘Ž) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
104101, 103syl5ibrcom 246 . . 3 ((πœ‘ ∧ π‘Ž ∈ (𝒫 ((π‘†β€˜πΌ)β€˜π‘‹) ∩ Fin)) β†’ (((π‘†β€˜πΌ)β€˜π‘‹) = ((RSpanβ€˜π‘…)β€˜π‘Ž) β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
105104rexlimdva 3155 . 2 (πœ‘ β†’ (βˆƒπ‘Ž ∈ (𝒫 ((π‘†β€˜πΌ)β€˜π‘‹) ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) = ((RSpanβ€˜π‘…)β€˜π‘Ž) β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹)))
10614, 105mpd 15 1 (πœ‘ β†’ βˆƒπ‘˜ ∈ (𝒫 𝐼 ∩ Fin)((π‘†β€˜πΌ)β€˜π‘‹) βŠ† ((π‘†β€˜(π‘β€˜π‘˜))β€˜π‘‹))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601   class class class wbr 5147   ↦ cmpt 5230  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   Fn wfn 6535  β€˜cfv 6540  Fincfn 8935   ≀ cle 11245  β„•0cn0 12468  Basecbs 17140  Ringcrg 20049  LIdealclidl 20775  RSpancrsp 20776  Poly1cpl1 21692  coe1cco1 21693   deg1 cdg1 25560  LNoeRclnr 41836  ldgIdlSeqcldgis 41848
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-fzo 13624  df-seq 13963  df-hash 14287  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-ghm 19084  df-cntz 19175  df-cmn 19644  df-abl 19645  df-mgp 19982  df-ur 19999  df-ring 20051  df-cring 20052  df-subrg 20353  df-lmod 20465  df-lss 20535  df-lsp 20575  df-sra 20777  df-rgmod 20778  df-lidl 20779  df-rsp 20780  df-cnfld 20937  df-ascl 21401  df-psr 21453  df-mvr 21454  df-mpl 21455  df-opsr 21457  df-psr1 21695  df-vr1 21696  df-ply1 21697  df-coe1 21698  df-mdeg 25561  df-deg1 25562  df-lfig 41795  df-lnm 41803  df-lnr 41837  df-ldgis 41849
This theorem is referenced by:  hbt  41857
  Copyright terms: Public domain W3C validator