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 ↾_{𝑠} F$
	algextdeg.l	$⊢ L = E ↾_{𝑠} (E fldGen (F \cup \{A\}))$
	algextdeg.d	$⊢ D = \deg_{1} (E)$
	algextdeg.m	$⊢ M = E minPoly F$
	algextdeg.f	$⊢ φ \to E \in Field$
	algextdeg.e	$⊢ φ \to F \in SubDRing (E)$
	algextdeg.a	$⊢ φ \to A \in (E IntgRing F)$
	algextdeglem.o	$⊢ O = E {evalSub}_{1} F$
	algextdeglem.y	$⊢ P = {Poly}_{1} (K)$
	algextdeglem.u	$⊢ U = {Base}_{P}$
	algextdeglem.g	$⊢ G = (p \in U ⟼ O (p) (A))$
	algextdeglem.n	$⊢ N = (x \in U ⟼ [x] (P ~_{QG} Z))$
	algextdeglem.z	$⊢ Z = G^{-1} [\{0_{L}\}]$
	algextdeglem.q	$⊢ Q = P /_{𝑠} (P ~_{QG} Z)$
	algextdeglem.j	$⊢ J = (p \in {Base}_{Q} ⟼ ⋃ G [p])$
	algextdeglem.r	$⊢ R = {rem}_{1p} (K)$
	algextdeglem.h	$⊢ H = (p \in U ⟼ p R M (A))$
