Theorem algextdeglem2 34343

Description: Lemma for algextdeg 34350. Both the ring of polynomials 𝑃 and the field 𝐿 generated by 𝐾 and the algebraic element 𝐴 can be considered as modules over the elements of 𝐹. Then, the evaluation map 𝐺, mapping polynomials to their evaluation at 𝐴, is a module homomorphism between those modules. (Contributed by Thierry Arnoux, 2-Apr-2025.)

Hypotheses

Ref	Expression
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‘𝑄) ↦ ∪ (𝐺 “ 𝑝))

Assertion

Ref	Expression
algextdeglem2	⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))

Distinct variable groups:   𝐴,𝑝   𝐸,𝑝   𝐹,𝑝,𝑥   𝐺,𝑝,𝑥   𝐽,𝑝,𝑥   𝐾,𝑝   𝐿,𝑝,𝑥   𝑥,𝑁   𝑂,𝑝   𝑃,𝑝,𝑥   𝑄,𝑝,𝑥   𝑈,𝑝,𝑥   𝑍,𝑝,𝑥   𝜑,𝑝,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐷(𝑥, 𝑝)   𝐸(𝑥)   𝐾(𝑥)   𝑀(𝑥, 𝑝)   𝑁(𝑝)   𝑂(𝑥)

Proof of Theorem algextdeglem2

