Metamath Proof Explorer


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 A SubRing R A SubRng R

Proof

Step Hyp Ref Expression
1 eqid Base R = Base R
2 eqid 1 R = 1 R
3 1 2 issubrg A SubRing R R Ring R 𝑠 A Ring A Base R 1 R A
4 ringrng R Ring R Rng
5 4 ad2antrr R Ring R 𝑠 A Ring A Base R 1 R A R Rng
6 ringrng R 𝑠 A Ring R 𝑠 A Rng
7 6 ad2antlr R Ring R 𝑠 A Ring A Base R 1 R A R 𝑠 A Rng
8 simprl R Ring R 𝑠 A Ring A Base R 1 R A A Base R
9 1 issubrng A SubRng R R Rng R 𝑠 A Rng A Base R
10 5 7 8 9 syl3anbrc R Ring R 𝑠 A Ring A Base R 1 R A A SubRng R
11 3 10 sylbi A SubRing R A SubRng R