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

Proof

Step Hyp Ref Expression
1 elrspsn.1 
 |-  B = ( Base ` R )
2 elrspsn.2 
 |-  .x. = ( .r ` R )
3 elrspsn.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 ellspsn 
 |-  ( ( ( 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 ) ) )