Metamath Proof Explorer


Theorem hbtlem7

Description: Functionality of leading coefficient ideal sequence. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypotheses hbtlem.p 𝑃 = ( Poly1𝑅 )
hbtlem.u 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem7.t 𝑇 = ( LIdeal ‘ 𝑅 )
Assertion hbtlem7 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( 𝑆𝐼 ) : ℕ0𝑇 )

Proof

Step Hyp Ref Expression
1 hbtlem.p 𝑃 = ( Poly1𝑅 )
2 hbtlem.u 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem7.t 𝑇 = ( LIdeal ‘ 𝑅 )
5 simpr ( ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) → 𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) )
6 5 reximi ( ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) → ∃ 𝑗𝐼 𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) )
7 6 ss2abi { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ⊆ { 𝑦 ∣ ∃ 𝑗𝐼 𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) }
8 abrexexg ( 𝐼𝑈 → { 𝑦 ∣ ∃ 𝑗𝐼 𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) } ∈ V )
9 ssexg ( ( { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ⊆ { 𝑦 ∣ ∃ 𝑗𝐼 𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) } ∧ { 𝑦 ∣ ∃ 𝑗𝐼 𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) } ∈ V ) → { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ∈ V )
10 7 8 9 sylancr ( 𝐼𝑈 → { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ∈ V )
11 10 ralrimivw ( 𝐼𝑈 → ∀ 𝑥 ∈ ℕ0 { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ∈ V )
12 11 adantl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ∀ 𝑥 ∈ ℕ0 { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ∈ V )
13 eqid ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } )
14 13 fnmpt ( ∀ 𝑥 ∈ ℕ0 { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ∈ V → ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) Fn ℕ0 )
15 12 14 syl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) Fn ℕ0 )
16 elex ( 𝑅 ∈ Ring → 𝑅 ∈ V )
17 fveq2 ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = ( Poly1𝑅 ) )
18 17 1 eqtr4di ( 𝑟 = 𝑅 → ( Poly1𝑟 ) = 𝑃 )
19 18 fveq2d ( 𝑟 = 𝑅 → ( LIdeal ‘ ( Poly1𝑟 ) ) = ( LIdeal ‘ 𝑃 ) )
20 19 2 eqtr4di ( 𝑟 = 𝑅 → ( LIdeal ‘ ( Poly1𝑟 ) ) = 𝑈 )
21 fveq2 ( 𝑟 = 𝑅 → ( deg1𝑟 ) = ( deg1𝑅 ) )
22 21 fveq1d ( 𝑟 = 𝑅 → ( ( deg1𝑟 ) ‘ 𝑗 ) = ( ( deg1𝑅 ) ‘ 𝑗 ) )
23 22 breq1d ( 𝑟 = 𝑅 → ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥 ↔ ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥 ) )
24 23 anbi1d ( 𝑟 = 𝑅 → ( ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) ↔ ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) ) )
25 24 rexbidv ( 𝑟 = 𝑅 → ( ∃ 𝑗𝑖 ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) ↔ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) ) )
26 25 abbidv ( 𝑟 = 𝑅 → { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } )
27 26 mpteq2dv ( 𝑟 = 𝑅 → ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) )
28 20 27 mpteq12dv ( 𝑟 = 𝑅 → ( 𝑖 ∈ ( LIdeal ‘ ( Poly1𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) )
29 df-ldgis ldgIdlSeq = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly1𝑟 ) ) ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑟 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) )
30 28 29 2 mptfvmpt ( 𝑅 ∈ V → ( ldgIdlSeq ‘ 𝑅 ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) )
31 16 30 syl ( 𝑅 ∈ Ring → ( ldgIdlSeq ‘ 𝑅 ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) )
32 3 31 eqtrid ( 𝑅 ∈ Ring → 𝑆 = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) )
33 32 fveq1d ( 𝑅 ∈ Ring → ( 𝑆𝐼 ) = ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) )
34 rexeq ( 𝑖 = 𝐼 → ( ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) ↔ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) ) )
35 34 abbidv ( 𝑖 = 𝐼 → { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } = { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } )
36 35 mpteq2dv ( 𝑖 = 𝐼 → ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) )
37 eqid ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) = ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) )
38 nn0ex 0 ∈ V
39 38 mptex ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ∈ V
40 36 37 39 fvmpt ( 𝐼𝑈 → ( ( 𝑖𝑈 ↦ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝑖 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) ) ‘ 𝐼 ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) )
41 33 40 sylan9eq ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( 𝑆𝐼 ) = ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) )
42 41 fneq1d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( ( 𝑆𝐼 ) Fn ℕ0 ↔ ( 𝑥 ∈ ℕ0 ↦ { 𝑦 ∣ ∃ 𝑗𝐼 ( ( ( deg1𝑅 ) ‘ 𝑗 ) ≤ 𝑥𝑦 = ( ( coe1𝑗 ) ‘ 𝑥 ) ) } ) Fn ℕ0 ) )
43 15 42 mpbird ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( 𝑆𝐼 ) Fn ℕ0 )
44 1 2 3 4 hbtlem2 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈𝑥 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑥 ) ∈ 𝑇 )
45 44 3expa ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑆𝐼 ) ‘ 𝑥 ) ∈ 𝑇 )
46 45 ralrimiva ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ∀ 𝑥 ∈ ℕ0 ( ( 𝑆𝐼 ) ‘ 𝑥 ) ∈ 𝑇 )
47 ffnfv ( ( 𝑆𝐼 ) : ℕ0𝑇 ↔ ( ( 𝑆𝐼 ) Fn ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( ( 𝑆𝐼 ) ‘ 𝑥 ) ∈ 𝑇 ) )
48 43 46 47 sylanbrc ( ( 𝑅 ∈ Ring ∧ 𝐼𝑈 ) → ( 𝑆𝐼 ) : ℕ0𝑇 )