Theorem rngoisoco

Description: The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Assertion	rngoisoco	Could not format assertion : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) e. ( R RingOpsIso T ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rngoisohom	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) with typecode |-
2	1	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) with typecode |-
3	2	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) ) with typecode |-
4		rngoisohom	Could not format ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) ) : No typesetting found for |- ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) ) with typecode |-
5	4	3expa	Could not format ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) ) with typecode |-
6	5	3adantl1	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) ) with typecode |-
7	3 6	anim12dan	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) with typecode |-
8		rngohomco	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ G e. ( S RingOpsHom T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) with typecode |-
9	7 8	syldan	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) e. ( R RingOpsHom T ) ) with typecode |-
10		eqid	$$⊢1^{st}\left(S\right)=1^{st}\left(S\right)$$
11		eqid	$$⊢\mathrm{ran}{1}^{st}\left(S\right)=\mathrm{ran}{1}^{st}\left(S\right)$$
12		eqid	$$⊢1^{st}\left(T\right)=1^{st}\left(T\right)$$
13		eqid	$$⊢\mathrm{ran}{1}^{st}\left(T\right)=\mathrm{ran}{1}^{st}\left(T\right)$$
14	10 11 12 13	rngoiso1o	Could not format ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) : No typesetting found for |- ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) with typecode |-
15	14	3expa	Could not format ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) with typecode |-
16	15	3adantl1	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) with typecode |-
17	16	adantrl	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) ) with typecode |-
18		eqid	$$⊢1^{st}\left(R\right)=1^{st}\left(R\right)$$
19		eqid	$$⊢\mathrm{ran}{1}^{st}\left(R\right)=\mathrm{ran}{1}^{st}\left(R\right)$$
20	18 19 10 11	rngoiso1o	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) with typecode |-
21	20	3expa	Could not format ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) with typecode |-
22	21	3adantl3	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) with typecode |-
23	22	adantrr	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) with typecode |-
24		f1oco	$$⊢\left(G:\mathrm{ran}{1}^{st}\left(S\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(T\right)\wedge F:\mathrm{ran}{1}^{st}\left(R\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(S\right)\right)\to \left(G\circ F\right):\mathrm{ran}{1}^{st}\left(R\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(T\right)$$
25	17 23 24	syl2anc	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) with typecode |-
26	18 19 12 13	isrngoiso	Could not format ( ( R e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsIso T ) <-> ( ( G o. F ) e. ( R RingOpsHom T ) /\ ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsIso T ) <-> ( ( G o. F ) e. ( R RingOpsHom T ) /\ ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) ) ) with typecode |-
27	26	3adant2	Could not format ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsIso T ) <-> ( ( G o. F ) e. ( R RingOpsHom T ) /\ ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) -> ( ( G o. F ) e. ( R RingOpsIso T ) <-> ( ( G o. F ) e. ( R RingOpsHom T ) /\ ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) ) ) with typecode |-
28	27	adantr	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( ( G o. F ) e. ( R RingOpsIso T ) <-> ( ( G o. F ) e. ( R RingOpsHom T ) /\ ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( ( G o. F ) e. ( R RingOpsIso T ) <-> ( ( G o. F ) e. ( R RingOpsHom T ) /\ ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) ) ) ) with typecode |-
29	9 25 28	mpbir2and	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) e. ( R RingOpsIso T ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ ( F e. ( R RingOpsIso S ) /\ G e. ( S RingOpsIso T ) ) ) -> ( G o. F ) e. ( R RingOpsIso T ) ) with typecode |-