Theorem subrgsubrng

Description: A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025)

	Ref	Expression
Assertion	subrgsubrng	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3	1 2	issubrg	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) )
4		ringrng	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
5	4	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → 𝑅 ∈ Rng )
6		ringrng	⊢ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
7	6	ad2antlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
8		simprl	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
9	1	issubrng	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) )
10	5 7 8 9	syl3anbrc	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )
11	3 10	sylbi	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )