Metamath Proof Explorer

Theorem algextdeglem4

Description: Lemma for algextdeg . By lmhmqusker , the surjective module homomorphism G described in algextdeglem2 induces an isomorphism with the quotient space. Therefore, the dimension of that quotient space P / Z is the degree of the algebraic field extension. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses algextdeg.k ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
algextdeg.l ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
algextdeg.d ⊢ 𝐷 = ( deg1 ‘ 𝐸 )
algextdeg.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
algextdeg.f ⊢ ( 𝜑 → 𝐸 ∈ Field )
algextdeg.e ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
algextdeg.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
algextdeglem.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
algextdeglem.y ⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
algextdeglem.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
algextdeglem.g ⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
algextdeglem.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
algextdeglem.z ⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
algextdeglem.q ⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
algextdeglem.j ⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
Assertion algextdeglem4 ( 𝜑 → ( dim ‘ 𝑄 ) = ( 𝐿 [:] 𝐾 ) )

Proof

Step Hyp Ref Expression
1 algextdeg.k ⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
2 algextdeg.l ⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
3 algextdeg.d ⊢ 𝐷 = ( deg1 ‘ 𝐸 )
4 algextdeg.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
5 algextdeg.f ⊢ ( 𝜑 → 𝐸 ∈ Field )
6 algextdeg.e ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
7 algextdeg.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
8 algextdeglem.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
9 algextdeglem.y ⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
10 algextdeglem.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
11 algextdeglem.g ⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
12 algextdeglem.n ⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
13 algextdeglem.z ⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
14 algextdeglem.q ⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
15 algextdeglem.j ⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
16 issdrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
17 6 16 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
18 17 simp2d ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
19 subrgsubg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
20 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
21 20 subgss ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
22 18 19 21 3syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
23 1 20 ressbas2 ⊢ ( 𝐹 ⊆ ( Base ‘ 𝐸 ) → 𝐹 = ( Base ‘ 𝐾 ) )
24 22 23 syl ⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐾 ) )
25 24 fveq2d ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐿 ) ‘ ( Base ‘ 𝐾 ) ) )
26 25 fveq2d ⊢ ( 𝜑 → ( dim ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) = ( dim ‘ ( ( subringAlg ‘ 𝐿 ) ‘ ( Base ‘ 𝐾 ) ) ) )
27 eqid ⊢ ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem2 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
29 eqid ⊢ ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) = ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } )
30 eqid ⊢ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) )
31 1 fveq2i ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
32 9 31 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
33 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐸 ∈ Field )
34 6 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
35 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
36 5 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
37 8 1 20 35 36 18 irngssv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
38 37 7 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐴 ∈ ( Base ‘ 𝐸 ) )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
41 20 8 32 10 33 34 39 40 evls1fldgencl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
42 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑈 ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
43 11 rnmptss ⊢ ( ∀ 𝑝 ∈ 𝑈 ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) → ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
44 42 43 syl ⊢ ( 𝜑 → ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
45 5 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
46 8 32 20 10 36 18 38 11 evls1maprhm ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 RingHom 𝐸 ) )
47 rnrhmsubrg ⊢ ( 𝐺 ∈ ( 𝑃 RingHom 𝐸 ) → ran 𝐺 ∈ ( SubRing ‘ 𝐸 ) )
48 46 47 syl ⊢ ( 𝜑 → ran 𝐺 ∈ ( SubRing ‘ 𝐸 ) )
49 2 oveq1i ⊢ ( 𝐿 ↾s ran 𝐺 ) = ( ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ↾s ran 𝐺 )
50 ovex ⊢ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ V
51 ressabs ⊢ ( ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ V ∧ ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) → ( ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ↾s ran 𝐺 ) = ( 𝐸 ↾s ran 𝐺 ) )
52 50 44 51 sylancr ⊢ ( 𝜑 → ( ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ↾s ran 𝐺 ) = ( 𝐸 ↾s ran 𝐺 ) )
53 49 52 eqtrid ⊢ ( 𝜑 → ( 𝐿 ↾s ran 𝐺 ) = ( 𝐸 ↾s ran 𝐺 ) )
54 eqid ⊢ ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 )
55 38 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( Base ‘ 𝐸 ) )
56 22 55 unssd ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( Base ‘ 𝐸 ) )
57 20 45 56 fldgensdrg ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) )
58 issdrg ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∈ DivRing ) )
59 57 58 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∈ DivRing ) )
60 59 simp2d ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) )
61 2 resrhm2b ⊢ ( ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) → ( 𝐺 ∈ ( 𝑃 RingHom 𝐸 ) ↔ 𝐺 ∈ ( 𝑃 RingHom 𝐿 ) ) )
62 61 biimpa ⊢ ( ( ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ran 𝐺 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∧ 𝐺 ∈ ( 𝑃 RingHom 𝐸 ) ) → 𝐺 ∈ ( 𝑃 RingHom 𝐿 ) )
63 60 44 46 62 syl21anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 RingHom 𝐿 ) )
64 rhmghm ⊢ ( 𝐺 ∈ ( 𝑃 RingHom 𝐿 ) → 𝐺 ∈ ( 𝑃 GrpHom 𝐿 ) )
65 63 64 syl ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 GrpHom 𝐿 ) )
66 54 65 13 14 15 10 12 ghmquskerco ⊢ ( 𝜑 → 𝐺 = ( 𝐽 ∘ 𝑁 ) )
67 66 rneqd ⊢ ( 𝜑 → ran 𝐺 = ran ( 𝐽 ∘ 𝑁 ) )
68 14 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) ) )
69 10 a1i ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑃 ) )
70 ovexd ⊢ ( 𝜑 → ( 𝑃 ~QG 𝑍 ) ∈ V )
71 17 simp3d ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
72 32 71 ply1lvec ⊢ ( 𝜑 → 𝑃 ∈ LVec )
73 68 69 70 72 qusbas ⊢ ( 𝜑 → ( 𝑈 / ( 𝑃 ~QG 𝑍 ) ) = ( Base ‘ 𝑄 ) )
74 eqid ⊢ ( 𝑈 / ( 𝑃 ~QG 𝑍 ) ) = ( 𝑈 / ( 𝑃 ~QG 𝑍 ) )
75 54 ghmker ⊢ ( 𝐺 ∈ ( 𝑃 GrpHom 𝐿 ) → ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } ) ∈ ( NrmSGrp ‘ 𝑃 ) )
76 65 75 syl ⊢ ( 𝜑 → ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } ) ∈ ( NrmSGrp ‘ 𝑃 ) )
77 13 76 eqeltrid ⊢ ( 𝜑 → 𝑍 ∈ ( NrmSGrp ‘ 𝑃 ) )
78 10 74 12 77 qusrn ⊢ ( 𝜑 → ran 𝑁 = ( 𝑈 / ( 𝑃 ~QG 𝑍 ) ) )
79 eqid ⊢ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 )
80 8 32 20 10 36 18 38 11 79 evls1maplmhm ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) )
81 80 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑄 ) ) → 𝐺 ∈ V )
83 82 imaexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐺 “ 𝑝 ) ∈ V )
84 83 uniexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑄 ) ) → ∪ ( 𝐺 “ 𝑝 ) ∈ V )
85 15 84 dmmptd ⊢ ( 𝜑 → dom 𝐽 = ( Base ‘ 𝑄 ) )
86 73 78 85 3eqtr4rd ⊢ ( 𝜑 → dom 𝐽 = ran 𝑁 )
87 rncoeq ⊢ ( dom 𝐽 = ran 𝑁 → ran ( 𝐽 ∘ 𝑁 ) = ran 𝐽 )
88 86 87 syl ⊢ ( 𝜑 → ran ( 𝐽 ∘ 𝑁 ) = ran 𝐽 )
89 67 88 eqtrd ⊢ ( 𝜑 → ran 𝐺 = ran 𝐽 )
90 89 oveq2d ⊢ ( 𝜑 → ( 𝐿 ↾s ran 𝐺 ) = ( 𝐿 ↾s ran 𝐽 ) )
91 eqid ⊢ ( 𝐿 ↾s ran 𝐽 ) = ( 𝐿 ↾s ran 𝐽 )
92 1 subrgcrng ⊢ ( ( 𝐸 ∈ CRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ) → 𝐾 ∈ CRing )
93 36 18 92 syl2anc ⊢ ( 𝜑 → 𝐾 ∈ CRing )
94 9 ply1crng ⊢ ( 𝐾 ∈ CRing → 𝑃 ∈ CRing )
95 93 94 syl ⊢ ( 𝜑 → 𝑃 ∈ CRing )
96 54 63 13 14 15 95 rhmquskerlem ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 RingHom 𝐿 ) )
97 8 32 20 10 36 18 38 11 evls1maprnss ⊢ ( 𝜑 → 𝐹 ⊆ ran 𝐺 )
98 eqid ⊢ ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐸 )
99 1 98 subrg1 ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐾 ) )
100 18 99 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) = ( 1r ‘ 𝐾 ) )
101 98 subrg1cl ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → ( 1r ‘ 𝐸 ) ∈ 𝐹 )
102 18 101 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) ∈ 𝐹 )
103 100 102 eqeltrrd ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ∈ 𝐹 )
104 97 103 sseldd ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ∈ ran 𝐺 )
105 drngnzr ⊢ ( 𝐸 ∈ DivRing → 𝐸 ∈ NzRing )
106 98 35 nzrnz ⊢ ( 𝐸 ∈ NzRing → ( 1r ‘ 𝐸 ) ≠ ( 0g ‘ 𝐸 ) )
107 45 105 106 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝐸 ) ≠ ( 0g ‘ 𝐸 ) )
108 36 crnggrpd ⊢ ( 𝜑 → 𝐸 ∈ Grp )
109 108 grpmndd ⊢ ( 𝜑 → 𝐸 ∈ Mnd )
110 sdrgsubrg ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) )
111 subrgsubg ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubGrp ‘ 𝐸 ) )
112 57 110 111 3syl ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubGrp ‘ 𝐸 ) )
113 35 subg0cl ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubGrp ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
114 112 113 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
115 20 45 56 fldgenssv ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) )
116 2 20 35 ress0g ⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐿 ) )
117 109 114 115 116 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐿 ) )
118 107 100 117 3netr3d ⊢ ( 𝜑 → ( 1r ‘ 𝐾 ) ≠ ( 0g ‘ 𝐿 ) )
119 nelsn ⊢ ( ( 1r ‘ 𝐾 ) ≠ ( 0g ‘ 𝐿 ) → ¬ ( 1r ‘ 𝐾 ) ∈ { ( 0g ‘ 𝐿 ) } )
120 118 119 syl ⊢ ( 𝜑 → ¬ ( 1r ‘ 𝐾 ) ∈ { ( 0g ‘ 𝐿 ) } )
121 nelne1 ⊢ ( ( ( 1r ‘ 𝐾 ) ∈ ran 𝐺 ∧ ¬ ( 1r ‘ 𝐾 ) ∈ { ( 0g ‘ 𝐿 ) } ) → ran 𝐺 ≠ { ( 0g ‘ 𝐿 ) } )
122 104 120 121 syl2anc ⊢ ( 𝜑 → ran 𝐺 ≠ { ( 0g ‘ 𝐿 ) } )
123 89 122 eqnetrrd ⊢ ( 𝜑 → ran 𝐽 ≠ { ( 0g ‘ 𝐿 ) } )
124 eqid ⊢ ( oppr ‘ 𝑃 ) = ( oppr ‘ 𝑃 )
125 1 sdrgdrng ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐾 ∈ DivRing )
126 drngnzr ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ NzRing )
127 6 125 126 3syl ⊢ ( 𝜑 → 𝐾 ∈ NzRing )
128 9 ply1nz ⊢ ( 𝐾 ∈ NzRing → 𝑃 ∈ NzRing )
129 127 128 syl ⊢ ( 𝜑 → 𝑃 ∈ NzRing )
130 eqid ⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) }
131 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
132 1 fveq2i ⊢ ( idlGen1p ‘ 𝐾 ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
133 8 32 20 5 6 38 35 130 131 132 ply1annig1p ⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ 𝐾 ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) } ) )
134 117 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝐸 ) } = { ( 0g ‘ 𝐿 ) } )
135 134 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐺 “ { ( 0g ‘ 𝐸 ) } ) = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } ) )
136 13 135 eqtr4id ⊢ ( 𝜑 → 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐸 ) } ) )
137 10 mpteq1i ⊢ ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
138 11 137 eqtri ⊢ 𝐺 = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
139 8 32 20 36 18 38 35 130 138 ply1annidllem ⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = ( ◡ 𝐺 “ { ( 0g ‘ 𝐸 ) } ) )
140 136 139 eqtr4d ⊢ ( 𝜑 → 𝑍 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } )
141 eqid ⊢ ( 𝐸 minPoly 𝐹 ) = ( 𝐸 minPoly 𝐹 )
142 8 32 20 5 6 38 35 130 131 132 141 minplyval ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) = ( ( idlGen1p ‘ 𝐾 ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) )
143 142 sneqd ⊢ ( 𝜑 → { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } = { ( ( idlGen1p ‘ 𝐾 ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) } )
144 143 fveq2d ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ 𝐾 ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) } ) )
145 133 140 144 3eqtr4d ⊢ ( 𝜑 → 𝑍 = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) )
146 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
147 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
148 147 5 6 141 7 irngnminplynz ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) )
149 eqid ⊢ ( Poly1 ‘ 𝐸 ) = ( Poly1 ‘ 𝐸 )
150 149 1 9 10 18 147 ressply10g ⊢ ( 𝜑 → ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) = ( 0g ‘ 𝑃 ) )
151 148 150 neeqtrd ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) ≠ ( 0g ‘ 𝑃 ) )
152 8 32 20 5 6 38 141 146 151 minplyirred ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) ∈ ( Irred ‘ 𝑃 ) )
153 eqid ⊢ ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } )
154 fldsdrgfld ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ) → ( 𝐸 ↾s 𝐹 ) ∈ Field )
155 5 6 154 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Field )
156 1 155 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ Field )
157 9 ply1pid ⊢ ( 𝐾 ∈ Field → 𝑃 ∈ PID )
158 156 157 syl ⊢ ( 𝜑 → 𝑃 ∈ PID )
159 8 32 20 5 6 38 35 130 131 132 141 minplycl ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )
160 159 10 eleqtrrdi ⊢ ( 𝜑 → ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) ∈ 𝑈 )
161 95 crngringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
162 160 snssd ⊢ ( 𝜑 → { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ⊆ 𝑈 )
163 eqid ⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
164 131 10 163 rspcl ⊢ ( ( 𝑃 ∈ Ring ∧ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ⊆ 𝑈 ) → ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) ∈ ( LIdeal ‘ 𝑃 ) )
165 161 162 164 syl2anc ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) ∈ ( LIdeal ‘ 𝑃 ) )
166 10 131 146 153 158 160 151 165 mxidlirred ⊢ ( 𝜑 → ( ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) ∈ ( MaxIdeal ‘ 𝑃 ) ↔ ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) ∈ ( Irred ‘ 𝑃 ) ) )
167 152 166 mpbird ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑃 ) ‘ { ( ( 𝐸 minPoly 𝐹 ) ‘ 𝐴 ) } ) ∈ ( MaxIdeal ‘ 𝑃 ) )
168 145 167 eqeltrd ⊢ ( 𝜑 → 𝑍 ∈ ( MaxIdeal ‘ 𝑃 ) )
169 eqid ⊢ ( MaxIdeal ‘ 𝑃 ) = ( MaxIdeal ‘ 𝑃 )
170 169 124 crngmxidl ⊢ ( 𝑃 ∈ CRing → ( MaxIdeal ‘ 𝑃 ) = ( MaxIdeal ‘ ( oppr ‘ 𝑃 ) ) )
171 95 170 syl ⊢ ( 𝜑 → ( MaxIdeal ‘ 𝑃 ) = ( MaxIdeal ‘ ( oppr ‘ 𝑃 ) ) )
172 168 171 eleqtrd ⊢ ( 𝜑 → 𝑍 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑃 ) ) )
173 124 14 129 168 172 qsdrngi ⊢ ( 𝜑 → 𝑄 ∈ DivRing )
174 91 54 96 123 173 rndrhmcl ⊢ ( 𝜑 → ( 𝐿 ↾s ran 𝐽 ) ∈ DivRing )
175 90 174 eqeltrd ⊢ ( 𝜑 → ( 𝐿 ↾s ran 𝐺 ) ∈ DivRing )
176 53 175 eqeltrrd ⊢ ( 𝜑 → ( 𝐸 ↾s ran 𝐺 ) ∈ DivRing )
177 issdrg ⊢ ( ran 𝐺 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ ran 𝐺 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s ran 𝐺 ) ∈ DivRing ) )
178 45 48 176 177 syl3anbrc ⊢ ( 𝜑 → ran 𝐺 ∈ ( SubDRing ‘ 𝐸 ) )
179 fveq2 ⊢ ( 𝑝 = ( var1 ‘ 𝐾 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( var1 ‘ 𝐾 ) ) )
180 179 fveq1d ⊢ ( 𝑝 = ( var1 ‘ 𝐾 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ ( var1 ‘ 𝐾 ) ) ‘ 𝐴 ) )
181 180 eqeq2d ⊢ ( 𝑝 = ( var1 ‘ 𝐾 ) → ( 𝐴 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ↔ 𝐴 = ( ( 𝑂 ‘ ( var1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) )
182 1 71 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
183 182 drngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
184 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
185 184 9 10 vr1cl ⊢ ( 𝐾 ∈ Ring → ( var1 ‘ 𝐾 ) ∈ 𝑈 )
186 183 185 syl ⊢ ( 𝜑 → ( var1 ‘ 𝐾 ) ∈ 𝑈 )
187 8 184 1 20 36 18 evls1var ⊢ ( 𝜑 → ( 𝑂 ‘ ( var1 ‘ 𝐾 ) ) = ( I ↾ ( Base ‘ 𝐸 ) ) )
188 187 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( var1 ‘ 𝐾 ) ) ‘ 𝐴 ) = ( ( I ↾ ( Base ‘ 𝐸 ) ) ‘ 𝐴 ) )
189 fvresi ⊢ ( 𝐴 ∈ ( Base ‘ 𝐸 ) → ( ( I ↾ ( Base ‘ 𝐸 ) ) ‘ 𝐴 ) = 𝐴 )
190 38 189 syl ⊢ ( 𝜑 → ( ( I ↾ ( Base ‘ 𝐸 ) ) ‘ 𝐴 ) = 𝐴 )
191 188 190 eqtr2d ⊢ ( 𝜑 → 𝐴 = ( ( 𝑂 ‘ ( var1 ‘ 𝐾 ) ) ‘ 𝐴 ) )
192 181 186 191 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑈 𝐴 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
193 11 192 7 elrnmptd ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐺 )
194 193 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ran 𝐺 )
195 97 194 unssd ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ran 𝐺 )
196 20 45 178 195 fldgenssp ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ran 𝐺 )
197 44 196 eqssd ⊢ ( 𝜑 → ran 𝐺 = ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
198 2 20 ressbas2 ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) = ( Base ‘ 𝐿 ) )
199 115 198 syl ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) = ( Base ‘ 𝐿 ) )
200 eqidd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) )
201 20 45 56 fldgenssid ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
202 201 unssad ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
203 202 199 sseqtrd ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐿 ) )
204 200 203 srabase ⊢ ( 𝜑 → ( Base ‘ 𝐿 ) = ( Base ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
205 197 199 204 3eqtrd ⊢ ( 𝜑 → ran 𝐺 = ( Base ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
206 imaeq2 ⊢ ( 𝑞 = 𝑝 → ( 𝐺 “ 𝑞 ) = ( 𝐺 “ 𝑝 ) )
207 206 unieqd ⊢ ( 𝑞 = 𝑝 → ∪ ( 𝐺 “ 𝑞 ) = ∪ ( 𝐺 “ 𝑝 ) )
208 207 cbvmptv ⊢ ( 𝑞 ∈ ( Base ‘ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) ) ↦ ∪ ( 𝐺 “ 𝑞 ) ) = ( 𝑝 ∈ ( Base ‘ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
209 27 28 29 30 205 208 lmhmqusker ⊢ ( 𝜑 → ( 𝑞 ∈ ( Base ‘ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) ) ↦ ∪ ( 𝐺 “ 𝑞 ) ) ∈ ( ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) LMIso ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
210 eqidd ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) )
211 200 210 203 sralmod0 ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
212 211 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝐿 ) } = { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } )
213 212 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } ) = ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) )
214 13 213 eqtrid ⊢ ( 𝜑 → 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) )
215 214 oveq2d ⊢ ( 𝜑 → ( 𝑃 ~QG 𝑍 ) = ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) )
216 215 oveq2d ⊢ ( 𝜑 → ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) ) = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) )
217 14 216 eqtrid ⊢ ( 𝜑 → 𝑄 = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) )
218 217 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) ) )
219 218 mpteq1d ⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) ) = ( 𝑝 ∈ ( Base ‘ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) ) ↦ ∪ ( 𝐺 “ 𝑝 ) ) )
220 219 15 208 3eqtr4g ⊢ ( 𝜑 → 𝐽 = ( 𝑞 ∈ ( Base ‘ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) ) ↦ ∪ ( 𝐺 “ 𝑞 ) ) )
221 217 oveq1d ⊢ ( 𝜑 → ( 𝑄 LMIso ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) = ( ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ) ) LMIso ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
222 209 220 221 3eltr4d ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 LMIso ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
223 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem3 ⊢ ( 𝜑 → 𝑄 ∈ LVec )
224 222 223 lmimdim ⊢ ( 𝜑 → ( dim ‘ 𝑄 ) = ( dim ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
225 20 5 56 fldgenfld ⊢ ( 𝜑 → ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ∈ Field )
226 2 225 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ Field )
227 1 2 3 4 5 6 7 algextdeglem1 ⊢ ( 𝜑 → ( 𝐿 ↾s 𝐹 ) = 𝐾 )
228 24 oveq2d ⊢ ( 𝜑 → ( 𝐿 ↾s 𝐹 ) = ( 𝐿 ↾s ( Base ‘ 𝐾 ) ) )
229 227 228 eqtr3d ⊢ ( 𝜑 → 𝐾 = ( 𝐿 ↾s ( Base ‘ 𝐾 ) ) )
230 2 subsubrg ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) → ( 𝐹 ∈ ( SubRing ‘ 𝐿 ) ↔ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) )
231 230 biimpar ⊢ ( ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ) → 𝐹 ∈ ( SubRing ‘ 𝐿 ) )
232 60 18 202 231 syl12anc ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐿 ) )
233 24 232 eqeltrrd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐿 ) )
234 brfldext ⊢ ( ( 𝐿 ∈ Field ∧ 𝐾 ∈ Field ) → ( 𝐿 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐿 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐿 ) ) ) )
235 234 biimpar ⊢ ( ( ( 𝐿 ∈ Field ∧ 𝐾 ∈ Field ) ∧ ( 𝐾 = ( 𝐿 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐿 ) ) ) → 𝐿 /FldExt 𝐾 )
236 226 156 229 233 235 syl22anc ⊢ ( 𝜑 → 𝐿 /FldExt 𝐾 )
237 extdgval ⊢ ( 𝐿 /FldExt 𝐾 → ( 𝐿 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ 𝐿 ) ‘ ( Base ‘ 𝐾 ) ) ) )
238 236 237 syl ⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ 𝐿 ) ‘ ( Base ‘ 𝐾 ) ) ) )
239 26 224 238 3eqtr4d ⊢ ( 𝜑 → ( dim ‘ 𝑄 ) = ( 𝐿 [:] 𝐾 ) )