This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspidlid

Description: The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses rspidlid.1 ⊢ K = RSpan ⁡ R
rspidlid.2 ⊢ U = LIdeal ⁡ R
Assertion rspidlid ⊢ R ∈ Ring ∧ I ∈ U → K ⁡ I = I

Proof

Step Hyp Ref Expression
1 rspidlid.1 ⊢ K = RSpan ⁡ R
2 rspidlid.2 ⊢ U = LIdeal ⁡ R
3 ssid ⊢ I ⊆ I
4 1 2 rspssp ⊢ R ∈ Ring ∧ I ∈ U ∧ I ⊆ I → K ⁡ I ⊆ I
5 3 4 mp3an3 ⊢ R ∈ Ring ∧ I ∈ U → K ⁡ I ⊆ I
6 eqid ⊢ Base R = Base R
7 6 2 lidlss ⊢ I ∈ U → I ⊆ Base R
8 1 6 rspssid ⊢ R ∈ Ring ∧ I ⊆ Base R → I ⊆ K ⁡ I
9 7 8 sylan2 ⊢ R ∈ Ring ∧ I ∈ U → I ⊆ K ⁡ I
10 5 9 eqssd ⊢ R ∈ Ring ∧ I ∈ U → K ⁡ I = I