Metamath Proof Explorer


Theorem rictr

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

Ref Expression
Assertion rictr ( ( 𝑅𝑟 𝑆𝑆𝑟 𝑇 ) → 𝑅𝑟 𝑇 )

Proof

Step Hyp Ref Expression
1 brric ( 𝑅𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2 brric ( 𝑆𝑟 𝑇 ↔ ( 𝑆 RingIso 𝑇 ) ≠ ∅ )
3 n0 ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
4 n0 ( ( 𝑆 RingIso 𝑇 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) )
5 exdistrv ( ∃ 𝑓𝑔 ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ) )
6 rimco ( ( 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( 𝑔𝑓 ) ∈ ( 𝑅 RingIso 𝑇 ) )
7 brrici ( ( 𝑔𝑓 ) ∈ ( 𝑅 RingIso 𝑇 ) → 𝑅𝑟 𝑇 )
8 6 7 syl ( ( 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ∧ 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) → 𝑅𝑟 𝑇 )
9 8 ancoms ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ) → 𝑅𝑟 𝑇 )
10 9 exlimivv ( ∃ 𝑓𝑔 ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ) → 𝑅𝑟 𝑇 )
11 5 10 sylbir ( ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ ∃ 𝑔 𝑔 ∈ ( 𝑆 RingIso 𝑇 ) ) → 𝑅𝑟 𝑇 )
12 3 4 11 syl2anb ( ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ∧ ( 𝑆 RingIso 𝑇 ) ≠ ∅ ) → 𝑅𝑟 𝑇 )
13 1 2 12 syl2anb ( ( 𝑅𝑟 𝑆𝑆𝑟 𝑇 ) → 𝑅𝑟 𝑇 )