Step	Hyp	Ref	Expression
1		algextdeg.e	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
2		issdrg 21038	. . . . . 6 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
3	1, 2	sylib 221	. . . . 5 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
4	3	simp2d 1161	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		eqid 2761	. . . . 5 ⊢ ((subringAlg ‘𝐸)‘𝐹) = ((subringAlg ‘𝐸)‘𝐹)
6	5	sralmod 21455	. . . 4 ⊢ (𝐹 ∈ (SubRing‘𝐸) → ((subringAlg ‘𝐸)‘𝐹) ∈ LMod)
7	4, 6	syl 18	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐸)‘𝐹) ∈ LMod)
8		eqid 2761	. . . 4 ⊢ (Base‘𝐸) = (Base‘𝐸)
9		eqid 2761	. . . 4 ⊢ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
10		algextdeg.f	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ Field)
11	10	flddrngd 20987	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ DivRing)
12		subrgsubg 20822	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
13	8	subgss 19330	. . . . . . . . 9 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
14	4, 12, 13	3syl 19	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
15		algextdeglem.o	. . . . . . . . . . 11 ⊢ 𝑂 = (𝐸 evalSub1 𝐹)
16		algextdeg.k	. . . . . . . . . . 11 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
17		eqid 2761	. . . . . . . . . . 11 ⊢ (0g‘𝐸) = (0g‘𝐸)
18	10	fldcrngd 20988	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ CRing)
19	15, 16, 8, 17, 18, 4	irngssv 34313	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
20		algextdeg.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
21	19, 20	sseldd 3932	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
22	21	snssd 4747	. . . . . . . 8 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
23	14, 22	unssd 4138	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
24	8, 11, 23	fldgensdrg 33869	. . . . . 6 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
25		issdrg 21038	. . . . . 6 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
26	24, 25	sylib 221	. . . . 5 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
27	26	simp2d 1161	. . . 4 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
28	8, 11, 23	fldgenssid 33868	. . . . . 6 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
29	28	unssad 4139	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
30	9	subsubrg 20843	. . . . . 6 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘(𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
31	30	biimpar 483	. . . . 5 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘(𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))))
32	27, 4, 29, 31	syl12anc 850	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘(𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))))
33	5, 8, 9, 27, 32	lsssra 34213	. . 3 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (LSubSp‘((subringAlg ‘𝐸)‘𝐹)))
34		algextdeglem.y	. . . . . . 7 ⊢ 𝑃 = (Poly1‘𝐾)
35	16	fveq2i 6886	. . . . . . 7 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
36	34, 35	eqtri 2784	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
37		algextdeglem.u	. . . . . 6 ⊢ 𝑈 = (Base‘𝑃)
38	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐸 ∈ Field)
39	1	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubDRing‘𝐸))
40	21	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐸))
41		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
42	8, 15, 36, 37, 38, 39, 40, 41	evls1fldgencl 34295	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	42	ralrimiva 3155	. . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
44		algextdeglem.g	. . . . 5 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
45	44	rnmptss 7121	. . . 4 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
46	43, 45	syl 18	. . 3 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
47	15, 36, 8, 37, 18, 4, 21, 44, 5	evls1maplmhm 22688	. . 3 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)))
48		eqid 2761	. . . . 5 ⊢ (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) = (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
49		eqid 2761	. . . . 5 ⊢ (LSubSp‘((subringAlg ‘𝐸)‘𝐹)) = (LSubSp‘((subringAlg ‘𝐸)‘𝐹))
50	48, 49	reslmhm2b 21322	. . . 4 ⊢ ((((subringAlg ‘𝐸)‘𝐹) ∈ LMod ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (LSubSp‘((subringAlg ‘𝐸)‘𝐹)) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹)) ↔ 𝐺 ∈ (𝑃 LMHom (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))))))
51	50	biimpa 482	. . 3 ⊢ (((((subringAlg ‘𝐸)‘𝐹) ∈ LMod ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (LSubSp‘((subringAlg ‘𝐸)‘𝐹)) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐸)‘𝐹))) → 𝐺 ∈ (𝑃 LMHom (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))))
52	7, 33, 46, 47, 51	syl31anc 1400	. 2 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))))
53		algextdeg.l	. . . 4 ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
54	8, 11, 23	fldgenssv 33870	. . . 4 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
55	8, 53, 54, 29, 10	resssra 34212	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))))
56	55	oveq2d 7434	. 2 ⊢ (𝜑 → (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)) = (𝑃 LMHom (((subringAlg ‘𝐸)‘𝐹) ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))))
57	52, 56	eleqtrrd 2864	1 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077   ∪ cun 3897   ⊆ wss 3899  {csn 4584  ∪ cuni 4867   ↦ cmpt 5186  ^◡ccnv 5650  ran crn 5652   “ cima 5654  ‘cfv 6537  (class class class)co 7418  [cec 8708  Basecbs 17380   ↾_s cress 17401  0_gc0g 17603   /_s cqus 17670  SubGrpcsubg 19323   ~_QG cqg 19325  SubRingcsubrg 20814  DivRingcdr 20973  Fieldcfield 20974  SubDRingcsdrg 21036  LModclmod 21128  LSubSpclss 21199   LMHom clmhm 21287  subringAlg csra 21439  Poly₁cpl1 22488   evalSub₁ ces1 22624  deg₁cdg1 26365   fldGen cfldgen 33865   IntgRing cirng 34308   minPoly cminply 34324

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-ofr 7692  df-om 7876  df-1st 7999  df-2nd 8000  df-supp 8171  df-tpos 8236  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-er 8710  df-map 8842  df-pm 8843  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9347  df-sup 9427  df-oi 9497  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-z 12687  df-dec 12808  df-uz 12959  df-fz 13633  df-fzo 13782  df-seq 14138  df-hash 14468  df-struct 17318  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-ress 17402  df-plusg 17434  df-mulr 17435  df-sca 17437  df-vsca 17438  df-ip 17439  df-tset 17440  df-ple 17441  df-ds 17443  df-hom 17445  df-cco 17446  df-0g 17605  df-gsum 17606  df-prds 17611  df-pws 17613  df-mre 17749  df-mrc 17750  df-acs 17752  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-mhm 18971  df-submnd 18972  df-grp 19140  df-minusg 19141  df-sbg 19142  df-mulg 19271  df-subg 19326  df-ghm 19421  df-cntz 19524  df-cmn 19989  df-abl 19990  df-mgp 20354  df-rng 20368  df-ur 20401  df-srg 20406  df-ring 20454  df-cring 20455  df-oppr 20560  df-dvdsr 20580  df-unit 20581  df-invr 20611  df-dvr 20624  df-rhm 20695  df-subrng 20791  df-subrg 20815  df-drng 20975  df-field 20976  df-sdrg 21037  df-lmod 21130  df-lss 21200  df-lsp 21240  df-lmhm 21290  df-sra 21441  df-assa 22154  df-asp 22155  df-ascl 22156  df-psr 22210  df-mvr 22211  df-mpl 22212  df-opsr 22214  df-evls 22376  df-evl 22377  df-psr1 22491  df-vr1 22492  df-ply1 22493  df-coe1 22494  df-evls1 22626  df-evl1 22627  df-mon1 26442  df-fldgen 33866  df-irng 34309

This theorem is used by:  algextdeglem3  34344  algextdeglem4  34345