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 ⊢B=BaseR
rspsnel.2 ⊢·˙=⋅R
rspsnel.3 ⊢K=RSpan⁡R
Assertion rspsnel ⊢R∈Ring∧X∈B→I∈K⁡X↔∃x∈BI=x·˙X

Proof

Step Hyp Ref Expression
1 rspsnel.1 ⊢B=BaseR
2 rspsnel.2 ⊢·˙=⋅R
3 rspsnel.3 ⊢K=RSpan⁡R
4 rlmlmod ⊢R∈Ring→ringLMod⁡R∈LMod
5 simpr ⊢R∈Ring∧X∈B→X∈B
6 5 1 eleqtrdi ⊢R∈Ring∧X∈B→X∈BaseR
7 eqid ⊢Scalar⁡ringLMod⁡R=Scalar⁡ringLMod⁡R
8 eqid ⊢BaseScalar⁡ringLMod⁡R=BaseScalar⁡ringLMod⁡R
9 rlmbas ⊢BaseR=BaseringLMod⁡R
10 rlmvsca ⊢⋅R=⋅ringLMod⁡R
11 2 10 eqtri ⊢·˙=⋅ringLMod⁡R
12 rspval ⊢RSpan⁡R=LSpan⁡ringLMod⁡R
13 3 12 eqtri ⊢K=LSpan⁡ringLMod⁡R
14 7 8 9 11 13 lspsnel ⊢ringLMod⁡R∈LMod∧X∈BaseR→I∈K⁡X↔∃x∈BaseScalar⁡ringLMod⁡RI=x·˙X
15 4 6 14 syl2an2r ⊢R∈Ring∧X∈B→I∈K⁡X↔∃x∈BaseScalar⁡ringLMod⁡RI=x·˙X
16 rlmsca ⊢R∈Ring→R=Scalar⁡ringLMod⁡R
17 16 adantr ⊢R∈Ring∧X∈B→R=Scalar⁡ringLMod⁡R
18 17 fveq2d ⊢R∈Ring∧X∈B→BaseR=BaseScalar⁡ringLMod⁡R
19 1 18 eqtr2id ⊢R∈Ring∧X∈B→BaseScalar⁡ringLMod⁡R=B
20 19 rexeqdv ⊢R∈Ring∧X∈B→∃x∈BaseScalar⁡ringLMod⁡RI=x·˙X↔∃x∈BI=x·˙X
21 15 20 bitrd ⊢R∈Ring∧X∈B→I∈K⁡X↔∃x∈BI=x·˙X