Theorem brric2

Description: The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019)

	Ref	Expression
Assertion	brric2	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brric	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2		n0	⊢ ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
3		rimrcl	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )
4		isrim0	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ) ) )
5		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
6		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
7	5 6	isrhm	⊢ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) )
8	7	simplbi	⊢ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
9	8	adantr	⊢ ( ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝑓 ∈ ( 𝑆 RingHom 𝑅 ) ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
10	4 9	syl6bi	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ) )
11	3 10	mpcom	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
12	11	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
13	12	pm4.71ri	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )
14	1 2 13	3bitri	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )