Metamath Proof Explorer

Theorem rimco

Description: The composition of ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised 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