Theorem elrspsn

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

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

Proof

Step	Hyp	Ref	Expression
1		elrspsn.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elrspsn.2	⊢ · = ( .r ‘ 𝑅 )
3		elrspsn.3	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
5		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
6	5 1	eleqtrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
7		eqid	⊢ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) )
8		eqid	⊢ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
9		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
10		rlmvsca	⊢ ( .r ‘ 𝑅 ) = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
11	2 10	eqtri	⊢ · = ( ·𝑠 ‘ ( ringLMod ‘ 𝑅 ) )
12		rspval	⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
13	3 12	eqtri	⊢ 𝐾 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
14	7 8 9 11 13	ellspsn	⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) 𝐼 = ( 𝑥 · 𝑋 ) ) )
15	4 6 14	syl2an2r	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) 𝐼 = ( 𝑥 · 𝑋 ) ) )
16		rlmsca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
17	16	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
18	17	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) )
19	1 18	eqtr2id	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) = 𝐵 )
20	19	rexeqdv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) ) 𝐼 = ( 𝑥 · 𝑋 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐼 = ( 𝑥 · 𝑋 ) ) )
21	15 20	bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐵 𝐼 = ( 𝑥 · 𝑋 ) ) )