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 𝑃 ) ) )