This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )