Metamath Proof Explorer

Theorem algextdeglem6

Description: Lemma for algextdeg . By r1pquslmic , the univariate polynomial remainder ring ( H "s P ) is isomorphic with the quotient ring Q . (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 ) )
algextdeglem.r 
|- R = ( rem1p ` K )
algextdeglem.h 
|- H = ( p e. U |-> ( p R ( M ` A ) ) )
Assertion algextdeglem6 
|- ( ph -> ( dim ` Q ) = ( dim ` ( H "s P ) ) )

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 algextdeglem.r 
 |-  R = ( rem1p ` K )
17 algextdeglem.h 
 |-  H = ( p e. U |-> ( p R ( M ` A ) ) )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem5 
 |-  ( ph -> Z = ( ( RSpan ` P ) ` { ( M ` A ) } ) )
19 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
20 6 19 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
21 1 subrgring 
 |-  ( F e. ( SubRing ` E ) -> K e. Ring )
22 20 21 syl 
 |-  ( ph -> K e. Ring )
23 9 ply1ring 
 |-  ( K e. Ring -> P e. Ring )
24 22 23 syl 
 |-  ( ph -> P e. Ring )
25 1 fveq2i 
 |-  ( Poly1 ` K ) = ( Poly1 ` ( E |`s F ) )
26 9 25 eqtri 
 |-  P = ( Poly1 ` ( E |`s F ) )
27 eqid 
 |-  ( Base ` E ) = ( Base ` E )
28 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
29 5 fldcrngd 
 |-  ( ph -> E e. CRing )
30 8 1 27 28 29 20 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
31 30 7 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
32 eqid 
 |-  { p e. dom O | ( ( O ` p ) ` A ) = ( 0g ` E ) } = { p e. dom O | ( ( O ` p ) ` A ) = ( 0g ` E ) }
33 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
34 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
35 8 26 27 5 6 31 28 32 33 34 4 minplycl 
 |-  ( ph -> ( M ` A ) e. ( Base ` P ) )
36 35 10 eleqtrrdi 
 |-  ( ph -> ( M ` A ) e. U )
37 eqid 
 |-  ( ||r ` P ) = ( ||r ` P )
38 10 33 37 rspsn 
 |-  ( ( P e. Ring /\ ( M ` A ) e. U ) -> ( ( RSpan ` P ) ` { ( M ` A ) } ) = { p | ( M ` A ) ( ||r ` P ) p } )
39 24 36 38 syl2anc 
 |-  ( ph -> ( ( RSpan ` P ) ` { ( M ` A ) } ) = { p | ( M ` A ) ( ||r ` P ) p } )
40 nfv 
 |-  F/ p ph
41 nfab1 
 |-  F/_ p { p | ( M ` A ) ( ||r ` P ) p }
42 nfrab1 
 |-  F/_ p { p e. U | ( H ` p ) = ( 0g ` P ) }
43 10 37 dvdsrcl2 
 |-  ( ( P e. Ring /\ ( M ` A ) ( ||r ` P ) p ) -> p e. U )
44 43 ex 
 |-  ( P e. Ring -> ( ( M ` A ) ( ||r ` P ) p -> p e. U ) )
45 44 pm4.71rd 
 |-  ( P e. Ring -> ( ( M ` A ) ( ||r ` P ) p <-> ( p e. U /\ ( M ` A ) ( ||r ` P ) p ) ) )
46 24 45 syl 
 |-  ( ph -> ( ( M ` A ) ( ||r ` P ) p <-> ( p e. U /\ ( M ` A ) ( ||r ` P ) p ) ) )
47 22 adantr 
 |-  ( ( ph /\ p e. U ) -> K e. Ring )
48 simpr 
 |-  ( ( ph /\ p e. U ) -> p e. U )
49 eqid 
 |-  ( 0g ` ( Poly1 ` E ) ) = ( 0g ` ( Poly1 ` E ) )
50 1 fveq2i 
 |-  ( Monic1p ` K ) = ( Monic1p ` ( E |`s F ) )
51 49 5 6 4 7 50 minplym1p 
 |-  ( ph -> ( M ` A ) e. ( Monic1p ` K ) )
52 eqid 
 |-  ( Unic1p ` K ) = ( Unic1p ` K )
53 eqid 
 |-  ( Monic1p ` K ) = ( Monic1p ` K )
54 52 53 mon1puc1p 
 |-  ( ( K e. Ring /\ ( M ` A ) e. ( Monic1p ` K ) ) -> ( M ` A ) e. ( Unic1p ` K ) )
55 22 51 54 syl2anc 
 |-  ( ph -> ( M ` A ) e. ( Unic1p ` K ) )
56 55 adantr 
 |-  ( ( ph /\ p e. U ) -> ( M ` A ) e. ( Unic1p ` K ) )
57 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
58 9 37 10 52 57 16 dvdsr1p 
 |-  ( ( K e. Ring /\ p e. U /\ ( M ` A ) e. ( Unic1p ` K ) ) -> ( ( M ` A ) ( ||r ` P ) p <-> ( p R ( M ` A ) ) = ( 0g ` P ) ) )
59 47 48 56 58 syl3anc 
 |-  ( ( ph /\ p e. U ) -> ( ( M ` A ) ( ||r ` P ) p <-> ( p R ( M ` A ) ) = ( 0g ` P ) ) )
60 ovexd 
 |-  ( ( ph /\ p e. U ) -> ( p R ( M ` A ) ) e. _V )
61 17 fvmpt2 
 |-  ( ( p e. U /\ ( p R ( M ` A ) ) e. _V ) -> ( H ` p ) = ( p R ( M ` A ) ) )
62 48 60 61 syl2anc 
 |-  ( ( ph /\ p e. U ) -> ( H ` p ) = ( p R ( M ` A ) ) )
63 62 eqeq1d 
 |-  ( ( ph /\ p e. U ) -> ( ( H ` p ) = ( 0g ` P ) <-> ( p R ( M ` A ) ) = ( 0g ` P ) ) )
64 59 63 bitr4d 
 |-  ( ( ph /\ p e. U ) -> ( ( M ` A ) ( ||r ` P ) p <-> ( H ` p ) = ( 0g ` P ) ) )
65 64 pm5.32da 
 |-  ( ph -> ( ( p e. U /\ ( M ` A ) ( ||r ` P ) p ) <-> ( p e. U /\ ( H ` p ) = ( 0g ` P ) ) ) )
66 46 65 bitrd 
 |-  ( ph -> ( ( M ` A ) ( ||r ` P ) p <-> ( p e. U /\ ( H ` p ) = ( 0g ` P ) ) ) )
67 abid 
 |-  ( p e. { p | ( M ` A ) ( ||r ` P ) p } <-> ( M ` A ) ( ||r ` P ) p )
68 rabid 
 |-  ( p e. { p e. U | ( H ` p ) = ( 0g ` P ) } <-> ( p e. U /\ ( H ` p ) = ( 0g ` P ) ) )
69 66 67 68 3bitr4g 
 |-  ( ph -> ( p e. { p | ( M ` A ) ( ||r ` P ) p } <-> p e. { p e. U | ( H ` p ) = ( 0g ` P ) } ) )
70 40 41 42 69 eqrd 
 |-  ( ph -> { p | ( M ` A ) ( ||r ` P ) p } = { p e. U | ( H ` p ) = ( 0g ` P ) } )
71 40 60 17 fnmptd 
 |-  ( ph -> H Fn U )
72 fniniseg2 
 |-  ( H Fn U -> ( `' H " { ( 0g ` P ) } ) = { p e. U | ( H ` p ) = ( 0g ` P ) } )
73 71 72 syl 
 |-  ( ph -> ( `' H " { ( 0g ` P ) } ) = { p e. U | ( H ` p ) = ( 0g ` P ) } )
74 70 73 eqtr4d 
 |-  ( ph -> { p | ( M ` A ) ( ||r ` P ) p } = ( `' H " { ( 0g ` P ) } ) )
75 18 39 74 3eqtrd 
 |-  ( ph -> Z = ( `' H " { ( 0g ` P ) } ) )
