This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- K = ( E |`s F )
algextdeg.l 
|- L = ( E |`s ( E fldGen ( F u. { A } ) ) )
algextdeg.d 
|- D = ( deg1 ` E )
algextdeg.m 
|- M = ( E minPoly F )
algextdeg.f 
|- ( ph -> E e. Field )
algextdeg.e 
|- ( ph -> F e. ( SubDRing ` E ) )
algextdeg.a 
|- ( ph -> A e. ( E IntgRing F ) )
algextdeglem.o 
|- O = ( E evalSub1 F )
algextdeglem.y 
|- P = ( Poly1 ` K )
algextdeglem.u 
|- U = ( Base ` P )
algextdeglem.g 
|- G = ( p e. U |-> ( ( O ` p ) ` A ) )
algextdeglem.n 
|- N = ( x e. U |-> [ x ] ( P ~QG Z ) )
algextdeglem.z 
|- Z = ( `' G " { ( 0g ` L ) } )
algextdeglem.q 
|- Q = ( P /s ( P ~QG Z ) )
algextdeglem.j 
|- J = ( p e. ( Base ` Q ) |-> U. ( G " p ) )
Assertion algextdeglem4 
|- ( ph -> ( dim ` Q ) = ( L [:] K ) )

Proof

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