Step | Hyp | Ref
| Expression |
1 | | fldgenval.1 |
. . 3
⊢ 𝐵 = (Base‘𝐹) |
2 | | fldgenval.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ DivRing) |
3 | | fldgenval.3 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
4 | 1, 2, 3 | fldgenval 31905 |
. 2
⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) |
5 | 2 | drngringd 20146 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ Ring) |
6 | | eqid 2738 |
. . . . . 6
⊢ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) = (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) |
7 | | sseq2 3969 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝑥)) |
8 | 7 | elrab 3644 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ↔ (𝑥 ∈ (SubDRing‘𝐹) ∧ 𝑆 ⊆ 𝑥)) |
9 | 8 | biimpi 215 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} → (𝑥 ∈ (SubDRing‘𝐹) ∧ 𝑆 ⊆ 𝑥)) |
10 | 9 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → (𝑥 ∈ (SubDRing‘𝐹) ∧ 𝑆 ⊆ 𝑥)) |
11 | 10 | simpld 496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → 𝑥 ∈ (SubDRing‘𝐹)) |
12 | | issdrg 20214 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (SubDRing‘𝐹) ↔ (𝐹 ∈ DivRing ∧ 𝑥 ∈ (SubRing‘𝐹) ∧ (𝐹 ↾s 𝑥) ∈ DivRing)) |
13 | 12 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑥 ∈ (SubDRing‘𝐹) → 𝑥 ∈ (SubRing‘𝐹)) |
14 | 11, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → 𝑥 ∈ (SubRing‘𝐹)) |
15 | 14 | ex 414 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} → 𝑥 ∈ (SubRing‘𝐹))) |
16 | 15 | ssrdv 3949 |
. . . . . 6
⊢ (𝜑 → {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ⊆ (SubRing‘𝐹)) |
17 | | sseq2 3969 |
. . . . . . . 8
⊢ (𝑎 = 𝐵 → (𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵)) |
18 | 1 | sdrgid 20215 |
. . . . . . . . 9
⊢ (𝐹 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝐹)) |
19 | 2, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐹)) |
20 | 17, 19, 3 | elrabd 3646 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) |
21 | 20 | ne0d 4294 |
. . . . . 6
⊢ (𝜑 → {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ≠ ∅) |
22 | 12 | simp3bi 1148 |
. . . . . . 7
⊢ (𝑥 ∈ (SubDRing‘𝐹) → (𝐹 ↾s 𝑥) ∈ DivRing) |
23 | 11, 22 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → (𝐹 ↾s 𝑥) ∈ DivRing) |
24 | 6, 2, 16, 21, 23 | subdrgint 20223 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈
DivRing) |
25 | 24 | drngringd 20146 |
. . . 4
⊢ (𝜑 → (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈ Ring) |
26 | | intss1 4923 |
. . . . 5
⊢ (𝐵 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} → ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵) |
27 | 20, 26 | syl 17 |
. . . 4
⊢ (𝜑 → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵) |
28 | | issdrg 20214 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (SubDRing‘𝐹) ↔ (𝐹 ∈ DivRing ∧ 𝑎 ∈ (SubRing‘𝐹) ∧ (𝐹 ↾s 𝑎) ∈ DivRing)) |
29 | 28 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑎 ∈ (SubDRing‘𝐹) → 𝑎 ∈ (SubRing‘𝐹)) |
30 | | eqid 2738 |
. . . . . . . . . 10
⊢
(1r‘𝐹) = (1r‘𝐹) |
31 | 30 | subrg1cl 20183 |
. . . . . . . . 9
⊢ (𝑎 ∈ (SubRing‘𝐹) →
(1r‘𝐹)
∈ 𝑎) |
32 | 29, 31 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ (SubDRing‘𝐹) →
(1r‘𝐹)
∈ 𝑎) |
33 | 32 | ad2antlr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐹)) ∧ 𝑆 ⊆ 𝑎) → (1r‘𝐹) ∈ 𝑎) |
34 | 33 | ex 414 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐹)) → (𝑆 ⊆ 𝑎 → (1r‘𝐹) ∈ 𝑎)) |
35 | 34 | ralrimiva 3142 |
. . . . 5
⊢ (𝜑 → ∀𝑎 ∈ (SubDRing‘𝐹)(𝑆 ⊆ 𝑎 → (1r‘𝐹) ∈ 𝑎)) |
36 | | fvex 6853 |
. . . . . 6
⊢
(1r‘𝐹) ∈ V |
37 | 36 | elintrab 4920 |
. . . . 5
⊢
((1r‘𝐹) ∈ ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ↔ ∀𝑎 ∈ (SubDRing‘𝐹)(𝑆 ⊆ 𝑎 → (1r‘𝐹) ∈ 𝑎)) |
38 | 35, 37 | sylibr 233 |
. . . 4
⊢ (𝜑 → (1r‘𝐹) ∈ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) |
39 | 1, 30 | issubrg 20175 |
. . . . 5
⊢ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹) ↔ ((𝐹 ∈ Ring ∧ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈ Ring) ∧ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵 ∧ (1r‘𝐹) ∈ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}))) |
40 | 39 | biimpri 227 |
. . . 4
⊢ (((𝐹 ∈ Ring ∧ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈ Ring) ∧ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵 ∧ (1r‘𝐹) ∈ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎})) → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹)) |
41 | 5, 25, 27, 38, 40 | syl22anc 838 |
. . 3
⊢ (𝜑 → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹)) |
42 | | issdrg 20214 |
. . 3
⊢ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubDRing‘𝐹) ↔ (𝐹 ∈ DivRing ∧ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹) ∧ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈
DivRing)) |
43 | 2, 41, 24, 42 | syl3anbrc 1344 |
. 2
⊢ (𝜑 → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubDRing‘𝐹)) |
44 | 4, 43 | eqeltrd 2839 |
1
⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) |