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

Metamath Proof Explorer

Theorem ig1prsp

Description: Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses ig1pval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ig1pval.g ⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
ig1pcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
ig1prsp.k ⊢ 𝐾 = ( RSpan ‘ 𝑃 )
Assertion ig1prsp ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝐼 ) } ) )

Proof

Step Hyp Ref Expression
1 ig1pval.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ig1pval.g ⊢ 𝐺 = ( idlGen1p ‘ 𝑅 )
3 ig1pcl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
4 ig1prsp.k ⊢ 𝐾 = ( RSpan ‘ 𝑃 )
5 1 2 3 ig1pcl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 )
6 eqid ⊢ ( ∥r ‘ 𝑃 ) = ( ∥r ‘ 𝑃 )
7 1 2 3 6 ig1pdvds ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ( ∥r ‘ 𝑃 ) 𝑥 )
8 7 3expa ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝐼 ) ( ∥r ‘ 𝑃 ) 𝑥 )
9 8 ralrimiva ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝐼 ) ( ∥r ‘ 𝑃 ) 𝑥 )
10 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
11 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12 10 11 syl ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ Ring )
13 12 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → 𝑃 ∈ Ring )
14 simpr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ∈ 𝑈 )
15 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
16 15 3 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
17 16 adantl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
18 17 5 sseldd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐺 ‘ 𝐼 ) ∈ ( Base ‘ 𝑃 ) )
19 15 3 4 6 lidldvgen ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ ( 𝐺 ‘ 𝐼 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝐼 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝐼 ) } ) ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝐼 ) ( ∥r ‘ 𝑃 ) 𝑥 ) ) )
20 13 14 18 19 syl3anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝐼 ) } ) ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝐼 ) ( ∥r ‘ 𝑃 ) 𝑥 ) ) )
21 5 9 20 mpbir2and ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝐼 ) } ) )