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 โŠข ๐ต = ( Base โ€˜ ๐‘… )
rspsnel.2 โŠข ยท = ( .r โ€˜ ๐‘… )
rspsnel.3 โŠข ๐พ = ( RSpan โ€˜ ๐‘… )
Assertion rspsnel ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐ผ โˆˆ ( ๐พ โ€˜ { ๐‘‹ } ) โ†” โˆƒ ๐‘ฅ โˆˆ ๐ต ๐ผ = ( ๐‘ฅ ยท ๐‘‹ ) ) )

Proof

Step Hyp Ref Expression
1 rspsnel.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 rspsnel.2 โŠข ยท = ( .r โ€˜ ๐‘… )
3 rspsnel.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 lspsnel โŠข ( ( ( 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 โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐ผ โˆˆ ( ๐พ โ€˜ { ๐‘‹ } ) โ†” โˆƒ ๐‘ฅ โˆˆ ๐ต ๐ผ = ( ๐‘ฅ ยท ๐‘‹ ) ) )