Metamath Proof Explorer

Theorem imadrhmcl

Description: The image of a (nontrivial) division ring homomorphism is a division ring. (Contributed by SN, 17-Feb-2025)

Ref Expression
Hypotheses imadrhmcl.r 
|- R = ( N |`s ( F " S ) )
imadrhmcl.0 
|- .0. = ( 0g ` N )
imadrhmcl.h 
|- ( ph -> F e. ( M RingHom N ) )
imadrhmcl.s 
|- ( ph -> S e. ( SubDRing ` M ) )
imadrhmcl.1 
|- ( ph -> ran F =/= { .0. } )
Assertion imadrhmcl 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 imadrhmcl.r 
 |-  R = ( N |`s ( F " S ) )
2 imadrhmcl.0 
 |-  .0. = ( 0g ` N )
3 imadrhmcl.h 
 |-  ( ph -> F e. ( M RingHom N ) )
4 imadrhmcl.s 
 |-  ( ph -> S e. ( SubDRing ` M ) )
5 imadrhmcl.1 
 |-  ( ph -> ran F =/= { .0. } )
6 sdrgsubrg 
 |-  ( S e. ( SubDRing ` M ) -> S e. ( SubRing ` M ) )
7 4 6 syl 
 |-  ( ph -> S e. ( SubRing ` M ) )
8 rhmima 
 |-  ( ( F e. ( M RingHom N ) /\ S e. ( SubRing ` M ) ) -> ( F " S ) e. ( SubRing ` N ) )
9 3 7 8 syl2anc 
 |-  ( ph -> ( F " S ) e. ( SubRing ` N ) )
10 1 subrgring 
 |-  ( ( F " S ) e. ( SubRing ` N ) -> R e. Ring )
11 9 10 syl 
 |-  ( ph -> R e. Ring )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
14 12 13 unitss 
 |-  ( Unit ` R ) C_ ( Base ` R )
15 14 a1i 
 |-  ( ph -> ( Unit ` R ) C_ ( Base ` R ) )
16 eqid 
 |-  ( Base ` M ) = ( Base ` M )
17 eqid 
 |-  ( Base ` N ) = ( Base ` N )
18 16 17 rhmf 
 |-  ( F e. ( M RingHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
19 3 18 syl 
 |-  ( ph -> F : ( Base ` M ) --> ( Base ` N ) )
20 19 adantr 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> F : ( Base ` M ) --> ( Base ` N ) )
21 rhmrcl2 
 |-  ( F e. ( M RingHom N ) -> N e. Ring )
22 3 21 syl 
 |-  ( ph -> N e. Ring )
23 simpr 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( 1r ` R ) = ( 0g ` R ) )
24 eqid 
 |-  ( 1r ` N ) = ( 1r ` N )
25 1 24 subrg1 
 |-  ( ( F " S ) e. ( SubRing ` N ) -> ( 1r ` N ) = ( 1r ` R ) )
26 9 25 syl 
 |-  ( ph -> ( 1r ` N ) = ( 1r ` R ) )
27 26 adantr 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( 1r ` N ) = ( 1r ` R ) )
28 1 2 subrg0 
 |-  ( ( F " S ) e. ( SubRing ` N ) -> .0. = ( 0g ` R ) )
29 9 28 syl 
 |-  ( ph -> .0. = ( 0g ` R ) )
30 29 adantr 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> .0. = ( 0g ` R ) )
31 23 27 30 3eqtr4rd 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> .0. = ( 1r ` N ) )
32 17 2 24 01eq0ring 
 |-  ( ( N e. Ring /\ .0. = ( 1r ` N ) ) -> ( Base ` N ) = { .0. } )
33 22 31 32 syl2an2r 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( Base ` N ) = { .0. } )
34 33 feq3d 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( F : ( Base ` M ) --> ( Base ` N ) <-> F : ( Base ` M ) --> { .0. } ) )
35 20 34 mpbid 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> F : ( Base ` M ) --> { .0. } )
36 2 fvexi 
 |-  .0. e. _V
37 36 fconst2 
 |-  ( F : ( Base ` M ) --> { .0. } <-> F = ( ( Base ` M ) X. { .0. } ) )
38 35 37 sylib 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> F = ( ( Base ` M ) X. { .0. } ) )
39 19 ffnd 
 |-  ( ph -> F Fn ( Base ` M ) )
40 sdrgrcl 
 |-  ( S e. ( SubDRing ` M ) -> M e. DivRing )
41 4 40 syl 
 |-  ( ph -> M e. DivRing )
42 41 drngringd 
 |-  ( ph -> M e. Ring )
43 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
44 16 43 ring0cl 
 |-  ( M e. Ring -> ( 0g ` M ) e. ( Base ` M ) )
45 42 44 syl 
 |-  ( ph -> ( 0g ` M ) e. ( Base ` M ) )
46 45 ne0d 
 |-  ( ph -> ( Base ` M ) =/= (/) )
47 fconst5 
 |-  ( ( F Fn ( Base ` M ) /\ ( Base ` M ) =/= (/) ) -> ( F = ( ( Base ` M ) X. { .0. } ) <-> ran F = { .0. } ) )
48 39 46 47 syl2anc 
 |-  ( ph -> ( F = ( ( Base ` M ) X. { .0. } ) <-> ran F = { .0. } ) )
49 48 adantr 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> ( F = ( ( Base ` M ) X. { .0. } ) <-> ran F = { .0. } ) )
50 38 49 mpbid 
 |-  ( ( ph /\ ( 1r ` R ) = ( 0g ` R ) ) -> ran F = { .0. } )
51 5 50 mteqand 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
52 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
53 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
54 13 52 53 0unit 
 |-  ( R e. Ring -> ( ( 0g ` R ) e. ( Unit ` R ) <-> ( 1r ` R ) = ( 0g ` R ) ) )
55 11 54 syl 
 |-  ( ph -> ( ( 0g ` R ) e. ( Unit ` R ) <-> ( 1r ` R ) = ( 0g ` R ) ) )
56 55 necon3bbid 
 |-  ( ph -> ( -. ( 0g ` R ) e. ( Unit ` R ) <-> ( 1r ` R ) =/= ( 0g ` R ) ) )
57 51 56 mpbird 
 |-  ( ph -> -. ( 0g ` R ) e. ( Unit ` R ) )
58 ssdifsn 
 |-  ( ( Unit ` R ) C_ ( ( Base ` R ) \ { ( 0g ` R ) } ) <-> ( ( Unit ` R ) C_ ( Base ` R ) /\ -. ( 0g ` R ) e. ( Unit ` R ) ) )
59 15 57 58 sylanbrc 
 |-  ( ph -> ( Unit ` R ) C_ ( ( Base ` R ) \ { ( 0g ` R ) } ) )
60 39 fnfund 
 |-  ( ph -> Fun F )
61 1 ressbasss2 
 |-  ( Base ` R ) C_ ( F " S )
62 eldifi 
 |-  ( x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) -> x e. ( Base ` R ) )
63 61 62 sselid 
 |-  ( x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) -> x e. ( F " S ) )
64 fvelima 
 |-  ( ( Fun F /\ x e. ( F " S ) ) -> E. a e. S ( F ` a ) = x )
65 60 63 64 syl2an 
 |-  ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) -> E. a e. S ( F ` a ) = x )
66 simprr 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( F ` a ) = x )
67 simprl 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> a e. S )
68 67 fvresd 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( ( F |` S ) ` a ) = ( F ` a ) )
69 eqid 
 |-  ( M |`s S ) = ( M |`s S )
70 69 resrhm 
 |-  ( ( F e. ( M RingHom N ) /\ S e. ( SubRing ` M ) ) -> ( F |` S ) e. ( ( M |`s S ) RingHom N ) )
71 3 7 70 syl2anc 
 |-  ( ph -> ( F |` S ) e. ( ( M |`s S ) RingHom N ) )
72 df-ima 
 |-  ( F " S ) = ran ( F |` S )
73 eqimss2 
 |-  ( ( F " S ) = ran ( F |` S ) -> ran ( F |` S ) C_ ( F " S ) )
74 72 73 mp1i 
 |-  ( ph -> ran ( F |` S ) C_ ( F " S ) )
75 1 resrhm2b 
 |-  ( ( ( F " S ) e. ( SubRing ` N ) /\ ran ( F |` S ) C_ ( F " S ) ) -> ( ( F |` S ) e. ( ( M |`s S ) RingHom N ) <-> ( F |` S ) e. ( ( M |`s S ) RingHom R ) ) )
76 9 74 75 syl2anc 
 |-  ( ph -> ( ( F |` S ) e. ( ( M |`s S ) RingHom N ) <-> ( F |` S ) e. ( ( M |`s S ) RingHom R ) ) )
77 71 76 mpbid 
 |-  ( ph -> ( F |` S ) e. ( ( M |`s S ) RingHom R ) )
78 77 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( F |` S ) e. ( ( M |`s S ) RingHom R ) )
79 eldifsni 
 |-  ( x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) -> x =/= ( 0g ` R ) )
80 79 ad2antlr 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> x =/= ( 0g ` R ) )
81 68 adantr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> ( ( F |` S ) ` a ) = ( F ` a ) )
82 simpr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> a = ( 0g ` M ) )
83 82 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> ( ( F |` S ) ` a ) = ( ( F |` S ) ` ( 0g ` M ) ) )
84 69 43 subrg0 
 |-  ( S e. ( SubRing ` M ) -> ( 0g ` M ) = ( 0g ` ( M |`s S ) ) )
85 7 84 syl 
 |-  ( ph -> ( 0g ` M ) = ( 0g ` ( M |`s S ) ) )
86 85 fveq2d 
 |-  ( ph -> ( ( F |` S ) ` ( 0g ` M ) ) = ( ( F |` S ) ` ( 0g ` ( M |`s S ) ) ) )
87 rhmghm 
 |-  ( ( F |` S ) e. ( ( M |`s S ) RingHom R ) -> ( F |` S ) e. ( ( M |`s S ) GrpHom R ) )
88 eqid 
 |-  ( 0g ` ( M |`s S ) ) = ( 0g ` ( M |`s S ) )
89 88 52 ghmid 
 |-  ( ( F |` S ) e. ( ( M |`s S ) GrpHom R ) -> ( ( F |` S ) ` ( 0g ` ( M |`s S ) ) ) = ( 0g ` R ) )
90 77 87 89 3syl 
 |-  ( ph -> ( ( F |` S ) ` ( 0g ` ( M |`s S ) ) ) = ( 0g ` R ) )
91 86 90 eqtrd 
 |-  ( ph -> ( ( F |` S ) ` ( 0g ` M ) ) = ( 0g ` R ) )
92 91 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> ( ( F |` S ) ` ( 0g ` M ) ) = ( 0g ` R ) )
93 83 92 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> ( ( F |` S ) ` a ) = ( 0g ` R ) )
94 simplrr 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> ( F ` a ) = x )
95 81 93 94 3eqtr3rd 
 |-  ( ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) /\ a = ( 0g ` M ) ) -> x = ( 0g ` R ) )
96 80 95 mteqand 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> a =/= ( 0g ` M ) )
97 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> S e. ( SubDRing ` M ) )
98 eqid 
 |-  ( Unit ` ( M |`s S ) ) = ( Unit ` ( M |`s S ) )
