Theorem subrgid

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

	Ref	Expression
Hypothesis	subrgss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		subrgss.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
3	1	ressid	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
4	3 2	eqeltrd	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ↾s 𝐵 ) ∈ Ring )
5		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6	1 5	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
7		ssid	⊢ 𝐵 ⊆ 𝐵
8	6 7	jctil	⊢ ( 𝑅 ∈ Ring → ( 𝐵 ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) )
9	1 5	issubrg	⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐵 ) ∈ Ring ) ∧ ( 𝐵 ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) ) )
10	2 4 8 9	syl21anbrc	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )