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

Metamath Proof Explorer

Theorem algextdeglem7

Description: Lemma for algextdeg . The polynomials X of lower degree than the minimal polynomial are left unchanged when taking the remainder of the division by that minimal polynomial. (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 ⊢ 𝐻 = ( 𝑝 ∈ 𝑈 ↦ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
algextdeglem.t ⊢ 𝑇 = ( ◡ ( deg1 ‘ 𝐾 ) “ ( -∞ [,) ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
algextdeglem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
Assertion algextdeglem7 ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝐻 ‘ 𝑋 ) = 𝑋 ) )

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 algextdeglem.t ⊢ 𝑇 = ( ◡ ( deg1 ‘ 𝐾 ) “ ( -∞ [,) ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
19 algextdeglem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
20 1 fveq2i ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
21 9 20 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
22 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
23 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
24 5 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
25 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
26 6 25 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
27 8 1 22 23 24 26 irngssv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
28 27 7 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
29 eqid ⊢ { 𝑝 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = { 𝑝 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) }
30 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
31 eqid ⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
32 8 21 22 5 6 28 23 29 30 31 4 minplycl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )
33 32 10 eleqtrrdi ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 )
34 1 3 9 10 33 26 ressdeg1 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝐴 ) ) )
35 34 breq2d ⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
36 eqid ⊢ ( deg1 ‘ 𝐾 ) = ( deg1 ‘ 𝐾 )
37 5 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
38 37 drngringd ⊢ ( 𝜑 → 𝐸 ∈ Ring )
39 eqid ⊢ ( Poly1 ‘ 𝐸 ) = ( Poly1 ‘ 𝐸 )
40 eqid ⊢ ( PwSer1 ‘ 𝐾 ) = ( PwSer1 ‘ 𝐾 )
41 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) = ( Base ‘ ( PwSer1 ‘ 𝐾 ) )
42 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) = ( Base ‘ ( Poly1 ‘ 𝐸 ) )
43 39 1 9 10 26 40 41 42 ressply1bas2 ⊢ ( 𝜑 → 𝑈 = ( ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ) )
44 inss2 ⊢ ( ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝐸 ) )
45 43 44 eqsstrdi ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) )
46 45 33 sseldd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) )
47 eqid ⊢ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
48 47 5 6 4 7 irngnminplynz ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) )
49 3 39 47 42 deg1nn0cl ⊢ ( ( 𝐸 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ∧ ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) ) → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
50 38 46 48 49 syl3anc ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
51 fldsdrgfld ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ) → ( 𝐸 ↾s 𝐹 ) ∈ Field )
52 5 6 51 syl2anc ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Field )
53 1 52 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ Field )
54 fldidom ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ IDomn )
55 53 54 syl ⊢ ( 𝜑 → 𝐾 ∈ IDomn )
56 55 idomringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
57 9 36 18 50 56 10 ply1degleel ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝑋 ∈ 𝑈 ∧ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) ) )
58 19 57 mpbirand ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
59 eqid ⊢ ( Unic1p ‘ 𝐾 ) = ( Unic1p ‘ 𝐾 )
60 55 idomdomd ⊢ ( 𝜑 → 𝐾 ∈ Domn )
61 1 fveq2i ⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) )
62 47 5 6 4 7 61 minplym1p ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ 𝐾 ) )
63 eqid ⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ 𝐾 )
64 59 63 mon1puc1p ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
65 56 62 64 syl2anc ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
66 9 10 59 16 36 60 19 65 r1pid2 ⊢ ( 𝜑 → ( ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) = 𝑋 ↔ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
67 35 58 66 3bitr4d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) = 𝑋 ) )
68 oveq1 ⊢ ( 𝑝 = 𝑋 → ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) = ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
69 ovexd ⊢ ( 𝜑 → ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) ∈ V )
70 17 68 19 69 fvmptd3 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
71 70 eqeq1d ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) = 𝑋 ↔ ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) = 𝑋 ) )
72 67 71 bitr4d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝐻 ‘ 𝑋 ) = 𝑋 ) )