Metamath Proof Explorer

Theorem hbtlem4

Description: The leading ideal function goes to increasing sequences. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem4.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
hbtlem4.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
hbtlem4.x ⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
hbtlem4.y ⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
hbtlem4.xy ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
Assertion hbtlem4 ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem4.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 hbtlem4.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
6 hbtlem4.x ⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
7 hbtlem4.y ⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
8 hbtlem4.xy ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
9 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑅 ∈ Ring )
10 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11 9 10 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑃 ∈ Ring )
12 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝐼 ∈ 𝑈 )
13 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
14 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15 13 14 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
16 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
17 13 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
18 11 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
19 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑋 ∈ ℕ0 )
20 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑌 ∈ ℕ0 )
21 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑋 ≤ 𝑌 )
22 nn0sub2 ⊢ ( ( 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℕ0 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℕ0 )
23 19 20 21 22 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( 𝑌 − 𝑋 ) ∈ ℕ0 )
24 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
25 24 1 14 vr1cl ⊢ ( 𝑅 ∈ Ring → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
26 9 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
27 15 16 18 23 26 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑐 ∈ 𝐼 )
29 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
30 2 14 29 lidlmcl ⊢ ( ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑐 ∈ 𝐼 ) ) → ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ∈ 𝐼 )
31 11 12 27 28 30 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ∈ 𝐼 )
32 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
33 14 2 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
34 12 33 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
35 34 28 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑐 ∈ ( Base ‘ 𝑃 ) )
36 32 1 24 13 16 deg1pwle ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 − 𝑋 ) ∈ ℕ0 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ≤ ( 𝑌 − 𝑋 ) )
37 9 23 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ≤ ( 𝑌 − 𝑋 ) )
38 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 )
39 1 32 9 14 29 27 35 23 19 37 38 deg1mulle2 ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ≤ ( ( 𝑌 − 𝑋 ) + 𝑋 ) )
40 20 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑌 ∈ ℂ )
41 19 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → 𝑋 ∈ ℂ )
42 40 41 npcand ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( 𝑌 − 𝑋 ) + 𝑋 ) = 𝑌 )
43 39 42 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ≤ 𝑌 )
44 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
45 44 1 24 13 16 14 29 9 35 23 19 coe1pwmulfv ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ ( ( 𝑌 − 𝑋 ) + 𝑋 ) ) = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) )
46 42 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ ( ( 𝑌 − 𝑋 ) + 𝑋 ) ) = ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ 𝑌 ) )
47 45 46 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ 𝑌 ) )
48 fveq2 ⊢ ( 𝑏 = ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) = ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) )
49 48 breq1d ⊢ ( 𝑏 = ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ↔ ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ≤ 𝑌 ) )
50 fveq2 ⊢ ( 𝑏 = ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) → ( coe1 ‘ 𝑏 ) = ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) )
51 50 fveq1d ⊢ ( 𝑏 = ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) → ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) = ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ 𝑌 ) )
52 51 eqeq2d ⊢ ( 𝑏 = ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) → ( ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ↔ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ 𝑌 ) ) )
53 49 52 anbi12d ⊢ ( 𝑏 = ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ 𝑌 ) ) ) )
54 53 rspcev ⊢ ( ( ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ∈ 𝐼 ∧ ( ( ( deg1 ‘ 𝑅 ) ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ ( ( ( 𝑌 − 𝑋 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑐 ) ) ‘ 𝑌 ) ) ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) )
55 31 43 47 54 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) )
56 eqeq1 ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) → ( 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ↔ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) )
57 56 anbi2d ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ↔ ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ) )
58 57 rexbidv ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) → ( ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ) )
59 55 58 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) → ( 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ) )
60 59 expimpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐼 ) → ( ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ) )
61 60 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) ) → ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) ) )
62 61 ss2abdv ⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑐 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) ) } ⊆ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) } )
63 1 2 3 32 hbtlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑐 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) ) } )
64 4 5 6 63 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑎 ∣ ∃ 𝑐 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ∧ 𝑎 = ( ( coe1 ‘ 𝑐 ) ‘ 𝑋 ) ) } )
65 1 2 3 32 hbtlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑌 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑌 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) } )
66 4 5 7 65 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑌 ) = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑌 ∧ 𝑎 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑌 ) ) } )
67 62 64 66 3sstr4d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑌 ) )