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