76 75 oveq2d 
 |-  ( ph -> ( P ~QG Z ) = ( P ~QG ( `' H " { ( 0g ` P ) } ) ) )
77 76 oveq2d 
 |-  ( ph -> ( P /s ( P ~QG Z ) ) = ( P /s ( P ~QG ( `' H " { ( 0g ` P ) } ) ) ) )
78 14 77 eqtrid 
 |-  ( ph -> Q = ( P /s ( P ~QG ( `' H " { ( 0g ` P ) } ) ) ) )
79 eqid 
 |-  ( `' H " { ( 0g ` P ) } ) = ( `' H " { ( 0g ` P ) } )
80 eqid 
 |-  ( P /s ( P ~QG ( `' H " { ( 0g ` P ) } ) ) ) = ( P /s ( P ~QG ( `' H " { ( 0g ` P ) } ) ) )
81 9 10 16 52 17 22 55 57 79 80 r1pquslmic 
 |-  ( ph -> ( P /s ( P ~QG ( `' H " { ( 0g ` P ) } ) ) ) ~=m ( H "s P ) )
82 78 81 eqbrtrd 
 |-  ( ph -> Q ~=m ( H "s P ) )
83 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem3 
 |-  ( ph -> Q e. LVec )
84 82 83 lmicdim 
 |-  ( ph -> ( dim ` Q ) = ( dim ` ( H "s P ) ) )