| Step | Hyp | Ref
| Expression |
| 1 | | algextdeg.e |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
| 2 | | issdrg 20789 |
. . . . . . . 8
⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) |
| 3 | 1, 2 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) |
| 4 | 3 | simp2d 1144 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
| 5 | | subrgsubg 20577 |
. . . . . 6
⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸)) |
| 6 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 7 | 6 | subgss 19145 |
. . . . . 6
⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸)) |
| 8 | 4, 5, 7 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸)) |
| 9 | | algextdeg.k |
. . . . . 6
⊢ 𝐾 = (𝐸 ↾s 𝐹) |
| 10 | 9, 6 | ressbas2 17283 |
. . . . 5
⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾)) |
| 11 | 8, 10 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 = (Base‘𝐾)) |
| 12 | 11 | fveq2d 6910 |
. . 3
⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾))) |
| 13 | 12 | fveq2d 6910 |
. 2
⊢ (𝜑 → (dim‘((subringAlg
‘𝐿)‘𝐹)) = (dim‘((subringAlg
‘𝐿)‘(Base‘𝐾)))) |
| 14 | | eqid 2737 |
. . . . 5
⊢
(0g‘((subringAlg ‘𝐿)‘𝐹)) = (0g‘((subringAlg
‘𝐿)‘𝐹)) |
| 15 | | algextdeg.l |
. . . . . 6
⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 16 | | algextdeg.d |
. . . . . 6
⊢ 𝐷 = (deg1‘𝐸) |
| 17 | | algextdeg.m |
. . . . . 6
⊢ 𝑀 = (𝐸 minPoly 𝐹) |
| 18 | | algextdeg.f |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ Field) |
| 19 | | algextdeg.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) |
| 20 | | algextdeglem.o |
. . . . . 6
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
| 21 | | algextdeglem.y |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝐾) |
| 22 | | algextdeglem.u |
. . . . . 6
⊢ 𝑈 = (Base‘𝑃) |
| 23 | | algextdeglem.g |
. . . . . 6
⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) |
| 24 | | algextdeglem.n |
. . . . . 6
⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) |
| 25 | | algextdeglem.z |
. . . . . 6
⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) |
| 26 | | algextdeglem.q |
. . . . . 6
⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) |
| 27 | | algextdeglem.j |
. . . . . 6
⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪
(𝐺 “ 𝑝)) |
| 28 | 9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27 | algextdeglem2 33759 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹))) |
| 29 | | eqid 2737 |
. . . . 5
⊢ (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}) = (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}) |
| 30 | | eqid 2737 |
. . . . 5
⊢ (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}))) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}))) |
| 31 | 9 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹)) |
| 32 | 21, 31 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝑃 =
(Poly1‘(𝐸
↾s 𝐹)) |
| 33 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field) |
| 34 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸)) |
| 35 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(0g‘𝐸) = (0g‘𝐸) |
| 36 | 18 | fldcrngd 20742 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ CRing) |
| 37 | 20, 9, 6, 35, 36, 4 | irngssv 33738 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸)) |
| 38 | 37, 19 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸)) |
| 39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸)) |
| 40 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈) |
| 41 | 6, 20, 32, 22, 33, 34, 39, 40 | evls1fldgencl 33720 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 42 | 41 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 43 | 23 | rnmptss 7143 |
. . . . . . . 8
⊢
(∀𝑝 ∈
𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 45 | 18 | flddrngd 20741 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ DivRing) |
| 46 | 20, 32, 6, 22, 36, 4, 38, 23 | evls1maprhm 22380 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸)) |
| 47 | | rnrhmsubrg 20605 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸)) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸)) |
| 49 | 15 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ (𝐿 ↾s ran 𝐺) = ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) |
| 50 | | ovex 7464 |
. . . . . . . . . . . 12
⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V |
| 51 | | ressabs 17294 |
. . . . . . . . . . . 12
⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺)) |
| 52 | 50, 44, 51 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺)) |
| 53 | 49, 52 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺)) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐿) = (0g‘𝐿) |
| 55 | 38 | snssd 4809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸)) |
| 56 | 8, 55 | unssd 4192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸)) |
| 57 | 6, 45, 56 | fldgensdrg 33316 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸)) |
| 58 | | issdrg 20789 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing)) |
| 59 | 57, 58 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing)) |
| 60 | 59 | simp2d 1144 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸)) |
| 61 | 15 | resrhm2b 20602 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿))) |
| 62 | 61 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐸)) → 𝐺 ∈ (𝑃 RingHom 𝐿)) |
| 63 | 60, 44, 46, 62 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿)) |
| 64 | | rhmghm 20484 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿)) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿)) |
| 66 | 54, 65, 25, 26, 27, 22, 24 | ghmquskerco 19302 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁)) |
| 67 | 66 | rneqd 5949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐺 = ran (𝐽 ∘ 𝑁)) |
| 68 | 26 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))) |
| 69 | 22 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 = (Base‘𝑃)) |
| 70 | | ovexd 7466 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 ~QG 𝑍) ∈ V) |
| 71 | 3 | simp3d 1145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing) |
| 72 | 32, 71 | ply1lvec 33585 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ LVec) |
| 73 | 68, 69, 70, 72 | qusbas 17590 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 / (𝑃 ~QG 𝑍)) = (Base‘𝑄)) |
| 74 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 / (𝑃 ~QG 𝑍)) = (𝑈 / (𝑃 ~QG 𝑍)) |
| 75 | 54 | ghmker 19260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃)) |
| 76 | 65, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃)) |
| 77 | 25, 76 | eqeltrid 2845 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃)) |
| 78 | 22, 74, 24, 77 | qusrn 33437 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~QG 𝑍))) |
| 79 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹) |
| 80 | 20, 32, 6, 22, 36, 4, 38, 23, 79 | evls1maplmhm 22381 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹))) |
| 81 | 80 | elexd 3504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺 ∈ V) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V) |
| 83 | 82 | imaexd 7938 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V) |
| 84 | 83 | uniexd 7762 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪
(𝐺 “ 𝑝) ∈ V) |
| 85 | 27, 84 | dmmptd 6713 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐽 = (Base‘𝑄)) |
| 86 | 73, 78, 85 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝐽 = ran 𝑁) |
| 87 | | rncoeq 5990 |
. . . . . . . . . . . . . 14
⊢ (dom
𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽) |
| 88 | 86, 87 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽) |
| 89 | 67, 88 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐺 = ran 𝐽) |
| 90 | 89 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐿 ↾s ran 𝐽)) |
| 91 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝐿 ↾s ran 𝐽) = (𝐿 ↾s ran 𝐽) |
| 92 | 9 | subrgcrng 20575 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing) |
| 93 | 36, 4, 92 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ CRing) |
| 94 | 21 | ply1crng 22200 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ CRing) |
| 96 | 54, 63, 25, 26, 27, 95 | rhmquskerlem 33453 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿)) |
| 97 | 20, 32, 6, 22, 36, 4, 38, 23 | evls1maprnss 22382 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ⊆ ran 𝐺) |
| 98 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(1r‘𝐸) = (1r‘𝐸) |
| 99 | 9, 98 | subrg1 20582 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (SubRing‘𝐸) →
(1r‘𝐸) =
(1r‘𝐾)) |
| 100 | 4, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾)) |
| 101 | 98 | subrg1cl 20580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (SubRing‘𝐸) →
(1r‘𝐸)
∈ 𝐹) |
| 102 | 4, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹) |
| 103 | 100, 102 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1r‘𝐾) ∈ 𝐹) |
| 104 | 97, 103 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1r‘𝐾) ∈ ran 𝐺) |
| 105 | | drngnzr 20748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing) |
| 106 | 98, 35 | nzrnz 20515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 ∈ NzRing →
(1r‘𝐸)
≠ (0g‘𝐸)) |
| 107 | 45, 105, 106 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1r‘𝐸) ≠
(0g‘𝐸)) |
| 108 | 36 | crnggrpd 20244 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ∈ Grp) |
| 109 | 108 | grpmndd 18964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ∈ Mnd) |
| 110 | | sdrgsubrg 20792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸)) |
| 111 | | subrgsubg 20577 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸)) |
| 112 | 57, 110, 111 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸)) |
| 113 | 35 | subg0cl 19152 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 115 | 6, 45, 56 | fldgenssv 33317 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) |
| 116 | 15, 6, 35 | ress0g 18775 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 ∈ Mnd ∧
(0g‘𝐸)
∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐿)) |
| 117 | 109, 114,
115, 116 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐿)) |
| 118 | 107, 100,
117 | 3netr3d 3017 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1r‘𝐾) ≠
(0g‘𝐿)) |
| 119 | | nelsn 4666 |
. . . . . . . . . . . . . . 15
⊢
((1r‘𝐾) ≠ (0g‘𝐿) → ¬
(1r‘𝐾)
∈ {(0g‘𝐿)}) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬
(1r‘𝐾)
∈ {(0g‘𝐿)}) |
| 121 | | nelne1 3039 |
. . . . . . . . . . . . . 14
⊢
(((1r‘𝐾) ∈ ran 𝐺 ∧ ¬ (1r‘𝐾) ∈
{(0g‘𝐿)})
→ ran 𝐺 ≠
{(0g‘𝐿)}) |
| 122 | 104, 120,
121 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐺 ≠ {(0g‘𝐿)}) |
| 123 | 89, 122 | eqnetrrd 3009 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐽 ≠ {(0g‘𝐿)}) |
| 124 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(oppr‘𝑃) = (oppr‘𝑃) |
| 125 | 9 | sdrgdrng 20791 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing) |
| 126 | | drngnzr 20748 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing) |
| 127 | 1, 125, 126 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ NzRing) |
| 128 | 21 | ply1nz 26161 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing) |
| 129 | 127, 128 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ NzRing) |
| 130 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} |
| 131 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(RSpan‘𝑃) =
(RSpan‘𝑃) |
| 132 | 9 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(idlGen1p‘𝐾) = (idlGen1p‘(𝐸 ↾s 𝐹)) |
| 133 | 20, 32, 6, 18, 1, 38, 35, 130, 131, 132 | ply1annig1p 33747 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})})) |
| 134 | 117 | sneqd 4638 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
{(0g‘𝐸)} =
{(0g‘𝐿)}) |
| 135 | 134 | imaeq2d 6078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐸)}) = (◡𝐺 “ {(0g‘𝐿)})) |
| 136 | 25, 135 | eqtr4id 2796 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘𝐸)})) |
| 137 | 22 | mpteq1i 5238 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴)) |
| 138 | 23, 137 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴)) |
| 139 | 20, 32, 6, 36, 4, 38, 35, 130, 138 | ply1annidllem 33744 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = (◡𝐺 “ {(0g‘𝐸)})) |
| 140 | 136, 139 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) |
| 141 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹) |
| 142 | 20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141 | minplyval 33748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})) |
| 143 | 142 | sneqd 4638 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}) |
| 144 | 143 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen1p‘𝐾)‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})})) |
| 145 | 133, 140,
144 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})) |
| 146 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 147 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘(Poly1‘𝐸)) =
(0g‘(Poly1‘𝐸)) |
| 148 | 147, 18, 1, 141, 19 | irngnminplynz 33755 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠
(0g‘(Poly1‘𝐸))) |
| 149 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(Poly1‘𝐸) = (Poly1‘𝐸) |
| 150 | 149, 9, 21, 22, 4, 147 | ressply10g 33592 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(0g‘(Poly1‘𝐸)) = (0g‘𝑃)) |
| 151 | 148, 150 | neeqtrd 3010 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘𝑃)) |
| 152 | 20, 32, 6, 18, 1, 38, 141, 146, 151 | minplyirred 33754 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)) |
| 153 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) |
| 154 | | fldsdrgfld 20799 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field) |
| 155 | 18, 1, 154 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field) |
| 156 | 9, 155 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ Field) |
| 157 | 21 | ply1pid 26222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ Field → 𝑃 ∈ PID) |
| 158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ PID) |
| 159 | 20, 32, 6, 18, 1, 38, 35, 130, 131, 132, 141 | minplycl 33749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃)) |
| 160 | 159, 22 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈) |
| 161 | 95 | crngringd 20243 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ Ring) |
| 162 | 160 | snssd 4809 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) |
| 163 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(LIdeal‘𝑃) =
(LIdeal‘𝑃) |
| 164 | 131, 22, 163 | rspcl 21245 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃)) |
| 165 | 161, 162,
164 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃)) |
| 166 | 22, 131, 146, 153, 158, 160, 151, 165 | mxidlirred 33500 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))) |
| 167 | 152, 166 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃)) |
| 168 | 145, 167 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃)) |
| 169 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(MaxIdeal‘𝑃) =
(MaxIdeal‘𝑃) |
| 170 | 169, 124 | crngmxidl 33497 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ CRing →
(MaxIdeal‘𝑃) =
(MaxIdeal‘(oppr‘𝑃))) |
| 171 | 95, 170 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (MaxIdeal‘𝑃) =
(MaxIdeal‘(oppr‘𝑃))) |
| 172 | 168, 171 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 ∈
(MaxIdeal‘(oppr‘𝑃))) |
| 173 | 124, 26, 129, 168, 172 | qsdrngi 33523 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ DivRing) |
| 174 | 91, 54, 96, 123, 173 | rndrhmcl 33299 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 ↾s ran 𝐽) ∈ DivRing) |
| 175 | 90, 174 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 ↾s ran 𝐺) ∈ DivRing) |
| 176 | 53, 175 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ↾s ran 𝐺) ∈ DivRing) |
| 177 | | issdrg 20789 |
. . . . . . . . 9
⊢ (ran
𝐺 ∈
(SubDRing‘𝐸) ↔
(𝐸 ∈ DivRing ∧ ran
𝐺 ∈
(SubRing‘𝐸) ∧
(𝐸 ↾s ran
𝐺) ∈
DivRing)) |
| 178 | 45, 48, 176, 177 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸)) |
| 179 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = (var1‘𝐾) → (𝑂‘𝑝) = (𝑂‘(var1‘𝐾))) |
| 180 | 179 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (var1‘𝐾) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var1‘𝐾))‘𝐴)) |
| 181 | 180 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑝 = (var1‘𝐾) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴))) |
| 182 | 9, 71 | eqeltrid 2845 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ DivRing) |
| 183 | 182 | drngringd 20737 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Ring) |
| 184 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(var1‘𝐾) = (var1‘𝐾) |
| 185 | 184, 21, 22 | vr1cl 22219 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Ring →
(var1‘𝐾)
∈ 𝑈) |
| 186 | 183, 185 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(var1‘𝐾)
∈ 𝑈) |
| 187 | 20, 184, 9, 6, 36, 4 | evls1var 22342 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘(var1‘𝐾)) = ( I ↾
(Base‘𝐸))) |
| 188 | 187 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑂‘(var1‘𝐾))‘𝐴) = (( I ↾ (Base‘𝐸))‘𝐴)) |
| 189 | | fvresi 7193 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (Base‘𝐸) → (( I ↾
(Base‘𝐸))‘𝐴) = 𝐴) |
| 190 | 38, 189 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (( I ↾
(Base‘𝐸))‘𝐴) = 𝐴) |
| 191 | 188, 190 | eqtr2d 2778 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 = ((𝑂‘(var1‘𝐾))‘𝐴)) |
| 192 | 181, 186,
191 | rspcedvdw 3625 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴)) |
| 193 | 23, 192, 19 | elrnmptd 5974 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ran 𝐺) |
| 194 | 193 | snssd 4809 |
. . . . . . . . 9
⊢ (𝜑 → {𝐴} ⊆ ran 𝐺) |
| 195 | 97, 194 | unssd 4192 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺) |
| 196 | 6, 45, 178, 195 | fldgenssp 33320 |
. . . . . . 7
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺) |
| 197 | 44, 196 | eqssd 4001 |
. . . . . 6
⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 198 | 15, 6 | ressbas2 17283 |
. . . . . . 7
⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿)) |
| 199 | 115, 198 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿)) |
| 200 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹)) |
| 201 | 6, 45, 56 | fldgenssid 33315 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 202 | 201 | unssad 4193 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) |
| 203 | 202, 199 | sseqtrd 4020 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿)) |
| 204 | 200, 203 | srabase 21177 |
. . . . . 6
⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg
‘𝐿)‘𝐹))) |
| 205 | 197, 199,
204 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹))) |
| 206 | | imaeq2 6074 |
. . . . . . 7
⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝)) |
| 207 | 206 | unieqd 4920 |
. . . . . 6
⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝)) |
| 208 | 207 | cbvmptv 5255 |
. . . . 5
⊢ (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺
“ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺
“ 𝑝)) |
| 209 | 14, 28, 29, 30, 205, 208 | lmhmqusker 33445 |
. . . 4
⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺
“ 𝑞)) ∈ ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}))) LMIso ((subringAlg
‘𝐿)‘𝐹))) |
| 210 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐿)) |
| 211 | 200, 210,
203 | sralmod0 21195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐿) =
(0g‘((subringAlg ‘𝐿)‘𝐹))) |
| 212 | 211 | sneqd 4638 |
. . . . . . . . . . . 12
⊢ (𝜑 →
{(0g‘𝐿)} =
{(0g‘((subringAlg ‘𝐿)‘𝐹))}) |
| 213 | 212 | imaeq2d 6078 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) = (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})) |
| 214 | 25, 213 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})) |
| 215 | 214 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 ~QG 𝑍) = (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}))) |
| 216 | 215 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 /s (𝑃 ~QG 𝑍)) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) |
| 217 | 26, 216 | eqtrid 2789 |
. . . . . . 7
⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) |
| 218 | 217 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}))))) |
| 219 | 218 | mpteq1d 5237 |
. . . . 5
⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪
(𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺
“ 𝑝))) |
| 220 | 219, 27, 208 | 3eqtr4g 2802 |
. . . 4
⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺
“ 𝑞))) |
| 221 | 217 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg
‘𝐿)‘𝐹))}))) LMIso ((subringAlg
‘𝐿)‘𝐹))) |
| 222 | 209, 220,
221 | 3eltr4d 2856 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹))) |
| 223 | 9, 15, 16, 17, 18, 1, 19, 20, 21, 22, 23, 24, 25, 26, 27 | algextdeglem3 33760 |
. . 3
⊢ (𝜑 → 𝑄 ∈ LVec) |
| 224 | 222, 223 | lmimdim 33654 |
. 2
⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg
‘𝐿)‘𝐹))) |
| 225 | 6, 18, 56 | fldgenfld 33322 |
. . . . 5
⊢ (𝜑 → (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field) |
| 226 | 15, 225 | eqeltrid 2845 |
. . . 4
⊢ (𝜑 → 𝐿 ∈ Field) |
| 227 | 9, 15, 16, 17, 18, 1, 19 | algextdeglem1 33758 |
. . . . 5
⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾) |
| 228 | 11 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐿 ↾s 𝐹) = (𝐿 ↾s (Base‘𝐾))) |
| 229 | 227, 228 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → 𝐾 = (𝐿 ↾s (Base‘𝐾))) |
| 230 | 15 | subsubrg 20598 |
. . . . . . 7
⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))))) |
| 231 | 230 | biimpar 477 |
. . . . . 6
⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿)) |
| 232 | 60, 4, 202, 231 | syl12anc 837 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿)) |
| 233 | 11, 232 | eqeltrrd 2842 |
. . . 4
⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿)) |
| 234 | | brfldext 33698 |
. . . . 5
⊢ ((𝐿 ∈ Field ∧ 𝐾 ∈ Field) → (𝐿/FldExt𝐾 ↔ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿)))) |
| 235 | 234 | biimpar 477 |
. . . 4
⊢ (((𝐿 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))) → 𝐿/FldExt𝐾) |
| 236 | 226, 156,
229, 233, 235 | syl22anc 839 |
. . 3
⊢ (𝜑 → 𝐿/FldExt𝐾) |
| 237 | | extdgval 33705 |
. . 3
⊢ (𝐿/FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾)))) |
| 238 | 236, 237 | syl 17 |
. 2
⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾)))) |
| 239 | 13, 224, 238 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾)) |