Theorem elrspsn

Description: Membership in a principal ideal. Analogous to ellspsn . (Contributed by Thierry Arnoux, 15-Jan-2024)

	Ref	Expression
Hypotheses	elrspsn.1	|- B = ( Base ` R )
	elrspsn.2	|- .x. = ( .r ` R )
	elrspsn.3	|- K = ( RSpan ` R )
Assertion	elrspsn	|- ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. B I = ( x .x. X ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrspsn.1	|- B = ( Base ` R )
2		elrspsn.2	|- .x. = ( .r ` R )
3		elrspsn.3	|- K = ( RSpan ` R )
4		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
5		simpr	|- ( ( R e. Ring /\ X e. B ) -> X e. B )
6	5 1	eleqtrdi	|- ( ( R e. Ring /\ X e. B ) -> X e. ( Base ` R ) )
7		eqid	|- ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
8		eqid	|- ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) )
9		rlmbas	|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
10		rlmvsca	|- ( .r ` R ) = ( .s ` ( ringLMod ` R ) )
11	2 10	eqtri	|- .x. = ( .s ` ( ringLMod ` R ) )
12		rspval	|- ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
13	3 12	eqtri	|- K = ( LSpan ` ( ringLMod ` R ) )
14	7 8 9 11 13	ellspsn	|- ( ( ( ringLMod ` R ) e. LMod /\ X e. ( Base ` R ) ) -> ( I e. ( K ` { X } ) <-> E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) ) )
15	4 6 14	syl2an2r	|- ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) ) )
16		rlmsca	|- ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) )
17	16	adantr	|- ( ( R e. Ring /\ X e. B ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
18	17	fveq2d	|- ( ( R e. Ring /\ X e. B ) -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
19	1 18	eqtr2id	|- ( ( R e. Ring /\ X e. B ) -> ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = B )
20	19	rexeqdv	|- ( ( R e. Ring /\ X e. B ) -> ( E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) <-> E. x e. B I = ( x .x. X ) ) )
21	15 20	bitrd	|- ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. B I = ( x .x. X ) ) )