Theorem subrgring

Description: A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Hypothesis	subrgring.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
Assertion	subrgring	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		subrgring.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	2 3	issubrg	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) )
5	4	simplbi	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) )
6	5	simprd	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝐴 ) ∈ Ring )
7	1 6	eqeltrid	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )