Metamath Proof Explorer


Theorem hbtlem1

Description: Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Hypotheses hbtlem.p 𝑃 = ( Poly1𝑅 )
hbtlem.u 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem.d 𝐷 = ( deg1𝑅 )
Assertion hbtlem1 ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } )

Proof

Step Hyp Ref Expression
1 hbtlem.p 𝑃 = ( Poly1𝑅 )
2 hbtlem.u 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem.d 𝐷 = ( deg1𝑅 )
5 elex ( 𝑅𝑉𝑅 ∈ V )
6 fveq2 ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = ( Poly1𝑅 ) )
7 6 1 eqtr4di ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = 𝑃 )
8 7 fveq2d ( 𝑟 = 𝑅 → ( LIdeal ‘ ( Poly1𝑟 ) ) = ( LIdeal ‘ 𝑃 ) )
9 8 2 eqtr4di ( 𝑟 = 𝑅 → ( LIdeal ‘ ( Poly1𝑟 ) ) = 𝑈 )
10 fveq2 ( 𝑟 = 𝑅 → ( deg1𝑟 ) = ( deg1𝑅 ) )
11 10 4 eqtr4di ( 𝑟 = 𝑅 → ( deg1𝑟 ) = 𝐷 )
12 11 fveq1d ( 𝑟 = 𝑅 → ( ( deg1𝑟 ) ‘ 𝑘 ) = ( 𝐷𝑘 ) )
13 12 breq1d ( 𝑟 = 𝑅 → ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥 ↔ ( 𝐷𝑘 ) ≤ 𝑥 ) )
14 13 anbi1d ( 𝑟 = 𝑅 → ( ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ↔ ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ) )
15 14 rexbidv ( 𝑟 = 𝑅 → ( ∃ 𝑘𝑖 ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ↔ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ) )
16 15 abbidv ( 𝑟 = 𝑅 → { 𝑗 ∣ ∃ 𝑘𝑖 ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } = { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } )
17 16 mpteq2dv ( 𝑟 = 𝑅 → ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) )
18 9 17 mpteq12dv ( 𝑟 = 𝑅 → ( 𝑖 ∈ ( LIdeal ‘ ( Poly1𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) )
19 df-ldgis ldgIdlSeq = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( ( deg1𝑟 ) ‘ 𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) )
20 18 19 2 mptfvmpt ( 𝑅 ∈ V → ( ldgIdlSeq ‘ 𝑅 ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) )
21 5 20 syl ( 𝑅𝑉 → ( ldgIdlSeq ‘ 𝑅 ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) )
22 3 21 syl5eq ( 𝑅𝑉𝑆 = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) )
23 22 fveq1d ( 𝑅𝑉 → ( 𝑆𝐼 ) = ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) )
24 23 fveq1d ( 𝑅𝑉 → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) ‘ 𝑋 ) )
25 24 3ad2ant1 ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = ( ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) ‘ 𝑋 ) )
26 rexeq ( 𝑖 = 𝐼 → ( ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ↔ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ) )
27 26 abbidv ( 𝑖 = 𝐼 → { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } = { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } )
28 27 mpteq2dv ( 𝑖 = 𝐼 → ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) )
29 eqid ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) )
30 nn0ex 0 ∈ V
31 30 mptex ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ∈ V
32 28 29 31 fvmpt ( 𝐼𝑈 → ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) )
33 32 fveq1d ( 𝐼𝑈 → ( ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ‘ 𝑋 ) )
34 33 3ad2ant2 ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝑖 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) ‘ 𝑋 ) = ( ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ‘ 𝑋 ) )
35 eqid ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } )
36 breq2 ( 𝑥 = 𝑋 → ( ( 𝐷𝑘 ) ≤ 𝑥 ↔ ( 𝐷𝑘 ) ≤ 𝑋 ) )
37 fveq2 ( 𝑥 = 𝑋 → ( ( coe1𝑘 ) ‘ 𝑥 ) = ( ( coe1𝑘 ) ‘ 𝑋 ) )
38 37 eqeq2d ( 𝑥 = 𝑋 → ( 𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ↔ 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) )
39 36 38 anbi12d ( 𝑥 = 𝑋 → ( ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ↔ ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) ) )
40 39 rexbidv ( 𝑥 = 𝑋 → ( ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) ↔ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) ) )
41 40 abbidv ( 𝑥 = 𝑋 → { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } = { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } )
42 simp3 ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → 𝑋 ∈ ℕ0 )
43 simpr ( ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) → 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) )
44 43 reximi ( ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) → ∃ 𝑘𝐼 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) )
45 44 ss2abi { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } ⊆ { 𝑗 ∣ ∃ 𝑘𝐼 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) }
46 abrexexg ( 𝐼𝑈 → { 𝑗 ∣ ∃ 𝑘𝐼 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) } ∈ V )
47 46 3ad2ant2 ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → { 𝑗 ∣ ∃ 𝑘𝐼 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) } ∈ V )
48 ssexg ( ( { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } ⊆ { 𝑗 ∣ ∃ 𝑘𝐼 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) } ∧ { 𝑗 ∣ ∃ 𝑘𝐼 𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) } ∈ V ) → { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } ∈ V )
49 45 47 48 sylancr ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } ∈ V )
50 35 41 42 49 fvmptd3 ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑥 ∈ ℕ0 ↦ { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑥𝑗 = ( ( coe1𝑘 ) ‘ 𝑥 ) ) } ) ‘ 𝑋 ) = { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } )
51 25 34 50 3eqtrd ( ( 𝑅𝑉𝐼𝑈𝑋 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑋 ) = { 𝑗 ∣ ∃ 𝑘𝐼 ( ( 𝐷𝑘 ) ≤ 𝑋𝑗 = ( ( coe1𝑘 ) ‘ 𝑋 ) ) } )