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

Proof

Step Hyp Ref Expression
1 elrspsn.1 ⊢ B = Base R
2 elrspsn.2 ⊢ · ˙ = ⋅ R
3 elrspsn.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 ellspsn ⊢ 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