This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |`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 )