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	⊢ 𝐿 = ( 𝑅 ↾s ∩ 𝑆 )
	subdrgint.2	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	subdrgint.3	⊢ ( 𝜑 → 𝑆 ⊆ ( SubRing ‘ 𝑅 ) )
	subdrgint.4	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
	subdrgint.5	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑅 ↾s 𝑠 ) ∈ DivRing )
Assertion	subdrgint	⊢ ( 𝜑 → 𝐿 ∈ DivRing )

Proof

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