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

Metamath Proof Explorer

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 ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∈ 𝑃 ↔ ∃ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 𝑥 ∥ 𝑦 ) )