Metamath Proof Explorer


Theorem brric2

Description: The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion brric2 R 𝑟 S R Ring S Ring f f R RingIso S

Proof

Step Hyp Ref Expression
1 brric R 𝑟 S R RingIso S
2 n0 R RingIso S f f R RingIso S
3 rimrcl f R RingIso S R V S V
4 isrim0 R V S V f R RingIso S f R RingHom S f -1 S RingHom R
5 eqid mulGrp R = mulGrp R
6 eqid mulGrp S = mulGrp S
7 5 6 isrhm f R RingHom S R Ring S Ring f R GrpHom S f mulGrp R MndHom mulGrp S
8 7 simplbi f R RingHom S R Ring S Ring
9 8 adantr f R RingHom S f -1 S RingHom R R Ring S Ring
10 4 9 syl6bi R V S V f R RingIso S R Ring S Ring
11 3 10 mpcom f R RingIso S R Ring S Ring
12 11 exlimiv f f R RingIso S R Ring S Ring
13 12 pm4.71ri f f R RingIso S R Ring S Ring f f R RingIso S
14 1 2 13 3bitri R 𝑟 S R Ring S Ring f f R RingIso S