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 = Base R
rspsnel.2 · ˙ = R
rspsnel.3 K = RSpan R
Assertion rspsnel R Ring X B I K X x B I = x · ˙ X

Proof

Step Hyp Ref Expression
1 rspsnel.1 B = Base R
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 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 = 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 Base R I K X x Base Scalar ringLMod R I = x · ˙ X
15 4 6 14 syl2an2r R Ring X B I K X x Base Scalar ringLMod R I = 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 Base R = Base Scalar ringLMod R
19 1 18 eqtr2id R Ring X B Base Scalar ringLMod R = B
20 19 rexeqdv R Ring X B x Base Scalar ringLMod R I = x · ˙ X x B I = x · ˙ X
21 15 20 bitrd R Ring X B I K X x B I = x · ˙ X