Metamath Proof Explorer


Theorem rspsnel

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

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

Proof

Step Hyp Ref Expression
1 rspsnel.1 𝐵 = ( Base ‘ 𝑅 )
2 rspsnel.2 · = ( .r𝑅 )
3 rspsnel.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 lspsnel ( ( ( 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 ∧ 𝑋𝐵 ) → ( 𝐼 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑥𝐵 𝐼 = ( 𝑥 · 𝑋 ) ) )