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
|- .x. = ( .r ` R )
rspsnel.3
|- K = ( RSpan ` R )
Assertion rspsnel
|- ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. B I = ( x .x. X ) ) )

Proof

Step Hyp Ref Expression
1 rspsnel.1
 |-  B = ( Base ` R )
2 rspsnel.2
 |-  .x. = ( .r ` R )
3 rspsnel.3
 |-  K = ( RSpan ` R )
4 rlmlmod
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
5 simpr
 |-  ( ( R e. Ring /\ X e. B ) -> X e. B )
6 5 1 eleqtrdi
 |-  ( ( R e. Ring /\ X e. B ) -> X e. ( 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 ` R ) = ( .s ` ( ringLMod ` R ) )
11 2 10 eqtri
 |-  .x. = ( .s ` ( 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 ) e. LMod /\ X e. ( Base ` R ) ) -> ( I e. ( K ` { X } ) <-> E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) ) )
15 4 6 14 syl2an2r
 |-  ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) ) )
16 rlmsca
 |-  ( R e. Ring -> R = ( Scalar ` ( ringLMod ` R ) ) )
17 16 adantr
 |-  ( ( R e. Ring /\ X e. B ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
18 17 fveq2d
 |-  ( ( R e. Ring /\ X e. B ) -> ( Base ` R ) = ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) )
19 1 18 eqtr2id
 |-  ( ( R e. Ring /\ X e. B ) -> ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) = B )
20 19 rexeqdv
 |-  ( ( R e. Ring /\ X e. B ) -> ( E. x e. ( Base ` ( Scalar ` ( ringLMod ` R ) ) ) I = ( x .x. X ) <-> E. x e. B I = ( x .x. X ) ) )
21 15 20 bitrd
 |-  ( ( R e. Ring /\ X e. B ) -> ( I e. ( K ` { X } ) <-> E. x e. B I = ( x .x. X ) ) )