99 69 43 98 sdrgunit 
 |-  ( S e. ( SubDRing ` M ) -> ( a e. ( Unit ` ( M |`s S ) ) <-> ( a e. S /\ a =/= ( 0g ` M ) ) ) )
100 97 99 syl 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( a e. ( Unit ` ( M |`s S ) ) <-> ( a e. S /\ a =/= ( 0g ` M ) ) ) )
101 67 96 100 mpbir2and 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> a e. ( Unit ` ( M |`s S ) ) )
102 elrhmunit 
 |-  ( ( ( F |` S ) e. ( ( M |`s S ) RingHom R ) /\ a e. ( Unit ` ( M |`s S ) ) ) -> ( ( F |` S ) ` a ) e. ( Unit ` R ) )
103 78 101 102 syl2anc 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( ( F |` S ) ` a ) e. ( Unit ` R ) )
104 68 103 eqeltrrd 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> ( F ` a ) e. ( Unit ` R ) )
105 66 104 eqeltrrd 
 |-  ( ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) /\ ( a e. S /\ ( F ` a ) = x ) ) -> x e. ( Unit ` R ) )
106 65 105 rexlimddv 
 |-  ( ( ph /\ x e. ( ( Base ` R ) \ { ( 0g ` R ) } ) ) -> x e. ( Unit ` R ) )
107 59 106 eqelssd 
 |-  ( ph -> ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) )
108 12 13 52 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) )
109 11 107 108 sylanbrc 
 |-  ( ph -> R e. DivRing )