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 ‘ 𝑘 ) ‘ 𝑋 ) ) } )