ig1pval

Description: Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	ig1pval.g	⊢ 𝐺 = ( idlGen_1p ‘ 𝑅 )
	ig1pval.z	⊢ 0 = ( 0_g ‘ 𝑃 )
	ig1pval.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
	ig1pval.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
	ig1pval.m	⊢ 𝑀 = ( Monic_1p ‘ 𝑅 )
Assertion	ig1pval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) = if ( 𝐼 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ig1pval.g	⊢ 𝐺 = ( idlGen_1p ‘ 𝑅 )
3		ig1pval.z	⊢ 0 = ( 0_g ‘ 𝑃 )
4		ig1pval.u	⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
5		ig1pval.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
6		ig1pval.m	⊢ 𝑀 = ( Monic_1p ‘ 𝑅 )
7		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
8		fveq2	⊢ ( 𝑟 = 𝑅 → ( Poly₁ ‘ 𝑟 ) = ( Poly₁ ‘ 𝑅 ) )
9	8 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Poly₁ ‘ 𝑟 ) = 𝑃 )
10	9	fveq2d	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ ( Poly₁ ‘ 𝑟 ) ) = ( LIdeal ‘ 𝑃 ) )
11	10 4	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( LIdeal ‘ ( Poly₁ ‘ 𝑟 ) ) = 𝑈 )
12	9	fveq2d	⊢ ( 𝑟 = 𝑅 → ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) = ( 0_g ‘ 𝑃 ) )
13	12 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) = 0 )
14	13	sneqd	⊢ ( 𝑟 = 𝑅 → { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } = { 0 } )
15	14	eqeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 = { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ↔ 𝑖 = { 0 } ) )
16		fveq2	⊢ ( 𝑟 = 𝑅 → ( Monic_1p ‘ 𝑟 ) = ( Monic_1p ‘ 𝑅 ) )
17	16 6	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Monic_1p ‘ 𝑟 ) = 𝑀 )
18	17	ineq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ∩ ( Monic_1p ‘ 𝑟 ) ) = ( 𝑖 ∩ 𝑀 ) )
19		fveq2	⊢ ( 𝑟 = 𝑅 → ( deg₁ ‘ 𝑟 ) = ( deg₁ ‘ 𝑅 ) )
20	19 5	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( deg₁ ‘ 𝑟 ) = 𝐷 )
21	20	fveq1d	⊢ ( 𝑟 = 𝑅 → ( ( deg₁ ‘ 𝑟 ) ‘ 𝑔 ) = ( 𝐷 ‘ 𝑔 ) )
22	14	difeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) = ( 𝑖 ∖ { 0 } ) )
23	20 22	imaeq12d	⊢ ( 𝑟 = 𝑅 → ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) = ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) )
24	23	infeq1d	⊢ ( 𝑟 = 𝑅 → inf ( ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) , ℝ , < ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) )
25	21 24	eqeq12d	⊢ ( 𝑟 = 𝑅 → ( ( ( deg₁ ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) , ℝ , < ) ↔ ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) )
26	18 25	riotaeqbidv	⊢ ( 𝑟 = 𝑅 → ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic_1p ‘ 𝑟 ) ) ( ( deg₁ ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) = ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) )
27	15 13 26	ifbieq12d	⊢ ( 𝑟 = 𝑅 → if ( 𝑖 = { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } , ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic_1p ‘ 𝑟 ) ) ( ( deg₁ ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) = if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) )
28	11 27	mpteq12dv	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ∈ ( LIdeal ‘ ( Poly₁ ‘ 𝑟 ) ) ↦ if ( 𝑖 = { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } , ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic_1p ‘ 𝑟 ) ) ( ( deg₁ ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) ) = ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) )
29		df-ig1p	⊢ idlGen_1p = ( 𝑟 ∈ V ↦ ( 𝑖 ∈ ( LIdeal ‘ ( Poly₁ ‘ 𝑟 ) ) ↦ if ( 𝑖 = { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } , ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) , ( ℩ 𝑔 ∈ ( 𝑖 ∩ ( Monic_1p ‘ 𝑟 ) ) ( ( deg₁ ‘ 𝑟 ) ‘ 𝑔 ) = inf ( ( ( deg₁ ‘ 𝑟 ) “ ( 𝑖 ∖ { ( 0_g ‘ ( Poly₁ ‘ 𝑟 ) ) } ) ) , ℝ , < ) ) ) ) )
30	28 29 4	mptfvmpt	⊢ ( 𝑅 ∈ V → ( idlGen_1p ‘ 𝑅 ) = ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) )
31	7 30	syl	⊢ ( 𝑅 ∈ 𝑉 → ( idlGen_1p ‘ 𝑅 ) = ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) )
32	2 31	syl5eq	⊢ ( 𝑅 ∈ 𝑉 → 𝐺 = ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) )
33	32	fveq1d	⊢ ( 𝑅 ∈ 𝑉 → ( 𝐺 ‘ 𝐼 ) = ( ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) ‘ 𝐼 ) )
34		eqeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 = { 0 } ↔ 𝐼 = { 0 } ) )
35		ineq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∩ 𝑀 ) = ( 𝐼 ∩ 𝑀 ) )
36		difeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∖ { 0 } ) = ( 𝐼 ∖ { 0 } ) )
37	36	imaeq2d	⊢ ( 𝑖 = 𝐼 → ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) = ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) )
38	37	infeq1d	⊢ ( 𝑖 = 𝐼 → inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) )
39	38	eqeq2d	⊢ ( 𝑖 = 𝐼 → ( ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ↔ ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
40	35 39	riotaeqbidv	⊢ ( 𝑖 = 𝐼 → ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) = ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) )
41	34 40	ifbieq2d	⊢ ( 𝑖 = 𝐼 → if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) = if ( 𝐼 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) )
42		eqid	⊢ ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) = ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) )
43	3	fvexi	⊢ 0 ∈ V
44		riotaex	⊢ ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ∈ V
45	43 44	ifex	⊢ if ( 𝐼 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) ∈ V
46	41 42 45	fvmpt	⊢ ( 𝐼 ∈ 𝑈 → ( ( 𝑖 ∈ 𝑈 ↦ if ( 𝑖 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝑖 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝑖 ∖ { 0 } ) ) , ℝ , < ) ) ) ) ‘ 𝐼 ) = if ( 𝐼 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) )
47	33 46	sylan9eq	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) = if ( 𝐼 = { 0 } , 0 , ( ℩ 𝑔 ∈ ( 𝐼 ∩ 𝑀 ) ( 𝐷 ‘ 𝑔 ) = inf ( ( 𝐷 “ ( 𝐼 ∖ { 0 } ) ) , ℝ , < ) ) ) )

Metamath Proof Explorer

Theorem ig1pval

Proof