Theorem rspsnid

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

	Ref	Expression
Hypotheses	rspsnid.b	|- B = ( Base ` R )
	rspsnid.k	|- K = ( RSpan ` R )
Assertion	rspsnid	|- ( ( R e. Ring /\ G e. B ) -> G e. ( K ` { G } ) )

Proof

Step	Hyp	Ref	Expression
1		rspsnid.b	|- B = ( Base ` R )
2		rspsnid.k	|- K = ( RSpan ` R )
3		snssi	|- ( G e. B -> { G } C_ B )
4	2 1	rspssid	|- ( ( R e. Ring /\ { G } C_ B ) -> { G } C_ ( K ` { G } ) )
5	3 4	sylan2	|- ( ( R e. Ring /\ G e. B ) -> { G } C_ ( K ` { G } ) )
6		snssg	|- ( G e. B -> ( G e. ( K ` { G } ) <-> { G } C_ ( K ` { G } ) ) )
7	6	adantl	|- ( ( R e. Ring /\ G e. B ) -> ( G e. ( K ` { G } ) <-> { G } C_ ( K ` { G } ) ) )
8	5 7	mpbird	|- ( ( R e. Ring /\ G e. B ) -> G e. ( K ` { G } ) )