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	|- ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) )

Proof

Step	Hyp	Ref	Expression
1		brric	|- ( R ~=r S <-> ( R RingIso S ) =/= (/) )
2		n0	|- ( ( R RingIso S ) =/= (/) <-> E. f f e. ( R RingIso S ) )
3		rimrcl	|- ( f e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) )
4		isrim0	|- ( ( R e. _V /\ S e. _V ) -> ( f e. ( R RingIso S ) <-> ( f e. ( R RingHom S ) /\ `' f e. ( S RingHom R ) ) ) )
5		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
6		eqid	|- ( mulGrp ` S ) = ( mulGrp ` S )
7	5 6	isrhm	|- ( f e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( f e. ( R GrpHom S ) /\ f e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) )
8	7	simplbi	|- ( f e. ( R RingHom S ) -> ( R e. Ring /\ S e. Ring ) )
9	8	adantr	|- ( ( f e. ( R RingHom S ) /\ `' f e. ( S RingHom R ) ) -> ( R e. Ring /\ S e. Ring ) )
10	4 9	syl6bi	|- ( ( R e. _V /\ S e. _V ) -> ( f e. ( R RingIso S ) -> ( R e. Ring /\ S e. Ring ) ) )
11	3 10	mpcom	|- ( f e. ( R RingIso S ) -> ( R e. Ring /\ S e. Ring ) )
12	11	exlimiv	|- ( E. f f e. ( R RingIso S ) -> ( R e. Ring /\ S e. Ring ) )
13	12	pm4.71ri	|- ( E. f f e. ( R RingIso S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) )
14	1 2 13	3bitri	|- ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) )