Assertion	algextdeglem6	$⊢ φ \to \dim (Q) = \dim (H “_{𝑠} P)$

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	$⊢ K = E ↾_{𝑠} F$
2		algextdeg.l	$⊢ L = E ↾_{𝑠} (E fldGen (F \cup \{A\}))$
3		algextdeg.d	$⊢ D = \deg_{1} (E)$
4		algextdeg.m	$⊢ M = E minPoly F$
5		algextdeg.f	$⊢ φ \to E \in Field$
6		algextdeg.e	$⊢ φ \to F \in SubDRing (E)$
7		algextdeg.a	$⊢ φ \to A \in (E IntgRing F)$
8		algextdeglem.o	$⊢ O = E {evalSub}_{1} F$
9		algextdeglem.y	$⊢ P = {Poly}_{1} (K)$
10		algextdeglem.u	$⊢ U = {Base}_{P}$
11		algextdeglem.g	$⊢ G = (p \in U ⟼ O (p) (A))$
12		algextdeglem.n	$⊢ N = (x \in U ⟼ [x] (P ~_{QG} Z))$
13		algextdeglem.z	$⊢ Z = G^{-1} [\{0_{L}\}]$
14		algextdeglem.q	$⊢ Q = P /_{𝑠} (P ~_{QG} Z)$
15		algextdeglem.j	$⊢ J = (p \in {Base}_{Q} ⟼ ⋃ G [p])$
16		algextdeglem.r	$⊢ R = {rem}_{1p} (K)$
17		algextdeglem.h	$⊢ H = (p \in U ⟼ p R M (A))$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	algextdeglem5	$⊢ φ \to Z = RSpan (P) (\{M (A)\})$
19		sdrgsubrg	$⊢ F \in SubDRing (E) \to F \in SubRing (E)$
20	6 19	syl	$⊢ φ \to F \in SubRing (E)$
21	1	subrgring	$⊢ F \in SubRing (E) \to K \in Ring$
22	20 21	syl	$⊢ φ \to K \in Ring$
23	9	ply1ring	$⊢ K \in Ring \to P \in Ring$
24	22 23	syl	$⊢ φ \to P \in Ring$
25	1	fveq2i	$⊢ {Poly}_{1} (K) = {Poly}_{1} (E ↾_{𝑠} F)$
26	9 25	eqtri	$⊢ P = {Poly}_{1} (E ↾_{𝑠} F)$
27		eqid	$⊢ {Base}_{E} = {Base}_{E}$
28		eqid	$⊢ 0_{E} = 0_{E}$
29	5	fldcrngd	$⊢ φ \to E \in CRing$
30	8 1 27 28 29 20	irngssv	$⊢ φ \to E IntgRing F \subseteq {Base}_{E}$
31	30 7	sseldd	$⊢ φ \to A \in {Base}_{E}$
32		eqid	$⊢ \{p \in dom O \| O (p) (A) = 0_{E}\} = \{p \in dom O \| O (p) (A) = 0_{E}\}$
33		eqid	$⊢ RSpan (P) = RSpan (P)$
34		eqid	$⊢ {idlGen}_{1p} (E ↾_{𝑠} F) = {idlGen}_{1p} (E ↾_{𝑠} F)$
35	8 26 27 5 6 31 28 32 33 34 4	minplycl	$⊢ φ \to M (A) \in {Base}_{P}$
36	35 10	eleqtrrdi	$⊢ φ \to M (A) \in U$
37		eqid	$⊢ ∥_{r} (P) = ∥_{r} (P)$
38	10 33 37	rspsn	$⊢ (P \in Ring \land M (A) \in U) \to RSpan (P) (\{M (A)\}) = \{p \| M (A) ∥_{r} (P) p\}$
39	24 36 38	syl2anc	$⊢ φ \to RSpan (P) (\{M (A)\}) = \{p \| M (A) ∥_{r} (P) p\}$
40		nfv	$⊢ Ⅎ p φ$
41		nfab1	$⊢ \underline{Ⅎ} p \{p \| M (A) ∥_{r} (P) p\}$
42		nfrab1	$⊢ \underline{Ⅎ} p \{p \in U \| H (p) = 0_{P}\}$
43	10 37	dvdsrcl2	$⊢ (P \in Ring \land M (A) ∥_{r} (P) p) \to p \in U$
44	43	ex	$⊢ P \in Ring \to (M (A) ∥_{r} (P) p \to p \in U)$
45	44	pm4.71rd	$⊢ P \in Ring \to (M (A) ∥_{r} (P) p \leftrightarrow (p \in U \land M (A) ∥_{r} (P) p))$
46	24 45	syl	$⊢ φ \to (M (A) ∥_{r} (P) p \leftrightarrow (p \in U \land M (A) ∥_{r} (P) p))$
47	22	adantr	$⊢ (φ \land p \in U) \to K \in Ring$
48		simpr	$⊢ (φ \land p \in U) \to p \in U$
49		eqid	$⊢ 0_{{Poly}_{1} (E)} = 0_{{Poly}_{1} (E)}$
50	1	fveq2i	$⊢ {Monic}_{1p} (K) = {Monic}_{1p} (E ↾_{𝑠} F)$
51	49 5 6 4 7 50	minplym1p	$⊢ φ \to M (A) \in {Monic}_{1p} (K)$
52		eqid	$⊢ {Unic}_{1p} (K) = {Unic}_{1p} (K)$
53		eqid	$⊢ {Monic}_{1p} (K) = {Monic}_{1p} (K)$
54	52 53	mon1puc1p	$⊢ (K \in Ring \land M (A) \in {Monic}_{1p} (K)) \to M (A) \in {Unic}_{1p} (K)$
55	22 51 54	syl2anc	$⊢ φ \to M (A) \in {Unic}_{1p} (K)$
56	55	adantr	$⊢ (φ \land p \in U) \to M (A) \in {Unic}_{1p} (K)$
57		eqid	$⊢ 0_{P} = 0_{P}$
58	9 37 10 52 57 16	dvdsr1p	$⊢ (K \in Ring \land p \in U \land M (A) \in {Unic}_{1p} (K)) \to (M (A) ∥_{r} (P) p \leftrightarrow p R M (A) = 0_{P})$
59	47 48 56 58	syl3anc	$⊢ (φ \land p \in U) \to (M (A) ∥_{r} (P) p \leftrightarrow p R M (A) = 0_{P})$
60		ovexd	$⊢ (φ \land p \in U) \to p R M (A) \in V$
61	17	fvmpt2	$⊢ (p \in U \land p R M (A) \in V) \to H (p) = p R M (A)$
62	48 60 61	syl2anc	$⊢ (φ \land p \in U) \to H (p) = p R M (A)$
63	62	eqeq1d	$⊢ (φ \land p \in U) \to (H (p) = 0_{P} \leftrightarrow p R M (A) = 0_{P})$
64	59 63	bitr4d	$⊢ (φ \land p \in U) \to (M (A) ∥_{r} (P) p \leftrightarrow H (p) = 0_{P})$
65	64	pm5.32da	$⊢ φ \to ((p \in U \land M (A) ∥_{r} (P) p) \leftrightarrow (p \in U \land H (p) = 0_{P}))$
66	46 65	bitrd	$⊢ φ \to (M (A) ∥_{r} (P) p \leftrightarrow (p \in U \land H (p) = 0_{P}))$
67		abid	$⊢ p \in \{p \| M (A) ∥_{r} (P) p\} \leftrightarrow M (A) ∥_{r} (P) p$
68		rabid	$⊢ p \in \{p \in U \| H (p) = 0_{P}\} \leftrightarrow (p \in U \land H (p) = 0_{P})$
69	66 67 68	3bitr4g	$⊢ φ \to (p \in \{p \| M (A) ∥_{r} (P) p\} \leftrightarrow p \in \{p \in U \| H (p) = 0_{P}\})$
70	40 41 42 69	eqrd	$⊢ φ \to \{p \| M (A) ∥_{r} (P) p\} = \{p \in U \| H (p) = 0_{P}\}$
71	40 60 17	fnmptd	$⊢ φ \to H Fn U$
72		fniniseg2	$⊢ H Fn U \to H^{-1} [\{0_{P}\}] = \{p \in U \| H (p) = 0_{P}\}$
73	71 72	syl	$⊢ φ \to H^{-1} [\{0_{P}\}] = \{p \in U \| H (p) = 0_{P}\}$
74	70 73	eqtr4d	$⊢ φ \to \{p \| M (A) ∥_{r} (P) p\} = H^{-1} [\{0_{P}\}]$
75	18 39 74	3eqtrd	$⊢ φ \to Z = H^{-1} [\{0_{P}\}]$
76	75	oveq2d	$⊢ φ \to P ~_{QG} Z = P ~_{QG} H^{-1} [\{0_{P}\}]$
77	76	oveq2d	$⊢ φ \to P /_{𝑠} (P ~_{QG} Z) = P /_{𝑠} (P ~_{QG} H^{-1} [\{0_{P}\}])$
78	14 77	eqtrid	$⊢ φ \to Q = P /_{𝑠} (P ~_{QG} H^{-1} [\{0_{P}\}])$
79		eqid	$⊢ H^{-1} [\{0_{P}\}] = H^{-1} [\{0_{P}\}]$
80		eqid	$⊢ P /_{𝑠} (P ~_{QG} H^{-1} [\{0_{P}\}]) = P /_{𝑠} (P ~_{QG} H^{-1} [\{0_{P}\}])$
81	9 10 16 52 17 22 55 57 79 80	r1pquslmic	$⊢ φ \to (P /_{𝑠} (P ~_{QG} H^{-1} [\{0_{P}\}])) ≃_{𝑚} (H “_{𝑠} P)$
82	78 81	eqbrtrd	$⊢ φ \to Q ≃_{𝑚} (H “_{𝑠} P)$
83	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	algextdeglem3	$⊢ φ \to Q \in LVec$
84	82 83	lmicdim	$⊢ φ \to \dim (Q) = \dim (H “_{𝑠} P)$

Metamath Proof Explorer

Theorem algextdeglem6

Proof