Theorem lpigen

Description: An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

	Ref	Expression
Hypotheses	lpigen.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	lpigen.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
	lpigen.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion	lpigen	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		lpigen.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2		lpigen.p	⊢ 𝑃 = ( LPIdeal ‘ 𝑅 )
3		lpigen.d	⊢ ∥ = ( ∥r ‘ 𝑅 )
4		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	2 4 5	islpidl	⊢ ( 𝑅 ∈ Ring → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) )
7	6	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) )
8	5 1 4 3	lidldvgen	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ↔ ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) )
9	8	3expa	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ↔ ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) )
10	9	rexbidva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝐼 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) )
11		simpr	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) → ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) )
12	5 1	lidlss	⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
13	12	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → 𝐼 ⊆ ( Base ‘ 𝑅 ) )
14	13	sseld	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝑥 ∈ 𝐼 → 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
15	14	adantrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
16	15	ancrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) ) )
17	11 16	impbid2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ) )
18	17	rexbidv2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) )
19	7 10 18	3bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) )