This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐵 𝐼 = ( 𝑥 · 𝑋 ) ) )