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 |`s |^| S )
	subdrgint.2	|- ( ph -> R e. DivRing )
	subdrgint.3	|- ( ph -> S C_ ( SubRing ` R ) )
	subdrgint.4	|- ( ph -> S =/= (/) )
	subdrgint.5	|- ( ( ph /\ s e. S ) -> ( R |`s s ) e. DivRing )
Assertion	subdrgint	|- ( ph -> L e. DivRing )

Proof

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