Metamath Proof Explorer

Theorem rspsn0

Description: A principal ideal (an ideal generated by one element) in a ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 12-Jul-2026)

Ref Expression
Hypotheses elrspsn.1 ⊢ B = Base R
elrspsn.2 ⊢ · ˙ = ⋅ R
elrspsn.3 ⊢ K = RSpan ⁡ R
Assertion rspsn0 ⊢ R ∈ Ring ∧ X ∈ B → K ⁡ X = i ∈ B | ∃ 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 1 2 3 elrspsn ⊢ R ∈ Ring ∧ X ∈ B → i ∈ K ⁡ X ↔ ∃ x ∈ B i = x · ˙ X
5 simpll ⊢ R ∈ Ring ∧ X ∈ B ∧ x ∈ B → R ∈ Ring
6 simpr ⊢ R ∈ Ring ∧ X ∈ B ∧ x ∈ B → x ∈ B
7 simplr ⊢ R ∈ Ring ∧ X ∈ B ∧ x ∈ B → X ∈ B
8 1 2 5 6 7 ringcld ⊢ R ∈ Ring ∧ X ∈ B ∧ x ∈ B → x · ˙ X ∈ B
9 eleq1 ⊢ i = x · ˙ X → i ∈ B ↔ x · ˙ X ∈ B
10 8 9 syl5ibrcom ⊢ R ∈ Ring ∧ X ∈ B ∧ x ∈ B → i = x · ˙ X → i ∈ B
11 10 rexlimdva ⊢ R ∈ Ring ∧ X ∈ B → ∃ x ∈ B i = x · ˙ X → i ∈ B
12 11 pm4.71rd ⊢ R ∈ Ring ∧ X ∈ B → ∃ x ∈ B i = x · ˙ X ↔ i ∈ B ∧ ∃ x ∈ B i = x · ˙ X
13 4 12 bitrd ⊢ R ∈ Ring ∧ X ∈ B → i ∈ K ⁡ X ↔ i ∈ B ∧ ∃ x ∈ B i = x · ˙ X
14 rabid ⊢ i ∈ i ∈ B | ∃ x ∈ B i = x · ˙ X ↔ i ∈ B ∧ ∃ x ∈ B i = x · ˙ X
15 13 14 bitr4di ⊢ R ∈ Ring ∧ X ∈ B → i ∈ K ⁡ X ↔ i ∈ i ∈ B | ∃ x ∈ B i = x · ˙ X
16 15 alrimiv ⊢ R ∈ Ring ∧ X ∈ B → ∀ i i ∈ K ⁡ X ↔ i ∈ i ∈ B | ∃ x ∈ B i = x · ˙ X
17 nfcv ⊢ Ⅎ _ i K ⁡ X
18 nfrab1 ⊢ Ⅎ _ i i ∈ B | ∃ x ∈ B i = x · ˙ X
19 17 18 cleqf ⊢ K ⁡ X = i ∈ B | ∃ x ∈ B i = x · ˙ X ↔ ∀ i i ∈ K ⁡ X ↔ i ∈ i ∈ B | ∃ x ∈ B i = x · ˙ X
20 16 19 sylibr ⊢ R ∈ Ring ∧ X ∈ B → K ⁡ X = i ∈ B | ∃ x ∈ B i = x · ˙ X