Metamath Proof Explorer

Theorem rngoisoco

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

Ref Expression
Assertion rngoisoco 
|- ( ( ( 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 ) )

Proof

Step Hyp Ref Expression
1 rngoisohom 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) )
2 1 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) )
3 2 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) )
4 rngoisohom 
 |-  ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) )
5 4 3expa 
 |-  ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) )
6 5 3adantl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G e. ( S RingOpsHom T ) )
7 3 6 anim12dan 
 |-  ( ( ( 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 ) ) )
8 rngohomco 
 |-  ( ( ( 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 ) )
9 7 8 syldan 
 |-  ( ( ( 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 ) )
10 eqid 
 |-  ( 1st ` S ) = ( 1st ` S )
11 eqid 
 |-  ran ( 1st ` S ) = ran ( 1st ` S )
12 eqid 
 |-  ( 1st ` T ) = ( 1st ` T )
13 eqid 
 |-  ran ( 1st ` T ) = ran ( 1st ` T )
14 10 11 12 13 rngoiso1o 
 |-  ( ( S e. RingOps /\ T e. RingOps /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) )
15 14 3expa 
 |-  ( ( ( S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) )
16 15 3adantl1 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ G e. ( S RingOpsIso T ) ) -> G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) )
17 16 adantrl 
 |-  ( ( ( 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 ) )
18 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
19 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
20 18 19 10 11 rngoiso1o 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) )
21 20 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) )
22 21 3adantl3 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ T e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) )
23 22 adantrr 
 |-  ( ( ( 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 ) )
24 f1oco 
 |-  ( ( G : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` T ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( G o. F ) : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` T ) )
25 17 23 24 syl2anc 
 |-  ( ( ( 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 ) )
26 18 19 12 13 isrngoiso 
 |-  ( ( 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 ) ) ) )
27 26 3adant2 
 |-  ( ( 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 ) ) ) )
28 27 adantr 
 |-  ( ( ( 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 ) ) ) )
29 9 25 28 mpbir2and 
 |-  ( ( ( 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 ) )