| Step | Hyp | Ref
| Expression |
| 1 | | fldgenval.1 |
. . 3
⊢ 𝐵 = (Base‘𝐹) |
| 2 | | fldgenval.2 |
. . 3
⊢ (𝜑 → 𝐹 ∈ DivRing) |
| 3 | | fldgenval.3 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 4 | 1, 2, 3 | fldgenval 33314 |
. 2
⊢ (𝜑 → (𝐹 fldGen 𝑆) = ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) |
| 5 | 2 | drngringd 20737 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ Ring) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) = (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) |
| 7 | | sseq2 4010 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝑥)) |
| 8 | 7 | elrab 3692 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ↔ (𝑥 ∈ (SubDRing‘𝐹) ∧ 𝑆 ⊆ 𝑥)) |
| 9 | 8 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} → (𝑥 ∈ (SubDRing‘𝐹) ∧ 𝑆 ⊆ 𝑥)) |
| 10 | 9 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → (𝑥 ∈ (SubDRing‘𝐹) ∧ 𝑆 ⊆ 𝑥)) |
| 11 | 10 | simpld 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → 𝑥 ∈ (SubDRing‘𝐹)) |
| 12 | | issdrg 20789 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (SubDRing‘𝐹) ↔ (𝐹 ∈ DivRing ∧ 𝑥 ∈ (SubRing‘𝐹) ∧ (𝐹 ↾s 𝑥) ∈ DivRing)) |
| 13 | 12 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑥 ∈ (SubDRing‘𝐹) → 𝑥 ∈ (SubRing‘𝐹)) |
| 14 | 11, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) → 𝑥 ∈ (SubRing‘𝐹)) |
| 15 | 14 | ex 412 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} → 𝑥 ∈ (SubRing‘𝐹))) |
| 16 | 15 | ssrdv 3989 |
. . . . . 6
⊢ (𝜑 → {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ⊆ (SubRing‘𝐹)) |
| 17 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑎 = 𝐵 → (𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵)) |
| 18 | 1 | sdrgid 20793 |
. . . . . . . . 9
⊢ (𝐹 ∈ DivRing → 𝐵 ∈ (SubDRing‘𝐹)) |
| 19 | 2, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐹)) |
| 20 | 17, 19, 3 | elrabd 3694 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎}) |
| 21 | 20 | ne0d 4342 |
. . . . . 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 20804 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈
DivRing) |
| 25 | 24 | drngringd 20737 |
. . . 4
⊢ (𝜑 → (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈ Ring) |
| 26 | | intss1 4963 |
. . . . 5
⊢ (𝐵 ∈ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} → ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵) |
| 27 | 20, 26 | syl 17 |
. . . 4
⊢ (𝜑 → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵) |
| 28 | | issdrg 20789 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (SubDRing‘𝐹) ↔ (𝐹 ∈ DivRing ∧ 𝑎 ∈ (SubRing‘𝐹) ∧ (𝐹 ↾s 𝑎) ∈ DivRing)) |
| 29 | 28 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝑎 ∈ (SubDRing‘𝐹) → 𝑎 ∈ (SubRing‘𝐹)) |
| 30 | | eqid 2737 |
. . . . . . . . . 10
⊢
(1r‘𝐹) = (1r‘𝐹) |
| 31 | 30 | subrg1cl 20580 |
. . . . . . . . 9
⊢ (𝑎 ∈ (SubRing‘𝐹) →
(1r‘𝐹)
∈ 𝑎) |
| 32 | 29, 31 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ (SubDRing‘𝐹) →
(1r‘𝐹)
∈ 𝑎) |
| 33 | 32 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐹)) ∧ 𝑆 ⊆ 𝑎) → (1r‘𝐹) ∈ 𝑎) |
| 34 | 33 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐹)) → (𝑆 ⊆ 𝑎 → (1r‘𝐹) ∈ 𝑎)) |
| 35 | 34 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑎 ∈ (SubDRing‘𝐹)(𝑆 ⊆ 𝑎 → (1r‘𝐹) ∈ 𝑎)) |
| 36 | | fvex 6919 |
. . . . . 6
⊢
(1r‘𝐹) ∈ V |
| 37 | 36 | elintrab 4960 |
. . . . 5
⊢
((1r‘𝐹) ∈ ∩ {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆 ⊆ 𝑎} ↔ ∀𝑎 ∈ (SubDRing‘𝐹)(𝑆 ⊆ 𝑎 → (1r‘𝐹) ∈ 𝑎)) |
| 38 | 35, 37 | sylibr 234 |
. . . 4
⊢ (𝜑 → (1r‘𝐹) ∈ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) |
| 39 | 1, 30 | issubrg 20571 |
. . . . 5
⊢ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹) ↔ ((𝐹 ∈ Ring ∧ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈ Ring) ∧ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵 ∧ (1r‘𝐹) ∈ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}))) |
| 40 | 39 | biimpri 228 |
. . . 4
⊢ (((𝐹 ∈ Ring ∧ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈ Ring) ∧ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ⊆ 𝐵 ∧ (1r‘𝐹) ∈ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎})) → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹)) |
| 41 | 5, 25, 27, 38, 40 | syl22anc 839 |
. . 3
⊢ (𝜑 → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹)) |
| 42 | | issdrg 20789 |
. . 3
⊢ (∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubDRing‘𝐹) ↔ (𝐹 ∈ DivRing ∧ ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubRing‘𝐹) ∧ (𝐹 ↾s ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎}) ∈
DivRing)) |
| 43 | 2, 41, 24, 42 | syl3anbrc 1344 |
. 2
⊢ (𝜑 → ∩ {𝑎
∈ (SubDRing‘𝐹)
∣ 𝑆 ⊆ 𝑎} ∈ (SubDRing‘𝐹)) |
| 44 | 4, 43 | eqeltrd 2841 |
1
⊢ (𝜑 → (𝐹 fldGen 𝑆) ∈ (SubDRing‘𝐹)) |