Theorem subrgrcl

Description: Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014)

	Ref	Expression
Assertion	subrgrcl	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3	1 2	issubrg	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) )
4	3	simplbi	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) )
5	4	simpld	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )