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

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 ⊢ 𝐾 = ( 𝐸 ↾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 ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
algextdeglem.r ⊢ 𝑅 = ( rem1p ‘ 𝐾 )
algextdeglem.h ⊢ 𝐻 = ( 𝑝 ∈ 𝑈 ↦ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
Assertion algextdeglem6 ( 𝜑 → ( dim ‘ 𝑄 ) = ( dim ‘ ( 𝐻 “s 𝑃 ) ) )

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 algextdeglem.r ⊢ 𝑅 = ( rem1p ‘ 𝐾 )
17 algextdeglem.h ⊢ 𝐻 = ( 𝑝 ∈ 𝑈 ↦ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem5 ⊢ ( 𝜑 → 𝑍 = ( ( RSpan ‘ 𝑃 ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) )
19 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
20 6 19 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
21 1 subrgring ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐾 ∈ Ring )
22 20 21 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
23 9 ply1ring ⊢ ( 𝐾 ∈ Ring → 𝑃 ∈ Ring )
24 22 23 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
25 1 fveq2i ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
26 9 25 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
27 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
28 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
29 5 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
30 8 1 27 28 29 20 irngssv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
31 30 7 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
32 eqid ⊢ { 𝑝 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = { 𝑝 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) }
33 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
34 eqid ⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
35 8 26 27 5 6 31 28 32 33 34 4 minplycl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )
36 35 10 eleqtrrdi ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 )
37 eqid ⊢ ( ∥r ‘ 𝑃 ) = ( ∥r ‘ 𝑃 )
38 10 33 37 rspsn ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 ) → ( ( RSpan ‘ 𝑃 ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) = { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 } )
39 24 36 38 syl2anc ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑃 ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) = { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 } )
40 nfv ⊢ Ⅎ 𝑝 𝜑
41 nfab1 ⊢ Ⅎ 𝑝 { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 }
42 nfrab1 ⊢ Ⅎ 𝑝 { 𝑝 ∈ 𝑈 ∣ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) }
43 10 37 dvdsrcl2 ⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ) → 𝑝 ∈ 𝑈 )
44 43 ex ⊢ ( 𝑃 ∈ Ring → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 → 𝑝 ∈ 𝑈 ) )
45 44 pm4.71rd ⊢ ( 𝑃 ∈ Ring → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ↔ ( 𝑝 ∈ 𝑈 ∧ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ) ) )
46 24 45 syl ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ↔ ( 𝑝 ∈ 𝑈 ∧ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ) ) )
47 22 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐾 ∈ Ring )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
49 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
50 1 fveq2i ⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) )
51 49 5 6 4 7 50 minplym1p ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ 𝐾 ) )
52 eqid ⊢ ( Unic1p ‘ 𝐾 ) = ( Unic1p ‘ 𝐾 )
53 eqid ⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ 𝐾 )
54 52 53 mon1puc1p ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
55 22 51 54 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
57 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
58 9 37 10 52 57 16 dvdsr1p ⊢ ( ( 𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) ) → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ↔ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) = ( 0g ‘ 𝑃 ) ) )
59 47 48 56 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ↔ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) = ( 0g ‘ 𝑃 ) ) )
60 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) ∈ V )
61 17 fvmpt2 ⊢ ( ( 𝑝 ∈ 𝑈 ∧ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) ∈ V ) → ( 𝐻 ‘ 𝑝 ) = ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
62 48 60 61 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝐻 ‘ 𝑝 ) = ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
63 62 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) ↔ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) = ( 0g ‘ 𝑃 ) ) )
64 59 63 bitr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ↔ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) ) )
65 64 pm5.32da ⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝑈 ∧ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ) ↔ ( 𝑝 ∈ 𝑈 ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) ) ) )
66 46 65 bitrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 ↔ ( 𝑝 ∈ 𝑈 ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) ) ) )
67 abid ⊢ ( 𝑝 ∈ { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 } ↔ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 )
68 rabid ⊢ ( 𝑝 ∈ { 𝑝 ∈ 𝑈 ∣ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) } ↔ ( 𝑝 ∈ 𝑈 ∧ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) ) )
69 66 67 68 3bitr4g ⊢ ( 𝜑 → ( 𝑝 ∈ { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 } ↔ 𝑝 ∈ { 𝑝 ∈ 𝑈 ∣ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) } ) )
70 40 41 42 69 eqrd ⊢ ( 𝜑 → { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 } = { 𝑝 ∈ 𝑈 ∣ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) } )
71 40 60 17 fnmptd ⊢ ( 𝜑 → 𝐻 Fn 𝑈 )
72 fniniseg2 ⊢ ( 𝐻 Fn 𝑈 → ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) = { 𝑝 ∈ 𝑈 ∣ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) } )
73 71 72 syl ⊢ ( 𝜑 → ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) = { 𝑝 ∈ 𝑈 ∣ ( 𝐻 ‘ 𝑝 ) = ( 0g ‘ 𝑃 ) } )
74 70 73 eqtr4d ⊢ ( 𝜑 → { 𝑝 ∣ ( 𝑀 ‘ 𝐴 ) ( ∥r ‘ 𝑃 ) 𝑝 } = ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) )
75 18 39 74 3eqtrd ⊢ ( 𝜑 → 𝑍 = ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) )
76 75 oveq2d ⊢ ( 𝜑 → ( 𝑃 ~QG 𝑍 ) = ( 𝑃 ~QG ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) ) )
77 76 oveq2d ⊢ ( 𝜑 → ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) ) = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) ) ) )
78 14 77 eqtrid ⊢ ( 𝜑 → 𝑄 = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) ) ) )
79 eqid ⊢ ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) = ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } )
80 eqid ⊢ ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) ) ) = ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) ) )
81 9 10 16 52 17 22 55 57 79 80 r1pquslmic ⊢ ( 𝜑 → ( 𝑃 /s ( 𝑃 ~QG ( ◡ 𝐻 “ { ( 0g ‘ 𝑃 ) } ) ) ) ≃𝑚 ( 𝐻 “s 𝑃 ) )
82 78 81 eqbrtrd ⊢ ( 𝜑 → 𝑄 ≃𝑚 ( 𝐻 “s 𝑃 ) )
83 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem3 ⊢ ( 𝜑 → 𝑄 ∈ LVec )
84 82 83 lmicdim ⊢ ( 𝜑 → ( dim ‘ 𝑄 ) = ( dim ‘ ( 𝐻 “s 𝑃 ) ) )