Theorem isriscg

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Assertion	isriscg	Could not format assertion : No typesetting found for |- ( ( R e. A /\ S e. B ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢r=R\to \left(r\in \mathrm{RingOps}\leftrightarrow R\in \mathrm{RingOps}\right)$$
2	1	anbi1d	$$⊢r=R\to \left(\left(r\in \mathrm{RingOps}\wedge s\in \mathrm{RingOps}\right)\leftrightarrow \left(R\in \mathrm{RingOps}\wedge s\in \mathrm{RingOps}\right)\right)$$
3		oveq1	Could not format ( r = R -> ( r RingOpsIso s ) = ( R RingOpsIso s ) ) : No typesetting found for |- ( r = R -> ( r RingOpsIso s ) = ( R RingOpsIso s ) ) with typecode |-
4	3	eleq2d	Could not format ( r = R -> ( f e. ( r RingOpsIso s ) <-> f e. ( R RingOpsIso s ) ) ) : No typesetting found for |- ( r = R -> ( f e. ( r RingOpsIso s ) <-> f e. ( R RingOpsIso s ) ) ) with typecode |-
5	4	exbidv	Could not format ( r = R -> ( E. f f e. ( r RingOpsIso s ) <-> E. f f e. ( R RingOpsIso s ) ) ) : No typesetting found for |- ( r = R -> ( E. f f e. ( r RingOpsIso s ) <-> E. f f e. ( R RingOpsIso s ) ) ) with typecode |-
6	2 5	anbi12d	Could not format ( r = R -> ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) <-> ( ( R e. RingOps /\ s e. RingOps ) /\ E. f f e. ( R RingOpsIso s ) ) ) ) : No typesetting found for |- ( r = R -> ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) <-> ( ( R e. RingOps /\ s e. RingOps ) /\ E. f f e. ( R RingOpsIso s ) ) ) ) with typecode |-
7		eleq1	$$⊢s=S\to \left(s\in \mathrm{RingOps}\leftrightarrow S\in \mathrm{RingOps}\right)$$
8	7	anbi2d	$$⊢s=S\to \left(\left(R\in \mathrm{RingOps}\wedge s\in \mathrm{RingOps}\right)\leftrightarrow \left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\right)\right)$$
9		oveq2	Could not format ( s = S -> ( R RingOpsIso s ) = ( R RingOpsIso S ) ) : No typesetting found for |- ( s = S -> ( R RingOpsIso s ) = ( R RingOpsIso S ) ) with typecode |-
10	9	eleq2d	Could not format ( s = S -> ( f e. ( R RingOpsIso s ) <-> f e. ( R RingOpsIso S ) ) ) : No typesetting found for |- ( s = S -> ( f e. ( R RingOpsIso s ) <-> f e. ( R RingOpsIso S ) ) ) with typecode |-
11	10	exbidv	Could not format ( s = S -> ( E. f f e. ( R RingOpsIso s ) <-> E. f f e. ( R RingOpsIso S ) ) ) : No typesetting found for |- ( s = S -> ( E. f f e. ( R RingOpsIso s ) <-> E. f f e. ( R RingOpsIso S ) ) ) with typecode |-
12	8 11	anbi12d	Could not format ( s = S -> ( ( ( R e. RingOps /\ s e. RingOps ) /\ E. f f e. ( R RingOpsIso s ) ) <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) : No typesetting found for |- ( s = S -> ( ( ( R e. RingOps /\ s e. RingOps ) /\ E. f f e. ( R RingOpsIso s ) ) <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) with typecode |-
13		df-risc	Could not format ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } : No typesetting found for |- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } with typecode |-
14	6 12 13	brabg	Could not format ( ( R e. A /\ S e. B ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) : No typesetting found for |- ( ( R e. A /\ S e. B ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RingOpsIso S ) ) ) ) with typecode |-