Theorem rspsnid

Description: A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024)

	Ref	Expression
Hypotheses	rspsnid.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rspsnid.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
Assertion	rspsnid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) )

Proof

Step	Hyp	Ref	Expression
1		rspsnid.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rspsnid.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3		snssi	⊢ ( 𝐺 ∈ 𝐵 → { 𝐺 } ⊆ 𝐵 )
4	2 1	rspssid	⊢ ( ( 𝑅 ∈ Ring ∧ { 𝐺 } ⊆ 𝐵 ) → { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) )
5	3 4	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) )
6		snssg	⊢ ( 𝐺 ∈ 𝐵 → ( 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) ) )
7	6	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) ↔ { 𝐺 } ⊆ ( 𝐾 ‘ { 𝐺 } ) ) )
8	5 7	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ ( 𝐾 ‘ { 𝐺 } ) )