Metamath Proof Explorer


Theorem rimco

Description: The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025)

Ref Expression
Assertion rimco F S RingIso T G R RingIso S F G R RingIso T

Proof

Step Hyp Ref Expression
1 isrim0 F S RingIso T F S RingHom T F -1 T RingHom S
2 isrim0 G R RingIso S G R RingHom S G -1 S RingHom R
3 rhmco F S RingHom T G R RingHom S F G R RingHom T
4 cnvco F G -1 = G -1 F -1
5 rhmco G -1 S RingHom R F -1 T RingHom S G -1 F -1 T RingHom R
6 5 ancoms F -1 T RingHom S G -1 S RingHom R G -1 F -1 T RingHom R
7 4 6 eqeltrid F -1 T RingHom S G -1 S RingHom R F G -1 T RingHom R
8 3 7 anim12i F S RingHom T G R RingHom S F -1 T RingHom S G -1 S RingHom R F G R RingHom T F G -1 T RingHom R
9 8 an4s F S RingHom T F -1 T RingHom S G R RingHom S G -1 S RingHom R F G R RingHom T F G -1 T RingHom R
10 1 2 9 syl2anb F S RingIso T G R RingIso S F G R RingHom T F G -1 T RingHom R
11 isrim0 F G R RingIso T F G R RingHom T F G -1 T RingHom R
12 10 11 sylibr F S RingIso T G R RingIso S F G R RingIso T