Metamath Proof Explorer


Theorem hbtlem6

Description: There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p 𝑃 = ( Poly1𝑅 )
hbtlem.u 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem6.n 𝑁 = ( RSpan ‘ 𝑃 )
hbtlem6.r ( 𝜑𝑅 ∈ LNoeR )
hbtlem6.i ( 𝜑𝐼𝑈 )
hbtlem6.x ( 𝜑𝑋 ∈ ℕ0 )
Assertion hbtlem6 ( 𝜑 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 hbtlem.p 𝑃 = ( Poly1𝑅 )
2 hbtlem.u 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem6.n 𝑁 = ( RSpan ‘ 𝑃 )
5 hbtlem6.r ( 𝜑𝑅 ∈ LNoeR )
6 hbtlem6.i ( 𝜑𝐼𝑈 )
7 hbtlem6.x ( 𝜑𝑋 ∈ ℕ0 )
8 lnrring ( 𝑅 ∈ LNoeR → 𝑅 ∈ Ring )
9 5 8 syl ( 𝜑𝑅 ∈ Ring )
10 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
11 1 2 3 10 hbtlem2 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
12 9 6 7 11 syl3anc ( 𝜑 → ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
13 eqid ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
14 10 13 lnr2i ( ( 𝑅 ∈ LNoeR ∧ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) → ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) )
15 5 12 14 syl2anc ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) )
16 elfpw ( 𝑎 ∈ ( 𝒫 ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∩ Fin ) ↔ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) )
17 fvex ( ( coe1𝑏 ) ‘ 𝑋 ) ∈ V
18 eqid ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) = ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) )
19 17 18 fnmpti ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 }
20 19 a1i ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } )
21 simprl ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) )
22 eqid ( deg1𝑅 ) = ( deg1𝑅 )
23 1 2 3 22 hbtlem1 ( ( 𝑅 ∈ LNoeR ∧ 𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = { 𝑑 ∣ ∃ 𝑏𝐼 ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) } )
24 5 6 7 23 syl3anc ( 𝜑 → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = { 𝑑 ∣ ∃ 𝑏𝐼 ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) } )
25 18 rnmpt ran ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) = { 𝑑 ∣ ∃ 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) }
26 fveq2 ( 𝑐 = 𝑏 → ( ( deg1𝑅 ) ‘ 𝑐 ) = ( ( deg1𝑅 ) ‘ 𝑏 ) )
27 26 breq1d ( 𝑐 = 𝑏 → ( ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ↔ ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ) )
28 27 rexrab ( ∃ 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) ↔ ∃ 𝑏𝐼 ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
29 28 abbii { 𝑑 ∣ ∃ 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) } = { 𝑑 ∣ ∃ 𝑏𝐼 ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) }
30 25 29 eqtri ran ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) = { 𝑑 ∣ ∃ 𝑏𝐼 ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑑 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) }
31 24 30 eqtr4di ( 𝜑 → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
32 31 adantr ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
33 21 32 sseqtrd ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ⊆ ran ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
34 simprr ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ∈ Fin )
35 fipreima ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑎 ⊆ ran ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ∧ 𝑎 ∈ Fin ) → ∃ 𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 )
36 20 33 34 35 syl3anc ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 )
37 elfpw ( 𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ↔ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) )
38 ssrab2 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ⊆ 𝐼
39 sstr2 ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ( { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ⊆ 𝐼𝑘𝐼 ) )
40 38 39 mpi ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → 𝑘𝐼 )
41 40 adantl ( ( 𝜑𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) → 𝑘𝐼 )
42 velpw ( 𝑘 ∈ 𝒫 𝐼𝑘𝐼 )
43 41 42 sylibr ( ( 𝜑𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) → 𝑘 ∈ 𝒫 𝐼 )
44 43 adantrr ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ 𝒫 𝐼 )
45 simprr ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ Fin )
46 44 45 elind ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) )
47 9 adantr ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑅 ∈ Ring )
48 1 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
49 9 48 syl ( 𝜑𝑃 ∈ Ring )
50 49 adantr ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑃 ∈ Ring )
51 simprl ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } )
52 51 38 sstrdi ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘𝐼 )
53 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
54 53 2 lidlss ( 𝐼𝑈𝐼 ⊆ ( Base ‘ 𝑃 ) )
55 6 54 syl ( 𝜑𝐼 ⊆ ( Base ‘ 𝑃 ) )
56 55 adantr ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
57 52 56 sstrd ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ ( Base ‘ 𝑃 ) )
58 4 53 2 rspcl ( ( 𝑃 ∈ Ring ∧ 𝑘 ⊆ ( Base ‘ 𝑃 ) ) → ( 𝑁𝑘 ) ∈ 𝑈 )
59 50 57 58 syl2anc ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( 𝑁𝑘 ) ∈ 𝑈 )
60 7 adantr ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑋 ∈ ℕ0 )
61 1 2 3 10 hbtlem2 ( ( 𝑅 ∈ Ring ∧ ( 𝑁𝑘 ) ∈ 𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
62 47 59 60 61 syl3anc ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
63 df-ima ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = ran ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 )
64 4 53 rspssid ( ( 𝑃 ∈ Ring ∧ 𝑘 ⊆ ( Base ‘ 𝑃 ) ) → 𝑘 ⊆ ( 𝑁𝑘 ) )
65 50 57 64 syl2anc ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ ( 𝑁𝑘 ) )
66 ssrab ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↔ ( 𝑘𝐼 ∧ ∀ 𝑐𝑘 ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) )
67 66 simprbi ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ∀ 𝑐𝑘 ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 )
68 67 ad2antrl ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ∀ 𝑐𝑘 ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 )
69 ssrab ( 𝑘 ⊆ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↔ ( 𝑘 ⊆ ( 𝑁𝑘 ) ∧ ∀ 𝑐𝑘 ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) )
70 65 68 69 sylanbrc ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } )
71 70 resmptd ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏𝑘 ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
72 resmpt ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏𝑘 ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
73 72 ad2antrl ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏𝑘 ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
74 71 73 eqtr4d ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) )
75 resss ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) )
76 74 75 eqsstrrdi ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
77 rnss ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) → ran ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
78 76 77 syl ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ran ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
79 63 78 eqsstrid ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
80 1 2 3 22 hbtlem1 ( ( 𝑅 ∈ Ring ∧ ( 𝑁𝑘 ) ∈ 𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁𝑘 ) ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) } )
81 47 59 60 80 syl3anc ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁𝑘 ) ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) } )
82 eqid ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) = ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) )
83 82 rnmpt ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) = { 𝑒 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) }
84 27 rexrab ( ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) ↔ ∃ 𝑏 ∈ ( 𝑁𝑘 ) ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
85 84 abbii { 𝑒 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) } = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁𝑘 ) ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) }
86 83 85 eqtri ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁𝑘 ) ( ( ( deg1𝑅 ) ‘ 𝑏 ) ≤ 𝑋𝑒 = ( ( coe1𝑏 ) ‘ 𝑋 ) ) }
87 81 86 eqtr4di ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁𝑘 ) ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) )
88 79 87 sseqtrrd ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )
89 13 10 rspssp ( ( 𝑅 ∈ Ring ∧ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )
90 47 62 88 89 syl3anc ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )
91 46 90 jca ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
92 fveq2 ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) )
93 92 sseq1d ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
94 93 anbi2d ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) ↔ ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) ) )
95 91 94 syl5ibcom ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) ) )
96 37 95 sylan2b ( ( 𝜑𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ) → ( ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) ) )
97 96 expimpd ( 𝜑 → ( ( 𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ∧ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) ) )
98 97 adantr ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ( 𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ∧ ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) ) )
99 98 reximdv2 ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ∃ 𝑘 ∈ ( 𝒫 { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐𝐼 ∣ ( ( deg1𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
100 36 99 mpd ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )
101 16 100 sylan2b ( ( 𝜑𝑎 ∈ ( 𝒫 ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∩ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )
102 sseq1 ( ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ( ( ( 𝑆𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
103 102 rexbidv ( ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ( ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ↔ ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
104 101 103 syl5ibrcom ( ( 𝜑𝑎 ∈ ( 𝒫 ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∩ Fin ) ) → ( ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
105 104 rexlimdva ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) ) )
106 15 105 mpd ( 𝜑 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁𝑘 ) ) ‘ 𝑋 ) )