Metamath Proof Explorer

Theorem subrgid

Description: Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Hypothesis subrgss.1 ⊢ B = Base R
Assertion subrgid ⊢ R ∈ Ring → B ∈ SubRing ⁡ R

Proof

Step Hyp Ref Expression
1 subrgss.1 ⊢ B = Base R
2 id ⊢ R ∈ Ring → R ∈ Ring
3 1 ressid ⊢ R ∈ Ring → R ↾ 𝑠 B = R
4 3 2 eqeltrd ⊢ R ∈ Ring → R ↾ 𝑠 B ∈ Ring
5 eqid ⊢ 1 R = 1 R
6 1 5 ringidcl ⊢ R ∈ Ring → 1 R ∈ B
7 ssid ⊢ B ⊆ B
8 6 7 jctil ⊢ R ∈ Ring → B ⊆ B ∧ 1 R ∈ B
9 1 5 issubrg ⊢ B ∈ SubRing ⁡ R ↔ R ∈ Ring ∧ R ↾ 𝑠 B ∈ Ring ∧ B ⊆ B ∧ 1 R ∈ B
10 2 4 8 9 syl21anbrc ⊢ R ∈ Ring → B ∈ SubRing ⁡ R