Theorem rspsn0

Description: A principal ideal (an ideal generated by one element) in a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 12-Jul-2026)

	Ref	Expression
Hypotheses	elrspsn.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elrspsn.2	⊢ · = ( .r ‘ 𝑅 )
	elrspsn.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
Assertion	rspsn0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝑋 } ) = { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } )

Proof

Step	Hyp	Ref	Expression
1		elrspsn.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elrspsn.2	⊢ · = ( .r ‘ 𝑅 )
3		elrspsn.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4	1 2 3	elrspsn	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑖 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) ) )
5		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Ring )
6		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
7		simplr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8	1 2 5 6 7	ringcld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 𝑋 ) ∈ 𝐵 )
9		eleq1	⊢ ( 𝑖 = ( 𝑥 · 𝑋 ) → ( 𝑖 ∈ 𝐵 ↔ ( 𝑥 · 𝑋 ) ∈ 𝐵 ) )
10	8 9	syl5ibrcom	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑖 = ( 𝑥 · 𝑋 ) → 𝑖 ∈ 𝐵 ) )
11	10	rexlimdva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) → 𝑖 ∈ 𝐵 ) )
12	11	pm4.71rd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) ↔ ( 𝑖 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) ) ) )
13	4 12	bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑖 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ( 𝑖 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) ) ) )
14		rabid	⊢ ( 𝑖 ∈ { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } ↔ ( 𝑖 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) ) )
15	13 14	bitr4di	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑖 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑖 ∈ { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } ) )
16	15	alrimiv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ∀ 𝑖 ( 𝑖 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑖 ∈ { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } ) )
17		nfcv	⊢ Ⅎ 𝑖 ( 𝐾 ‘ { 𝑋 } )
18		nfrab1	⊢ Ⅎ 𝑖 { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) }
19	17 18	cleqf	⊢ ( ( 𝐾 ‘ { 𝑋 } ) = { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } ↔ ∀ 𝑖 ( 𝑖 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑖 ∈ { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } ) )
20	16 19	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝑋 } ) = { 𝑖 ∈ 𝐵 ∣ ∃ 𝑥 ∈ 𝐵 𝑖 = ( 𝑥 · 𝑋 ) } )