Metamath Proof Explorer


Theorem brrici

Description: Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025)

Ref Expression
Assertion brrici F R RingIso S R 𝑟 S

Proof

Step Hyp Ref Expression
1 ne0i F R RingIso S R RingIso S
2 brric R 𝑟 S R RingIso S
3 1 2 sylibr F R RingIso S R 𝑟 S