hbtlem7

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

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

Proof

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

Metamath Proof Explorer

Theorem hbtlem7

Proof