# Metamath Proof Explorer

## 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}{↾}_{𝑠}\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}{↾}_{𝑠}{s}\in \mathrm{DivRing}$
Assertion subdrgint ${⊢}{\phi }\to {L}\in \mathrm{DivRing}$

### Proof

Step Hyp Ref Expression
1 subdrgint.1 ${⊢}{L}={R}{↾}_{𝑠}\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}{↾}_{𝑠}{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}{↾}_{𝑠}\bigcap {S}\right)}$
11 10 oveq1i ${⊢}{\mathrm{mulGrp}}_{{L}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}\bigcap {S}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)$
12 eqid ${⊢}{R}{↾}_{𝑠}\bigcap {S}={R}{↾}_{𝑠}\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}}{↾}_{𝑠}\bigcap {S}={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}\bigcap {S}\right)}$
15 2 7 14 syl2anc ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\bigcap {S}={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}\bigcap {S}\right)}$
16 15 oveq1d ${⊢}{\phi }\to \left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\bigcap {S}\right){↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}\bigcap {S}\right)}{↾}_{𝑠}\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}}{↾}_{𝑠}\bigcap {S}\right){↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)$
24 7 22 23 syl2anc ${⊢}{\phi }\to \left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\bigcap {S}\right){↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)$
25 16 24 eqtr3d ${⊢}{\phi }\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}\bigcap {S}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\bigcap \mathrm{ran}\left({s}\in {S}⟼{s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\bigcap \mathrm{ran}\left({s}\in {S}⟼{s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\bigcap \mathrm{ran}\left({s}\in {S}⟼{s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\in \mathrm{Grp}$
67 2 66 syl ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)$
72 eqid ${⊢}{R}{↾}_{𝑠}{s}={R}{↾}_{𝑠}{s}$
73 72 13 mgpress ${⊢}\left({R}\in \mathrm{DivRing}\wedge {s}\in {S}\right)\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{s}={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}$
74 2 73 sylan ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{s}={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{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}}{↾}_{𝑠}{s}\right){↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\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}}{↾}_{𝑠}{s}\right){↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}{s}\right){↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)$
81 76 80 eqtr3d ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({s}\setminus \left\{{0}_{{R}}\right\}\right)={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)$
82 72 18 ressbas2 ${⊢}{s}\subseteq {\mathrm{Base}}_{{R}}\to {s}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}$
83 56 57 82 3syl ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {s}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}$
84 72 50 subrg0 ${⊢}{s}\in \mathrm{SubRing}\left({R}\right)\to {0}_{{R}}={0}_{\left({R}{↾}_{𝑠}{s}\right)}$
85 56 84 syl ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {0}_{{R}}={0}_{\left({R}{↾}_{𝑠}{s}\right)}$
86 85 sneqd ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to \left\{{0}_{{R}}\right\}=\left\{{0}_{\left({R}{↾}_{𝑠}{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}{↾}_{𝑠}{s}\right)}\setminus \left\{{0}_{\left({R}{↾}_{𝑠}{s}\right)}\right\}$
88 87 oveq2d ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({s}\setminus \left\{{0}_{{R}}\right\}\right)={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}\setminus \left\{{0}_{\left({R}{↾}_{𝑠}{s}\right)}\right\}\right)$
89 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}$
90 eqid ${⊢}{0}_{\left({R}{↾}_{𝑠}{s}\right)}={0}_{\left({R}{↾}_{𝑠}{s}\right)}$
91 eqid ${⊢}{\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}\setminus \left\{{0}_{\left({R}{↾}_{𝑠}{s}\right)}\right\}\right)={\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}\setminus \left\{{0}_{\left({R}{↾}_{𝑠}{s}\right)}\right\}\right)$
92 89 90 91 drngmgp ${⊢}{R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}\setminus \left\{{0}_{\left({R}{↾}_{𝑠}{s}\right)}\right\}\right)\in \mathrm{Grp}$
93 5 92 syl ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{\left({R}{↾}_{𝑠}{s}\right)}\setminus \left\{{0}_{\left({R}{↾}_{𝑠}{s}\right)}\right\}\right)\in \mathrm{Grp}$
94 88 93 eqeltrd ${⊢}\left({\phi }\wedge {s}\in {S}\right)\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}{s}\right)}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\left({s}\setminus \left\{{0}_{{L}}\right\}\right)\in \mathrm{Grp}$
97 eqid ${⊢}{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)↔\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)}\wedge \left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)$
100 99 ralrimiva ${⊢}{\phi }\to \forall {s}\in {S}\phantom{\rule{.4em}{0ex}}{s}\setminus \left\{{0}_{{L}}\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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 {S}\phantom{\rule{.4em}{0ex}}{s}\setminus \left\{{0}_{{L}}\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)$
104 dmmptg ${⊢}\forall {s}\in {S}\phantom{\rule{.4em}{0ex}}{s}\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 ↔\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 ↔\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)$
114 eqid ${⊢}\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\bigcap \mathrm{ran}\left({s}\in {S}⟼{s}\setminus \left\{{0}_{{L}}\right\}\right)=\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right)\to \left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{R}}\setminus \left\{{0}_{{R}}\right\}\right)\right){↾}_{𝑠}\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}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left(\bigcap _{{s}\in {S}}{s}\setminus \left\{{0}_{{L}}\right\}\right)\in \mathrm{Grp}$
119 29 118 eqeltrd ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)\in \mathrm{Grp}$
120 25 119 eqeltrd ${⊢}{\phi }\to {\mathrm{mulGrp}}_{\left({R}{↾}_{𝑠}\bigcap {S}\right)}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)\in \mathrm{Grp}$
121 11 120 eqeltrid ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{L}}{↾}_{𝑠}\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}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)={\mathrm{mulGrp}}_{{L}}{↾}_{𝑠}\left({\mathrm{Base}}_{{L}}\setminus \left\{{0}_{{L}}\right\}\right)$
125 122 123 124 isdrng2 ${⊢}{L}\in \mathrm{DivRing}↔\left({L}\in \mathrm{Ring}\wedge {\mathrm{mulGrp}}_{{L}}{↾}_{𝑠}\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}$