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 ∧ 𝐼 ∈ 𝑈 ) → 𝐼 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝐼 ) } ) )