This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )