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
subdrgint.2 φ R DivRing
subdrgint.3 φ S SubRing R
subdrgint.4 φ S
subdrgint.5 φ s S R 𝑠 s DivRing
Assertion subdrgint φ L DivRing

Proof

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