Metamath Proof Explorer

Theorem algextdeglem3

Description: Lemma for algextdeg . The quotient P / Z of the vector space P of polynomials by the subspace Z of polynomials annihilating A is itself a vector space. (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 algextdeglem3 
|- ( ph -> Q e. LVec )

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 1 fveq2i 
 |-  ( Poly1 ` K ) = ( Poly1 ` ( E |`s F ) )
17 9 16 eqtri 
 |-  P = ( Poly1 ` ( E |`s F ) )
18 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
19 6 18 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
20 19 simp3d 
 |-  ( ph -> ( E |`s F ) e. DivRing )
21 17 20 ply1lvec 
 |-  ( ph -> P e. LVec )
22 eqidd 
 |-  ( ph -> ( ( subringAlg ` L ) ` F ) = ( ( subringAlg ` L ) ` F ) )
23 eqidd 
 |-  ( ph -> ( 0g ` L ) = ( 0g ` L ) )
24 eqid 
 |-  ( Base ` E ) = ( Base ` E )
25 5 flddrngd 
 |-  ( ph -> E e. DivRing )
26 19 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
27 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
28 24 subgss 
 |-  ( F e. ( SubGrp ` E ) -> F C_ ( Base ` E ) )
29 26 27 28 3syl 
 |-  ( ph -> F C_ ( Base ` E ) )
30 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
31 5 fldcrngd 
 |-  ( ph -> E e. CRing )
32 8 1 24 30 31 26 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
33 32 7 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
34 33 snssd 
 |-  ( ph -> { A } C_ ( Base ` E ) )
35 29 34 unssd 
 |-  ( ph -> ( F u. { A } ) C_ ( Base ` E ) )
36 24 25 35 fldgenssid 
 |-  ( ph -> ( F u. { A } ) C_ ( E fldGen ( F u. { A } ) ) )
37 36 unssad 
 |-  ( ph -> F C_ ( E fldGen ( F u. { A } ) ) )
38 24 25 35 fldgenssv 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) C_ ( Base ` E ) )
39 2 24 ressbas2 
 |-  ( ( E fldGen ( F u. { A } ) ) C_ ( Base ` E ) -> ( E fldGen ( F u. { A } ) ) = ( Base ` L ) )
40 38 39 syl 
 |-  ( ph -> ( E fldGen ( F u. { A } ) ) = ( Base ` L ) )
41 37 40 sseqtrd 
 |-  ( ph -> F C_ ( Base ` L ) )
42 22 23 41 sralmod0 
 |-  ( ph -> ( 0g ` L ) = ( 0g ` ( ( subringAlg ` L ) ` F ) ) )
43 42 sneqd 
 |-  ( ph -> { ( 0g ` L ) } = { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } )
44 43 imaeq2d 
 |-  ( ph -> ( `' G " { ( 0g ` L ) } ) = ( `' G " { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } ) )
45 13 44 eqtrid 
 |-  ( ph -> Z = ( `' G " { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } ) )
46 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem2 
 |-  ( ph -> G e. ( P LMHom ( ( subringAlg ` L ) ` F ) ) )
47 eqid 
 |-  ( `' G " { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } ) = ( `' G " { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } )
48 eqid 
 |-  ( 0g ` ( ( subringAlg ` L ) ` F ) ) = ( 0g ` ( ( subringAlg ` L ) ` F ) )
49 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
50 47 48 49 lmhmkerlss 
 |-  ( G e. ( P LMHom ( ( subringAlg ` L ) ` F ) ) -> ( `' G " { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } ) e. ( LSubSp ` P ) )
51 46 50 syl 
 |-  ( ph -> ( `' G " { ( 0g ` ( ( subringAlg ` L ) ` F ) ) } ) e. ( LSubSp ` P ) )
52 45 51 eqeltrd 
 |-  ( ph -> Z e. ( LSubSp ` P ) )
53 14 21 52 quslvec 
 |-  ( ph -> Q e. LVec )