Metamath Proof Explorer


Theorem rictr

Description: Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025)

Ref Expression
Assertion rictr
|- ( ( R ~=r S /\ S ~=r T ) -> R ~=r T )

Proof

Step Hyp Ref Expression
1 brric
 |-  ( R ~=r S <-> ( R RingIso S ) =/= (/) )
2 brric
 |-  ( S ~=r T <-> ( S RingIso T ) =/= (/) )
3 n0
 |-  ( ( R RingIso S ) =/= (/) <-> E. f f e. ( R RingIso S ) )
4 n0
 |-  ( ( S RingIso T ) =/= (/) <-> E. g g e. ( S RingIso T ) )
5 exdistrv
 |-  ( E. f E. g ( f e. ( R RingIso S ) /\ g e. ( S RingIso T ) ) <-> ( E. f f e. ( R RingIso S ) /\ E. g g e. ( S RingIso T ) ) )
6 rimco
 |-  ( ( g e. ( S RingIso T ) /\ f e. ( R RingIso S ) ) -> ( g o. f ) e. ( R RingIso T ) )
7 brrici
 |-  ( ( g o. f ) e. ( R RingIso T ) -> R ~=r T )
8 6 7 syl
 |-  ( ( g e. ( S RingIso T ) /\ f e. ( R RingIso S ) ) -> R ~=r T )
9 8 ancoms
 |-  ( ( f e. ( R RingIso S ) /\ g e. ( S RingIso T ) ) -> R ~=r T )
10 9 exlimivv
 |-  ( E. f E. g ( f e. ( R RingIso S ) /\ g e. ( S RingIso T ) ) -> R ~=r T )
11 5 10 sylbir
 |-  ( ( E. f f e. ( R RingIso S ) /\ E. g g e. ( S RingIso T ) ) -> R ~=r T )
12 3 4 11 syl2anb
 |-  ( ( ( R RingIso S ) =/= (/) /\ ( S RingIso T ) =/= (/) ) -> R ~=r T )
13 1 2 12 syl2anb
 |-  ( ( R ~=r S /\ S ~=r T ) -> R ~=r T )