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 )