| Step | Hyp | Ref
| Expression |
| 1 | | evls1fldgencl.2 |
. . . . . . . . 9
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
| 2 | | evls1fldgencl.1 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐸) |
| 3 | | evls1fldgencl.3 |
. . . . . . . . 9
⊢ 𝑃 =
(Poly1‘(𝐸
↾s 𝐹)) |
| 4 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) |
| 5 | | evls1fldgencl.4 |
. . . . . . . . 9
⊢ 𝑈 = (Base‘𝑃) |
| 6 | | evls1fldgencl.5 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ Field) |
| 7 | 6 | fldcrngd 20742 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ CRing) |
| 8 | | evls1fldgencl.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
| 9 | | sdrgsubrg 20792 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸)) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
| 11 | | evls1fldgencl.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝑈) |
| 12 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝐸) = (.r‘𝐸) |
| 13 | | eqid 2737 |
. . . . . . . . 9
⊢
(.g‘(mulGrp‘𝐸)) =
(.g‘(mulGrp‘𝐸)) |
| 14 | | eqid 2737 |
. . . . . . . . 9
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
| 15 | 1, 2, 3, 4, 5, 7, 10, 11, 12, 13, 14 | evls1fpws 22373 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝐺) = (𝑥 ∈ 𝐵 ↦ (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝑥)))))) |
| 16 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑘(.g‘(mulGrp‘𝐸))𝑥) = (𝑘(.g‘(mulGrp‘𝐸))𝐴)) |
| 17 | 16 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝑥)) = (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) |
| 18 | 17 | mpteq2dv 5244 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝑥))) = (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)))) |
| 19 | 18 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝑥)))) = (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))))) |
| 20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝑥)))) = (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))))) |
| 21 | | evls1fldgencl.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 22 | | ovexd 7466 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)))) ∈ V) |
| 23 | 15, 20, 21, 22 | fvmptd 7023 |
. . . . . . 7
⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))))) |
| 24 | 23 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → ((𝑂‘𝐺)‘𝐴) = (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))))) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐸) = (0g‘𝐸) |
| 26 | 7 | crngringd 20243 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ Ring) |
| 27 | 26 | ringabld 20280 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ Abel) |
| 28 | 27 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → 𝐸 ∈ Abel) |
| 29 | | nn0ex 12532 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
| 30 | 29 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → ℕ0 ∈
V) |
| 31 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → 𝑎 ∈ (SubDRing‘𝐸)) |
| 32 | | sdrgsubrg 20792 |
. . . . . . . 8
⊢ (𝑎 ∈ (SubDRing‘𝐸) → 𝑎 ∈ (SubRing‘𝐸)) |
| 33 | | subrgsubg 20577 |
. . . . . . . 8
⊢ (𝑎 ∈ (SubRing‘𝐸) → 𝑎 ∈ (SubGrp‘𝐸)) |
| 34 | 31, 32, 33 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → 𝑎 ∈ (SubGrp‘𝐸)) |
| 35 | 32 | ad3antlr 731 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈ (SubRing‘𝐸)) |
| 36 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → (𝐹 ∪ {𝐴}) ⊆ 𝑎) |
| 37 | 36 | unssad 4193 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝐹 ⊆ 𝑎) |
| 38 | 11 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝐺 ∈ 𝑈) |
| 39 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
| 40 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝐸
↾s 𝐹)) =
(Base‘(𝐸
↾s 𝐹)) |
| 41 | 14, 5, 3, 40 | coe1fvalcl 22214 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝐺)‘𝑘) ∈ (Base‘(𝐸 ↾s 𝐹))) |
| 42 | 38, 39, 41 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝐺)‘𝑘) ∈ (Base‘(𝐸 ↾s 𝐹))) |
| 43 | 2 | sdrgss 20794 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝐵) |
| 44 | 8, 43 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ⊆ 𝐵) |
| 45 | 4, 2 | ressbas2 17283 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ 𝐵 → 𝐹 = (Base‘(𝐸 ↾s 𝐹))) |
| 46 | 44, 45 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (Base‘(𝐸 ↾s 𝐹))) |
| 47 | 46 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝐹 = (Base‘(𝐸 ↾s 𝐹))) |
| 48 | 42, 47 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝐺)‘𝑘) ∈ 𝐹) |
| 49 | 37, 48 | sseldd 3984 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) →
((coe1‘𝐺)‘𝑘) ∈ 𝑎) |
| 50 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝑎 ∈ (SubDRing‘𝐸)) |
| 51 | 21 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ 𝐵) |
| 52 | 36 | unssbd 4194 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → {𝐴} ⊆ 𝑎) |
| 53 | | snssg 4783 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝑎 ↔ {𝐴} ⊆ 𝑎)) |
| 54 | 53 | biimpar 477 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝐵 ∧ {𝐴} ⊆ 𝑎) → 𝐴 ∈ 𝑎) |
| 55 | 51, 52, 54 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → 𝐴 ∈ 𝑎) |
| 56 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝐸) =
(mulGrp‘𝐸) |
| 57 | 56, 2 | mgpbas 20142 |
. . . . . . . . . . 11
⊢ 𝐵 =
(Base‘(mulGrp‘𝐸)) |
| 58 | 56, 12 | mgpplusg 20141 |
. . . . . . . . . . 11
⊢
(.r‘𝐸) = (+g‘(mulGrp‘𝐸)) |
| 59 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (SubDRing‘𝐸) → (mulGrp‘𝐸) ∈ V) |
| 60 | 2 | sdrgss 20794 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (SubDRing‘𝐸) → 𝑎 ⊆ 𝐵) |
| 61 | 12 | subrgmcl 20584 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (SubRing‘𝐸) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑎) |
| 62 | 32, 61 | syl3an1 1164 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ (SubDRing‘𝐸) ∧ 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎) → (𝑥(.r‘𝐸)𝑦) ∈ 𝑎) |
| 63 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘(mulGrp‘𝐸)) =
(0g‘(mulGrp‘𝐸)) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(1r‘𝐸) = (1r‘𝐸) |
| 65 | 56, 64 | ringidval 20180 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝐸) = (0g‘(mulGrp‘𝐸)) |
| 66 | 65 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢
(0g‘(mulGrp‘𝐸)) = (1r‘𝐸) |
| 67 | 66 | subrg1cl 20580 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (SubRing‘𝐸) →
(0g‘(mulGrp‘𝐸)) ∈ 𝑎) |
| 68 | 32, 67 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (SubDRing‘𝐸) →
(0g‘(mulGrp‘𝐸)) ∈ 𝑎) |
| 69 | 57, 13, 58, 59, 60, 62, 63, 68 | mulgnn0subcl 19105 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (SubDRing‘𝐸) ∧ 𝑘 ∈ ℕ0 ∧ 𝐴 ∈ 𝑎) → (𝑘(.g‘(mulGrp‘𝐸))𝐴) ∈ 𝑎) |
| 70 | 50, 39, 55, 69 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝐸))𝐴) ∈ 𝑎) |
| 71 | 12 | subrgmcl 20584 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (SubRing‘𝐸) ∧
((coe1‘𝐺)‘𝑘) ∈ 𝑎 ∧ (𝑘(.g‘(mulGrp‘𝐸))𝐴) ∈ 𝑎) → (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)) ∈ 𝑎) |
| 72 | 35, 49, 70, 71 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)) ∈ 𝑎) |
| 73 | 72 | fmpttd 7135 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))):ℕ0⟶𝑎) |
| 74 | 30 | mptexd 7244 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) ∈ V) |
| 75 | 73 | ffund 6740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)))) |
| 76 | | fvexd 6921 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (0g‘𝐸) ∈ V) |
| 77 | 4 | subrgring 20574 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ Ring) |
| 78 | 10, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Ring) |
| 79 | 78 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝐸 ↾s 𝐹) ∈ Ring) |
| 80 | 11 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → 𝐺 ∈ 𝑈) |
| 81 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘(𝐸 ↾s 𝐹)) = (0g‘(𝐸 ↾s 𝐹)) |
| 82 | 3, 5, 81 | mptcoe1fsupp 22217 |
. . . . . . . . . . 11
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝐺 ∈ 𝑈) → (𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) finSupp (0g‘(𝐸 ↾s 𝐹))) |
| 83 | 79, 80, 82 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) finSupp (0g‘(𝐸 ↾s 𝐹))) |
| 84 | | ringmnd 20240 |
. . . . . . . . . . . . 13
⊢ (𝐸 ∈ Ring → 𝐸 ∈ Mnd) |
| 85 | 26, 84 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ Mnd) |
| 86 | | subrgsubg 20577 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸)) |
| 87 | | subgsubm 19166 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ∈ (SubMnd‘𝐸)) |
| 88 | 25 | subm0cl 18824 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (SubMnd‘𝐸) →
(0g‘𝐸)
∈ 𝐹) |
| 89 | 10, 86, 87, 88 | 4syl 19 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝐸) ∈ 𝐹) |
| 90 | 4, 2, 25 | ress0g 18775 |
. . . . . . . . . . . 12
⊢ ((𝐸 ∈ Mnd ∧
(0g‘𝐸)
∈ 𝐹 ∧ 𝐹 ⊆ 𝐵) → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹))) |
| 91 | 85, 89, 44, 90 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹))) |
| 92 | 91 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (0g‘𝐸) = (0g‘(𝐸 ↾s 𝐹))) |
| 93 | 83, 92 | breqtrrd 5171 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) finSupp (0g‘𝐸)) |
| 94 | 93 | fsuppimpd 9409 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) supp (0g‘𝐸)) ∈ Fin) |
| 95 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → ((coe1‘𝐺)‘𝑘) = ((coe1‘𝐺)‘𝑖)) |
| 96 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑘(.g‘(mulGrp‘𝐸))𝐴) = (𝑖(.g‘(mulGrp‘𝐸))𝐴)) |
| 97 | 95, 96 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)) = (((coe1‘𝐺)‘𝑖)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴))) |
| 98 | 97 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) = (𝑖 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑖)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴))) |
| 99 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑘((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) |
| 100 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘)) = (𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) |
| 101 | 99, 42, 100 | fnmptd 6709 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) Fn ℕ0) |
| 102 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → 𝑖 ∈ ℕ0) |
| 103 | | fvexd 6921 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → ((coe1‘𝐺)‘𝑖) ∈ V) |
| 104 | 100, 95, 102, 103 | fvmptd3 7039 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘))‘𝑖) = ((coe1‘𝐺)‘𝑖)) |
| 105 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → ((𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) |
| 106 | 104, 105 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → ((coe1‘𝐺)‘𝑖) = (0g‘𝐸)) |
| 107 | 106 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → (((coe1‘𝐺)‘𝑖)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴)) = ((0g‘𝐸)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴))) |
| 108 | 26 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → 𝐸 ∈ Ring) |
| 109 | 56 | ringmgp 20236 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∈ Ring →
(mulGrp‘𝐸) ∈
Mnd) |
| 110 | 26, 109 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (mulGrp‘𝐸) ∈ Mnd) |
| 111 | 110 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → (mulGrp‘𝐸) ∈ Mnd) |
| 112 | 21 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → 𝐴 ∈ 𝐵) |
| 113 | 57, 13, 111, 102, 112 | mulgnn0cld 19113 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → (𝑖(.g‘(mulGrp‘𝐸))𝐴) ∈ 𝐵) |
| 114 | 2, 12, 25, 108, 113 | ringlzd 20292 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → ((0g‘𝐸)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴)) = (0g‘𝐸)) |
| 115 | 107, 114 | eqtrd 2777 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0) ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → (((coe1‘𝐺)‘𝑖)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴)) = (0g‘𝐸)) |
| 116 | 115 | 3impa 1110 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) ∧ 𝑖 ∈ ℕ0 ∧ ((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘))‘𝑖) = (0g‘𝐸)) → (((coe1‘𝐺)‘𝑖)(.r‘𝐸)(𝑖(.g‘(mulGrp‘𝐸))𝐴)) = (0g‘𝐸)) |
| 117 | 98, 30, 76, 101, 116 | suppss3 32735 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → ((𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) supp (0g‘𝐸)) ⊆ ((𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) supp (0g‘𝐸))) |
| 118 | | suppssfifsupp 9420 |
. . . . . . . 8
⊢ ((((𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) ∧ (0g‘𝐸) ∈ V) ∧ (((𝑘 ∈ ℕ0
↦ ((coe1‘𝐺)‘𝑘)) supp (0g‘𝐸)) ∈ Fin ∧ ((𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) supp (0g‘𝐸)) ⊆ ((𝑘 ∈ ℕ0 ↦
((coe1‘𝐺)‘𝑘)) supp (0g‘𝐸)))) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) finSupp (0g‘𝐸)) |
| 119 | 74, 75, 76, 94, 117, 118 | syl32anc 1380 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴))) finSupp (0g‘𝐸)) |
| 120 | 25, 28, 30, 34, 73, 119 | gsumsubgcl 19938 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → (𝐸 Σg (𝑘 ∈ ℕ0
↦ (((coe1‘𝐺)‘𝑘)(.r‘𝐸)(𝑘(.g‘(mulGrp‘𝐸))𝐴)))) ∈ 𝑎) |
| 121 | 24, 120 | eqeltrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) ∧ (𝐹 ∪ {𝐴}) ⊆ 𝑎) → ((𝑂‘𝐺)‘𝐴) ∈ 𝑎) |
| 122 | 121 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (SubDRing‘𝐸)) → ((𝐹 ∪ {𝐴}) ⊆ 𝑎 → ((𝑂‘𝐺)‘𝐴) ∈ 𝑎)) |
| 123 | 122 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ (SubDRing‘𝐸)((𝐹 ∪ {𝐴}) ⊆ 𝑎 → ((𝑂‘𝐺)‘𝐴) ∈ 𝑎)) |
| 124 | | fvex 6919 |
. . . 4
⊢ ((𝑂‘𝐺)‘𝐴) ∈ V |
| 125 | 124 | elintrab 4960 |
. . 3
⊢ (((𝑂‘𝐺)‘𝐴) ∈ ∩ {𝑎 ∈ (SubDRing‘𝐸) ∣ (𝐹 ∪ {𝐴}) ⊆ 𝑎} ↔ ∀𝑎 ∈ (SubDRing‘𝐸)((𝐹 ∪ {𝐴}) ⊆ 𝑎 → ((𝑂‘𝐺)‘𝐴) ∈ 𝑎)) |
| 126 | 123, 125 | sylibr 234 |
. 2
⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) ∈ ∩ {𝑎 ∈ (SubDRing‘𝐸) ∣ (𝐹 ∪ {𝐴}) ⊆ 𝑎}) |
| 127 | 6 | flddrngd 20741 |
. . 3
⊢ (𝜑 → 𝐸 ∈ DivRing) |
| 128 | 21 | snssd 4809 |
. . . 4
⊢ (𝜑 → {𝐴} ⊆ 𝐵) |
| 129 | 44, 128 | unssd 4192 |
. . 3
⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ 𝐵) |
| 130 | 2, 127, 129 | fldgenval 33314 |
. 2
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = ∩ {𝑎 ∈ (SubDRing‘𝐸) ∣ (𝐹 ∪ {𝐴}) ⊆ 𝑎}) |
| 131 | 126, 130 | eleqtrrd 2844 |
1
⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |