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

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 ⊢ 𝑅 = ( 𝑁 ↾s ( 𝐹 “ 𝑆 ) )
imadrhmcl.0 ⊢ 0 = ( 0g ‘ 𝑁 )
imadrhmcl.h ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) )
imadrhmcl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝑀 ) )
imadrhmcl.1 ⊢ ( 𝜑 → ran 𝐹 ≠ { 0 } )
Assertion imadrhmcl ( 𝜑 → 𝑅 ∈ DivRing )

Proof

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