This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ricdrng1

Description: A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025)

Ref Expression
Assertion ricdrng1 
|- ( ( R ~=r S /\ R e. DivRing ) -> S e. DivRing )

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 1 2 bitri 
 |-  ( R ~=r S <-> E. f f e. ( R RingIso S ) )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 4 5 rimf1o 
 |-  ( f e. ( R RingIso S ) -> f : ( Base ` R ) -1-1-onto-> ( Base ` S ) )
7 f1ofo 
 |-  ( f : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> f : ( Base ` R ) -onto-> ( Base ` S ) )
8 foima 
 |-  ( f : ( Base ` R ) -onto-> ( Base ` S ) -> ( f " ( Base ` R ) ) = ( Base ` S ) )
9 6 7 8 3syl 
 |-  ( f e. ( R RingIso S ) -> ( f " ( Base ` R ) ) = ( Base ` S ) )
10 9 oveq2d 
 |-  ( f e. ( R RingIso S ) -> ( S |`s ( f " ( Base ` R ) ) ) = ( S |`s ( Base ` S ) ) )
11 rimrcl2 
 |-  ( f e. ( R RingIso S ) -> S e. Ring )
12 5 ressid 
 |-  ( S e. Ring -> ( S |`s ( Base ` S ) ) = S )
13 11 12 syl 
 |-  ( f e. ( R RingIso S ) -> ( S |`s ( Base ` S ) ) = S )
14 10 13 eqtr2d 
 |-  ( f e. ( R RingIso S ) -> S = ( S |`s ( f " ( Base ` R ) ) ) )
15 14 adantr 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> S = ( S |`s ( f " ( Base ` R ) ) ) )
16 eqid 
 |-  ( S |`s ( f " ( Base ` R ) ) ) = ( S |`s ( f " ( Base ` R ) ) )
17 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
18 rimrhm 
 |-  ( f e. ( R RingIso S ) -> f e. ( R RingHom S ) )
19 18 adantr 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> f e. ( R RingHom S ) )
20 4 sdrgid 
 |-  ( R e. DivRing -> ( Base ` R ) e. ( SubDRing ` R ) )
21 20 adantl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( Base ` R ) e. ( SubDRing ` R ) )
22 forn 
 |-  ( f : ( Base ` R ) -onto-> ( Base ` S ) -> ran f = ( Base ` S ) )
23 6 7 22 3syl 
 |-  ( f e. ( R RingIso S ) -> ran f = ( Base ` S ) )
24 23 adantr 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ran f = ( Base ` S ) )
25 rhmrcl2 
 |-  ( f e. ( R RingHom S ) -> S e. Ring )
26 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
27 5 26 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) )
28 18 25 27 3syl 
 |-  ( f e. ( R RingIso S ) -> ( 1r ` S ) e. ( Base ` S ) )
29 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
30 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
31 29 30 drngunz 
 |-  ( R e. DivRing -> ( 1r ` R ) =/= ( 0g ` R ) )
32 31 adantl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( 1r ` R ) =/= ( 0g ` R ) )
33 f1of1 
 |-  ( f : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> f : ( Base ` R ) -1-1-> ( Base ` S ) )
34 6 33 syl 
 |-  ( f e. ( R RingIso S ) -> f : ( Base ` R ) -1-1-> ( Base ` S ) )
35 drngring 
 |-  ( R e. DivRing -> R e. Ring )
36 4 30 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
37 35 36 syl 
 |-  ( R e. DivRing -> ( 1r ` R ) e. ( Base ` R ) )
38 4 29 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
39 35 38 syl 
 |-  ( R e. DivRing -> ( 0g ` R ) e. ( Base ` R ) )
40 37 39 jca 
 |-  ( R e. DivRing -> ( ( 1r ` R ) e. ( Base ` R ) /\ ( 0g ` R ) e. ( Base ` R ) ) )
41 f1veqaeq 
 |-  ( ( f : ( Base ` R ) -1-1-> ( Base ` S ) /\ ( ( 1r ` R ) e. ( Base ` R ) /\ ( 0g ` R ) e. ( Base ` R ) ) ) -> ( ( f ` ( 1r ` R ) ) = ( f ` ( 0g ` R ) ) -> ( 1r ` R ) = ( 0g ` R ) ) )
42 34 40 41 syl2an 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( ( f ` ( 1r ` R ) ) = ( f ` ( 0g ` R ) ) -> ( 1r ` R ) = ( 0g ` R ) ) )
43 42 imp 
 |-  ( ( ( f e. ( R RingIso S ) /\ R e. DivRing ) /\ ( f ` ( 1r ` R ) ) = ( f ` ( 0g ` R ) ) ) -> ( 1r ` R ) = ( 0g ` R ) )
44 32 43 mteqand 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( f ` ( 1r ` R ) ) =/= ( f ` ( 0g ` R ) ) )
45 30 26 rhm1 
 |-  ( f e. ( R RingHom S ) -> ( f ` ( 1r ` R ) ) = ( 1r ` S ) )
46 19 45 syl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( f ` ( 1r ` R ) ) = ( 1r ` S ) )
47 rhmghm 
 |-  ( f e. ( R RingHom S ) -> f e. ( R GrpHom S ) )
48 29 17 ghmid 
 |-  ( f e. ( R GrpHom S ) -> ( f ` ( 0g ` R ) ) = ( 0g ` S ) )
49 19 47 48 3syl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( f ` ( 0g ` R ) ) = ( 0g ` S ) )
50 44 46 49 3netr3d 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( 1r ` S ) =/= ( 0g ` S ) )
51 nelsn 
 |-  ( ( 1r ` S ) =/= ( 0g ` S ) -> -. ( 1r ` S ) e. { ( 0g ` S ) } )
52 50 51 syl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> -. ( 1r ` S ) e. { ( 0g ` S ) } )
53 nelne1 
 |-  ( ( ( 1r ` S ) e. ( Base ` S ) /\ -. ( 1r ` S ) e. { ( 0g ` S ) } ) -> ( Base ` S ) =/= { ( 0g ` S ) } )
54 28 52 53 syl2an2r 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( Base ` S ) =/= { ( 0g ` S ) } )
55 24 54 eqnetrd 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ran f =/= { ( 0g ` S ) } )
56 16 17 19 21 55 imadrhmcl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> ( S |`s ( f " ( Base ` R ) ) ) e. DivRing )
57 15 56 eqeltrd 
 |-  ( ( f e. ( R RingIso S ) /\ R e. DivRing ) -> S e. DivRing )
58 57 ex 
 |-  ( f e. ( R RingIso S ) -> ( R e. DivRing -> S e. DivRing ) )
59 58 exlimiv 
 |-  ( E. f f e. ( R RingIso S ) -> ( R e. DivRing -> S e. DivRing ) )
60 59 imp 
 |-  ( ( E. f f e. ( R RingIso S ) /\ R e. DivRing ) -> S e. DivRing )
61 3 60 sylanb 
 |-  ( ( R ~=r S /\ R e. DivRing ) -> S e. DivRing )