Theorem subdrgint

Description: The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023)

	Ref	Expression
Hypotheses	subdrgint.1	$$⊢L=R{\upharpoonright }_{𝑠}\bigcap S$$
	subdrgint.2	$$⊢\phi \to R\in \mathrm{DivRing}$$
	subdrgint.3	$$⊢\phi \to S\subseteq \mathrm{SubRing}\left(R\right)$$
	subdrgint.4	$$⊢\phi \to S\ne \varnothing$$
	subdrgint.5	$$⊢\left(\phi \wedge s\in S\right)\to R{\upharpoonright }_{𝑠}s\in \mathrm{DivRing}$$
Assertion	subdrgint	$$⊢\phi \to L\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		subdrgint.1	$$⊢L=R{\upharpoonright }_{𝑠}\bigcap S$$
2		subdrgint.2	$$⊢\phi \to R\in \mathrm{DivRing}$$
3		subdrgint.3	$$⊢\phi \to S\subseteq \mathrm{SubRing}\left(R\right)$$
4		subdrgint.4	$$⊢\phi \to S\ne \varnothing$$
5		subdrgint.5	$$⊢\left(\phi \wedge s\in S\right)\to R{\upharpoonright }_{𝑠}s\in \mathrm{DivRing}$$
6		subrgint	$$⊢\left(S\subseteq \mathrm{SubRing}\left(R\right)\wedge S\ne \varnothing \right)\to \bigcap S\in \mathrm{SubRing}\left(R\right)$$
7	3 4 6	syl2anc	$$⊢\phi \to \bigcap S\in \mathrm{SubRing}\left(R\right)$$
8	1	subrgring	$$⊢\bigcap S\in \mathrm{SubRing}\left(R\right)\to L\in \mathrm{Ring}$$
9	7 8	syl	$$⊢\phi \to L\in \mathrm{Ring}$$
10	1	fveq2i	$$⊢{\mathrm{mulGrp}}_L={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}$$
11	10	oveq1i	$$⊢{\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)$$
12		eqid	$$⊢R{\upharpoonright }_{𝑠}\bigcap S=R{\upharpoonright }_{𝑠}\bigcap S$$
13		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
14	12 13	mgpress	$$⊢\left(R\in \mathrm{DivRing}\wedge \bigcap S\in \mathrm{SubRing}\left(R\right)\right)\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap S={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}$$
15	2 7 14	syl2anc	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap S={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}$$
16	15	oveq1d	$$⊢\phi \to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap S\right){\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)$$
17		difssd	$$⊢\phi \to {\mathrm{Base}}_L\setminus \left\{0_L\right\}\subseteq {\mathrm{Base}}_L$$
18		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
19	18	subrgss	$$⊢\bigcap S\in \mathrm{SubRing}\left(R\right)\to \bigcap S\subseteq {\mathrm{Base}}_R$$
20	1 18	ressbas2	$$⊢\bigcap S\subseteq {\mathrm{Base}}_R\to \bigcap S={\mathrm{Base}}_L$$
21	7 19 20	3syl	$$⊢\phi \to \bigcap S={\mathrm{Base}}_L$$
22	17 21	sseqtrrd	$$⊢\phi \to {\mathrm{Base}}_L\setminus \left\{0_L\right\}\subseteq \bigcap S$$
23		ressabs	$$⊢\left(\bigcap S\in \mathrm{SubRing}\left(R\right)\wedge {\mathrm{Base}}_L\setminus \left\{0_L\right\}\subseteq \bigcap S\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap S\right){\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)$$
24	7 22 23	syl2anc	$$⊢\phi \to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap S\right){\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)$$
25	16 24	eqtr3d	$$⊢\phi \to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)$$
26		intiin	$$⊢\bigcap S=\bigcap _{s\in S}s$$
27	26 21	syl5reqr	$$⊢\phi \to {\mathrm{Base}}_L=\bigcap _{s\in S}s$$
28	27	difeq1d	$$⊢\phi \to {\mathrm{Base}}_L\setminus \left\{0_L\right\}=\bigcap _{s\in S}s\setminus \left\{0_L\right\}$$
29	28	oveq2d	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(\bigcap _{s\in S}s\setminus \left\{0_L\right\}\right)$$
30		vex	$$⊢s\in \mathrm{V}$$
31	30	difexi	$$⊢s\setminus \left\{0_L\right\}\in \mathrm{V}$$
32	31	dfiin3	$$⊢\bigcap _{s\in S}\left(s\setminus \left\{0_L\right\}\right)=\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)$$
33		iindif1	$$⊢S\ne \varnothing \to \bigcap _{s\in S}\left(s\setminus \left\{0_L\right\}\right)=\bigcap _{s\in S}s\setminus \left\{0_L\right\}$$
34	4 33	syl	$$⊢\phi \to \bigcap _{s\in S}\left(s\setminus \left\{0_L\right\}\right)=\bigcap _{s\in S}s\setminus \left\{0_L\right\}$$
35	32 34	syl5eqr	$$⊢\phi \to \bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=\bigcap _{s\in S}s\setminus \left\{0_L\right\}$$
36	35	oveq2d	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(\bigcap _{s\in S}s\setminus \left\{0_L\right\}\right)$$
37		difss	$$⊢{\mathrm{Base}}_R\setminus \left\{0_R\right\}\subseteq {\mathrm{Base}}_R$$
38		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)$$
39	13 18	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
40	38 39	ressbas2	$$⊢{\mathrm{Base}}_R\setminus \left\{0_R\right\}\subseteq {\mathrm{Base}}_R\to {\mathrm{Base}}_R\setminus \left\{0_R\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)}$$
41	37 40	ax-mp	$$⊢{\mathrm{Base}}_R\setminus \left\{0_R\right\}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)}$$
42	41	fvexi	$$⊢{\mathrm{Base}}_R\setminus \left\{0_R\right\}\in \mathrm{V}$$
43		iinssiun	$$⊢S\ne \varnothing \to \bigcap _{s\in S}\left(s\setminus \left\{0_L\right\}\right)\subseteq \bigcup _{s\in S}\left(s\setminus \left\{0_L\right\}\right)$$
44	4 43	syl	$$⊢\phi \to \bigcap _{s\in S}\left(s\setminus \left\{0_L\right\}\right)\subseteq \bigcup _{s\in S}\left(s\setminus \left\{0_L\right\}\right)$$
45		subrgsubg	$$⊢s\in \mathrm{SubRing}\left(R\right)\to s\in \mathrm{SubGrp}\left(R\right)$$
46	45	ssriv	$$⊢\mathrm{SubRing}\left(R\right)\subseteq \mathrm{SubGrp}\left(R\right)$$
47	3 46	sstrdi	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(R\right)$$
48		subgint	$$⊢\left(S\subseteq \mathrm{SubGrp}\left(R\right)\wedge S\ne \varnothing \right)\to \bigcap S\in \mathrm{SubGrp}\left(R\right)$$
49	47 4 48	syl2anc	$$⊢\phi \to \bigcap S\in \mathrm{SubGrp}\left(R\right)$$
50		eqid	$$⊢0_R=0_R$$
51	1 50	subg0	$$⊢\bigcap S\in \mathrm{SubGrp}\left(R\right)\to 0_R=0_L$$
52	49 51	syl	$$⊢\phi \to 0_R=0_L$$
53	52	adantr	$$⊢\left(\phi \wedge s\in S\right)\to 0_R=0_L$$
54	53	sneqd	$$⊢\left(\phi \wedge s\in S\right)\to \left\{0_R\right\}=\left\{0_L\right\}$$
55	54	difeq2d	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_R\right\}=s\setminus \left\{0_L\right\}$$
56	3	sselda	$$⊢\left(\phi \wedge s\in S\right)\to s\in \mathrm{SubRing}\left(R\right)$$
57	18	subrgss	$$⊢s\in \mathrm{SubRing}\left(R\right)\to s\subseteq {\mathrm{Base}}_R$$
58	56 57	syl	$$⊢\left(\phi \wedge s\in S\right)\to s\subseteq {\mathrm{Base}}_R$$
59	58	ssdifd	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_R\right\}\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}$$
60	55 59	eqsstrrd	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_L\right\}\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}$$
61	60	iunssd	$$⊢\phi \to \bigcup _{s\in S}\left(s\setminus \left\{0_L\right\}\right)\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}$$
62	44 61	sstrd	$$⊢\phi \to \bigcap _{s\in S}\left(s\setminus \left\{0_L\right\}\right)\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}$$
63	32 62	eqsstrrid	$$⊢\phi \to \bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}$$
64		ressabs	$$⊢\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\in \mathrm{V}\wedge \bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)$$
65	42 63 64	sylancr	$$⊢\phi \to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)$$
66	18 50 38	drngmgp	$$⊢R\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\in \mathrm{Grp}$$
67	2 66	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\in \mathrm{Grp}$$
68	67	adantr	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\in \mathrm{Grp}$$
69	60 41	sseqtrdi	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_L\right\}\subseteq {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)}$$
70		ressabs	$$⊢\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\in \mathrm{V}\wedge s\setminus \left\{0_L\right\}\subseteq {\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)$$
71	42 60 70	sylancr	$$⊢\left(\phi \wedge s\in S\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)$$
72		eqid	$$⊢R{\upharpoonright }_{𝑠}s=R{\upharpoonright }_{𝑠}s$$
73	72 13	mgpress	$$⊢\left(R\in \mathrm{DivRing}\wedge s\in S\right)\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}s={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
74	2 73	sylan	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}s={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
75	55	eqcomd	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_L\right\}=s\setminus \left\{0_R\right\}$$
76	74 75	oveq12d	$$⊢\left(\phi \wedge s\in S\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}s\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_R\right\}\right)$$
77		simpr	$$⊢\left(\phi \wedge s\in S\right)\to s\in S$$
78		difssd	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_L\right\}\subseteq s$$
79		ressabs	$$⊢\left(s\in S\wedge s\setminus \left\{0_L\right\}\subseteq s\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}s\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)$$
80	77 78 79	syl2anc	$$⊢\left(\phi \wedge s\in S\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}s\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)$$
81	76 80	eqtr3d	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_R\right\}\right)={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)$$
82	72 18	ressbas2	$$⊢s\subseteq {\mathrm{Base}}_R\to s={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
83	56 57 82	3syl	$$⊢\left(\phi \wedge s\in S\right)\to s={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
84	72 50	subrg0	$$⊢s\in \mathrm{SubRing}\left(R\right)\to 0_R=0_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
85	56 84	syl	$$⊢\left(\phi \wedge s\in S\right)\to 0_R=0_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
86	85	sneqd	$$⊢\left(\phi \wedge s\in S\right)\to \left\{0_R\right\}=\left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}$$
87	83 86	difeq12d	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_R\right\}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}\setminus \left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}$$
88	87	oveq2d	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_R\right\}\right)={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}\setminus \left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}\right)$$
89		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
90		eqid	$$⊢0_{\left(R{\upharpoonright }_{𝑠}s\right)}=0_{\left(R{\upharpoonright }_{𝑠}s\right)}$$
91		eqid	$$⊢{\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}\setminus \left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}\right)={\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}\setminus \left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}\right)$$
92	89 90 91	drngmgp	$$⊢R{\upharpoonright }_{𝑠}s\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}\setminus \left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}\right)\in \mathrm{Grp}$$
93	5 92	syl	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}s\right)}\setminus \left\{0_{\left(R{\upharpoonright }_{𝑠}s\right)}\right\}\right)\in \mathrm{Grp}$$
94	88 93	eqeltrd	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}s\right)}{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_R\right\}\right)\in \mathrm{Grp}$$
95	81 94	eqeltrrd	$$⊢\left(\phi \wedge s\in S\right)\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
96	71 95	eqeltrd	$$⊢\left(\phi \wedge s\in S\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
97		eqid	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)}$$
98	97	issubg	$$⊢s\setminus \left\{0_L\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)\leftrightarrow \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\in \mathrm{Grp}\wedge s\setminus \left\{0_L\right\}\subseteq {\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)}\wedge \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\left(s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}\right)$$
99	68 69 96 98	syl3anbrc	$$⊢\left(\phi \wedge s\in S\right)\to s\setminus \left\{0_L\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)$$
100	99	ralrimiva	$$⊢\phi \to \forall s\in Ss\setminus \left\{0_L\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)$$
101		eqid	$$⊢\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=\left(s\in S⟼s\setminus \left\{0_L\right\}\right)$$
102	101	rnmptss	$$⊢\forall s\in Ss\setminus \left\{0_L\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)\to \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\subseteq \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)$$
103	100 102	syl	$$⊢\phi \to \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\subseteq \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)$$
104		dmmptg	$$⊢\forall s\in Ss\setminus \left\{0_L\right\}\in \mathrm{V}\to \mathrm{dom}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=S$$
105		difexg	$$⊢s\in S\to s\setminus \left\{0_L\right\}\in \mathrm{V}$$
106	104 105	mprg	$$⊢\mathrm{dom}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=S$$
107	106	a1i	$$⊢\phi \to \mathrm{dom}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=S$$
108	107 4	eqnetrd	$$⊢\phi \to \mathrm{dom}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\ne \varnothing$$
109		dm0rn0	$$⊢\mathrm{dom}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=\varnothing \leftrightarrow \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=\varnothing$$
110	109	necon3bii	$$⊢\mathrm{dom}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\ne \varnothing \leftrightarrow \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\ne \varnothing$$
111	108 110	sylib	$$⊢\phi \to \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\ne \varnothing$$
112		subgint	$$⊢\left(\mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\subseteq \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)\wedge \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\ne \varnothing \right)\to \bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)$$
113	103 111 112	syl2anc	$$⊢\phi \to \bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)$$
114		eqid	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)=\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)$$
115	114	subggrp	$$⊢\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right)\to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
116	113 115	syl	$$⊢\phi \to \left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_R\setminus \left\{0_R\right\}\right)\right){\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
117	65 116	eqeltrrd	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\bigcap \mathrm{ran}\left(s\in S⟼s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
118	36 117	eqeltrrd	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(\bigcap _{s\in S}s\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
119	29 118	eqeltrd	$$⊢\phi \to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
120	25 119	eqeltrd	$$⊢\phi \to {\mathrm{mulGrp}}_{\left(R{\upharpoonright }_{𝑠}\bigcap S\right)}{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
121	11 120	eqeltrid	$$⊢\phi \to {\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}$$
122		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
123		eqid	$$⊢0_L=0_L$$
124		eqid	$$⊢{\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)={\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)$$
125	122 123 124	isdrng2	$$⊢L\in \mathrm{DivRing}\leftrightarrow \left(L\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_L{\upharpoonright }_{𝑠}\left({\mathrm{Base}}_L\setminus \left\{0_L\right\}\right)\in \mathrm{Grp}\right)$$
126	9 121 125	sylanbrc	$$⊢\phi \to L\in \mathrm{DivRing}$$