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 ⊢ 𝐿 = ( 𝑅 ↾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 )