Theorem ig1pval2

Description: Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015) (Proof shortened by AV, 25-Sep-2020)

	Ref	Expression
Hypotheses	ig1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ig1pval.g	⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
	ig1pval2.z	⊢ 0 = ( 0g ‘ 𝑃 )
Assertion	ig1pval2	⊢ ( 𝑅 ∈ Ring → ( 𝐺 ‘ { 0 } ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		ig1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ig1pval.g	⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
3		ig1pval2.z	⊢ 0 = ( 0g ‘ 𝑃 )
4	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
5		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
6	5 3	lidl0	⊢ ( 𝑃 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑃 ) )
7	4 6	syl	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑃 ) )
8		eqid	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
9		eqid	⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
10	1 2 3 5 8 9	ig1pval	⊢ ( ( 𝑅 ∈ Ring ∧ { 0 } ∈ ( LIdeal ‘ 𝑃 ) ) → ( 𝐺 ‘ { 0 } ) = if ( { 0 } = { 0 } , 0 , ( ℩ 𝑔 ∈ ( { 0 } ∩ ( Monic1p ‘ 𝑅 ) ) ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑅 ) “ ( { 0 } ∖ { 0 } ) ) , ℝ , < ) ) ) )
11	7 10	mpdan	⊢ ( 𝑅 ∈ Ring → ( 𝐺 ‘ { 0 } ) = if ( { 0 } = { 0 } , 0 , ( ℩ 𝑔 ∈ ( { 0 } ∩ ( Monic1p ‘ 𝑅 ) ) ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑅 ) “ ( { 0 } ∖ { 0 } ) ) , ℝ , < ) ) ) )
12		eqid	⊢ { 0 } = { 0 }
13	12	iftruei	⊢ if ( { 0 } = { 0 } , 0 , ( ℩ 𝑔 ∈ ( { 0 } ∩ ( Monic1p ‘ 𝑅 ) ) ( ( deg1 ‘ 𝑅 ) ‘ 𝑔 ) = inf ( ( ( deg1 ‘ 𝑅 ) “ ( { 0 } ∖ { 0 } ) ) , ℝ , < ) ) ) = 0
14	11 13	eqtrdi	⊢ ( 𝑅 ∈ Ring → ( 𝐺 ‘ { 0 } ) = 0 )