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 ↾_{𝑠} ⋂ S$
	subdrgint.2	$⊢ φ \to R \in DivRing$
	subdrgint.3	$⊢ φ \to S \subseteq SubRing (R)$
	subdrgint.4	$⊢ φ \to S \neq \emptyset$
	subdrgint.5	$⊢ (φ \land s \in S) \to R ↾_{𝑠} s \in DivRing$
Assertion	subdrgint	$⊢ φ \to L \in DivRing$

Proof

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

Metamath Proof Explorer

Theorem subdrgint

Proof