Theorem algextdeglem1 32767

Description: Lemma for - algextdeg . (Contributed by Thierry Arnoux, 22-Mar-2025.)

Hypotheses

Ref	Expression
algextdeg.k	⊢ 𝐾 = (𝐸 ↾s 𝐹)
algextdeg.l	⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
algextdeg.f	⊢ (𝜑 → 𝐸 ∈ Field)
algextdeg.e	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
algextdeg.a	⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
algextdeglem.o	⊢ 𝑂 = (𝐸 evalSub1 𝐹)
algextdeglem.y	⊢ 𝑃 = (Poly1‘𝐾)
algextdeglem.u	⊢ 𝑈 = (Base‘𝑃)
algextdeglem.g	⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
algextdeglem.1	⊢ 𝑂 = (𝐿 evalSub1 𝐹)
algextdeglem.2	⊢ 𝑃 = (Poly1‘(𝐿 ↾s 𝐹))
algextdeglem.3	⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))
algextdeglem.4	⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})
algextdeglem.5	⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))
algextdeglem.6	⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))

Assertion

Ref	Expression
algextdeglem1	⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

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

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

Proof of Theorem algextdeglem1

Dummy variable 𝑞 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		algextdeg.e	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
2		issdrg 20403	. . . . . . . 8 ⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
3	1, 2	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing))
4	3	simp2d 1143	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
5		subrgsubg 20324	. . . . . 6 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
6		eqid 2732	. . . . . . 7 ⊢ (Base‘𝐸) = (Base‘𝐸)
7	6	subgss 19006	. . . . . 6 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
8	4, 5, 7	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐸))
9		algextdeg.k	. . . . . 6 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
10	9, 6	ressbas2 17181	. . . . 5 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
11	8, 10	syl 17	. . . 4 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
12	11	fveq2d 6895	. . 3 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘(Base‘𝐾)))
13	12	fveq2d 6895	. 2 ⊢ (𝜑 → (dim‘((subringAlg ‘𝐿)‘𝐹)) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
14		eqid 2732	. . . . 5 ⊢ (0g‘((subringAlg ‘𝐿)‘𝐹)) = (0g‘((subringAlg ‘𝐿)‘𝐹))
15		algextdeglem.1	. . . . . 6 ⊢ 𝑂 = (𝐿 evalSub1 𝐹)
16		algextdeglem.2	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐿 ↾s 𝐹))
17		eqid 2732	. . . . . 6 ⊢ (Base‘𝐿) = (Base‘𝐿)
18		algextdeglem.u	. . . . . 6 ⊢ 𝑈 = (Base‘𝑃)
19		algextdeg.l	. . . . . . . 8 ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
20		algextdeg.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ Field)
21		algextdeglem.o	. . . . . . . . . . . . 13 ⊢ 𝑂 = (𝐸 evalSub1 𝐹)
22		eqid 2732	. . . . . . . . . . . . 13 ⊢ (0g‘𝐸) = (0g‘𝐸)
23	20	fldcrngd 20369	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
24	21, 9, 6, 22, 23, 4	irngssv 32747	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
25		algextdeg.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
26	24, 25	sseldd 3983	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
27	26	snssd 4812	. . . . . . . . . 10 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐸))
28	8, 27	unssd 4186	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (Base‘𝐸))
29	6, 20, 28	fldgenfld 32405	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ Field)
30	19, 29	eqeltrid 2837	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ Field)
31	30	fldcrngd 20369	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ CRing)
32	20	flddrngd 20368	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ DivRing)
33	6, 32, 28	fldgensdrg 32399	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸))
34		issdrg 20403	. . . . . . . . 9 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
35	33, 34	sylib 217	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ∈ DivRing ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∈ DivRing))
36	35	simp2d 1143	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
37	6, 32, 28	fldgenssid 32398	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
38	37	unssad 4187	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
39	19	subsubrg 20344	. . . . . . . 8 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐹 ∈ (SubRing‘𝐿) ↔ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))))
40	39	biimpar 478	. . . . . . 7 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ (𝐹 ∈ (SubRing‘𝐸) ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))) → 𝐹 ∈ (SubRing‘𝐿))
41	36, 4, 38, 40	syl12anc 835	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐿))
42	37	unssbd 4188	. . . . . . . 8 ⊢ (𝜑 → {𝐴} ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
43	6, 32, 28	fldgenssv 32400	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸))
44	19, 6	ressbas2 17181	. . . . . . . . 9 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
45	43, 44	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
46	42, 45	sseqtrd 4022	. . . . . . 7 ⊢ (𝜑 → {𝐴} ⊆ (Base‘𝐿))
47		snssg 4787	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐸 IntgRing 𝐹) → (𝐴 ∈ (Base‘𝐿) ↔ {𝐴} ⊆ (Base‘𝐿)))
48	47	biimpar 478	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐸 IntgRing 𝐹) ∧ {𝐴} ⊆ (Base‘𝐿)) → 𝐴 ∈ (Base‘𝐿))
49	25, 46, 48	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐿))
50		algextdeglem.g	. . . . . 6 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
51		eqid 2732	. . . . . 6 ⊢ ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹)
52	15, 16, 17, 18, 31, 41, 49, 50, 51	evls1maplmhm 32755	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)))
53		eqid 2732	. . . . 5 ⊢ (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})
54		eqid 2732	. . . . 5 ⊢ (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
55	31	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐿 ∈ CRing)
56	41	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐹 ∈ (SubRing‘𝐿))
57	49	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐴 ∈ (Base‘𝐿))
58		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
59	15, 16, 17, 18, 55, 56, 57, 58	evls1fvcl 32753	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (Base‘𝐿))
60	45	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝐸 fldGen (𝐹 ∪ {𝐴})) = (Base‘𝐿))
61	59, 60	eleqtrrd 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
62	61	ralrimiva 3146	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
63	50	rnmptss 7121	. . . . . . . 8 ⊢ (∀𝑝 ∈ 𝑈 ((𝑂‘𝑝)‘𝐴) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
64	62, 63	syl 17	. . . . . . 7 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴})))
65	15, 16, 17, 18, 31, 41, 49, 50	evls1maprhm 32754	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐿))
66	19	resrhm2b 20348	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → (𝐺 ∈ (𝑃 RingHom 𝐸) ↔ 𝐺 ∈ (𝑃 RingHom 𝐿)))
67	66	biimpar 478	. . . . . . . . . . 11 ⊢ ((((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) ∧ 𝐺 ∈ (𝑃 RingHom 𝐿)) → 𝐺 ∈ (𝑃 RingHom 𝐸))
68	36, 64, 65, 67	syl21anc 836	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (𝑃 RingHom 𝐸))
69		rnrhmsubrg 20351	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐸) → ran 𝐺 ∈ (SubRing‘𝐸))
70	68, 69	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐺 ∈ (SubRing‘𝐸))
71	19	oveq1i 7418	. . . . . . . . . . 11 ⊢ (𝐿 ↾s ran 𝐺) = ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺)
72		ovex 7441	. . . . . . . . . . . 12 ⊢ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V
73		ressabs 17193	. . . . . . . . . . . 12 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ ran 𝐺 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
74	72, 64, 73	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
75	71, 74	eqtrid 2784	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐸 ↾s ran 𝐺))
76		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐿) = (0g‘𝐿)
77		rhmghm 20261	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ (𝑃 RingHom 𝐿) → 𝐺 ∈ (𝑃 GrpHom 𝐿))
78	65, 77	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ∈ (𝑃 GrpHom 𝐿))
79		algextdeglem.4	. . . . . . . . . . . . . . 15 ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})
80		algextdeglem.5	. . . . . . . . . . . . . . 15 ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))
81		algextdeglem.6	. . . . . . . . . . . . . . 15 ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))
82		algextdeglem.3	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))
83	76, 78, 79, 80, 81, 18, 82	ghmquskerco 32524	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝐽 ∘ 𝑁))
84	83	rneqd 5937	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 = ran (𝐽 ∘ 𝑁))
85	80	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)))
86	18	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈 = (Base‘𝑃))
87		ovexd 7443	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 ~QG 𝑍) ∈ V)
88	19	oveq1i 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ↾s 𝐹) = ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s 𝐹)
89		ressabs 17193	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ V ∧ 𝐹 ⊆ (𝐸 fldGen (𝐹 ∪ {𝐴}))) → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s 𝐹) = (𝐸 ↾s 𝐹))
90	72, 38, 89	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) ↾s 𝐹) = (𝐸 ↾s 𝐹))
91	88, 90	eqtrid 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = (𝐸 ↾s 𝐹))
92	3	simp3d 1144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing)
93	91, 92	eqeltrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 ↾s 𝐹) ∈ DivRing)
94	16, 93	ply1lvec 32633	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LVec)
95	85, 86, 87, 94	qusbas 17490	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 / (𝑃 ~QG 𝑍)) = (Base‘𝑄))
96		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 / (𝑃 ~QG 𝑍)) = (𝑈 / (𝑃 ~QG 𝑍))
97	76	ghmker 19117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ (𝑃 GrpHom 𝐿) → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
98	78, 97	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) ∈ (NrmSGrp‘𝑃))
99	79, 98	eqeltrid 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ (NrmSGrp‘𝑃))
100	18, 96, 82, 99	qusrn 32515	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑁 = (𝑈 / (𝑃 ~QG 𝑍)))
101	52	elexd 3494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐺 ∈ V)
102	101	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → 𝐺 ∈ V)
103	102	imaexd 31899	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → (𝐺 “ 𝑝) ∈ V)
104	103	uniexd 7731	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (Base‘𝑄)) → ∪ (𝐺 “ 𝑝) ∈ V)
105	81, 104	dmmptd 6695	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐽 = (Base‘𝑄))
106	95, 100, 105	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐽 = ran 𝑁)
107		rncoeq 5974	. . . . . . . . . . . . . 14 ⊢ (dom 𝐽 = ran 𝑁 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
108	106, 107	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐽 ∘ 𝑁) = ran 𝐽)
109	84, 108	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐺 = ran 𝐽)
110	109	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) = (𝐿 ↾s ran 𝐽))
111		eqid 2732	. . . . . . . . . . . 12 ⊢ (𝐿 ↾s ran 𝐽) = (𝐿 ↾s ran 𝐽)
112	9	subrgcrng 20322	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝐾 ∈ CRing)
113	23, 4, 112	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ CRing)
114		algextdeglem.y	. . . . . . . . . . . . . . 15 ⊢ 𝑃 = (Poly1‘𝐾)
115	114	ply1crng 21721	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ CRing → 𝑃 ∈ CRing)
116	113, 115	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ CRing)
117	76, 65, 79, 80, 81, 116	rhmquskerlem 32538	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐿))
118	15, 16, 17, 18, 31, 41, 49, 50	evls1maprnss 32756	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ⊆ ran 𝐺)
119		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (1r‘𝐸) = (1r‘𝐸)
120	9, 119	subrg1 20328	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) = (1r‘𝐾))
121	4, 120	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
122	119	subrg1cl 20326	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
123	4, 122	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
124	121, 123	eqeltrrd 2834	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ∈ 𝐹)
125	118, 124	sseldd 3983	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ ran 𝐺)
126		drngnzr 20376	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
127	119, 22	nzrnz 20293	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ (0g‘𝐸))
128	32, 126, 127	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1r‘𝐸) ≠ (0g‘𝐸))
129	23	crnggrpd 20069	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐸 ∈ Grp)
130	129	grpmndd 18831	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ Mnd)
131		sdrgsubrg 20406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubDRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸))
132		subrgsubg 20324	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubRing‘𝐸) → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
133	33, 131, 132	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸))
134	22	subg0cl 19013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐸 fldGen (𝐹 ∪ {𝐴})) ∈ (SubGrp‘𝐸) → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
135	133, 134	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})))
136	19, 6, 22	ress0g 18652	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 ∈ Mnd ∧ (0g‘𝐸) ∈ (𝐸 fldGen (𝐹 ∪ {𝐴})) ∧ (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ (Base‘𝐸)) → (0g‘𝐸) = (0g‘𝐿))
137	130, 135, 43, 136	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐿))
138	128, 121, 137	3netr3d 3017	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1r‘𝐾) ≠ (0g‘𝐿))
139		nelsn 4668	. . . . . . . . . . . . . . 15 ⊢ ((1r‘𝐾) ≠ (0g‘𝐿) → ¬ (1r‘𝐾) ∈ {(0g‘𝐿)})
140	138, 139	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (1r‘𝐾) ∈ {(0g‘𝐿)})
141		nelne1 3039	. . . . . . . . . . . . . 14 ⊢ (((1r‘𝐾) ∈ ran 𝐺 ∧ ¬ (1r‘𝐾) ∈ {(0g‘𝐿)}) → ran 𝐺 ≠ {(0g‘𝐿)})
142	125, 140, 141	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐺 ≠ {(0g‘𝐿)})
143	109, 142	eqnetrrd 3009	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐽 ≠ {(0g‘𝐿)})
144		eqid 2732	. . . . . . . . . . . . 13 ⊢ (oppr‘𝑃) = (oppr‘𝑃)
145	9	sdrgdrng 20405	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
146		drngnzr 20376	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
147	1, 145, 146	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ NzRing)
148	114	ply1nz 25638	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ NzRing → 𝑃 ∈ NzRing)
149	147, 148	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ NzRing)
150	9	fveq2i 6894	. . . . . . . . . . . . . . . . 17 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
151	114, 150	eqtri 2760	. . . . . . . . . . . . . . . 16 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
152		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}
153		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
154		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
155	21, 151, 6, 20, 1, 26, 22, 152, 153, 154	ply1annig1p 32760	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = ((RSpan‘𝑃)‘{((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
156		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐿)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐿)}
157	18	mpteq1i 5244	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
158	50, 157	eqtri 2760	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐺 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴))
159	15, 16, 17, 31, 41, 49, 76, 156, 158	ply1annidllem 32757	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐿)} = (◡𝐺 “ {(0g‘𝐿)}))
160	79, 159	eqtr4id 2791	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐿)})
161	137	eqeq2d 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑂‘𝑞)‘𝐴) = (0g‘𝐸) ↔ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐿)))
162	161	rabbidv 3440	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐿)})
163	160, 162	eqtr4d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑍 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})
164		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
165	21, 151, 6, 20, 1, 26, 22, 152, 153, 154, 164	minplyval 32761	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) = ((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}))
166	165	sneqd 4640	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} = {((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})})
167	166	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})}))
168	155, 163, 167	3eqtr4d 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}))
169		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (0g‘𝑃) = (0g‘𝑃)
170		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (0g‘(Poly1‘𝐸)) = (0g‘(Poly1‘𝐸))
171	170, 20, 1, 164, 25	irngnminplynz 32766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘(Poly1‘𝐸)))
172		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
173	172, 9, 114, 18, 4, 170	ressply10g 32651	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0g‘(Poly1‘𝐸)) = (0g‘𝑃))
174	171, 173	neeqtrd 3010	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ≠ (0g‘𝑃))
175	21, 151, 6, 20, 1, 26, 164, 169, 174	minplyirred 32765	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃))
176		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) = ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)})
177		fldsdrgfld 20413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
178	20, 1, 177	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
179	9, 178	eqeltrid 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ Field)
180	114	ply1pid 25696	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ Field → 𝑃 ∈ PID)
181	179, 180	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ PID)
182	21, 151, 6, 20, 1, 26, 22, 152, 153, 154, 164	minplycl 32762	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Base‘𝑃))
183	182, 86	eleqtrrd 2836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝐴) ∈ 𝑈)
184	116	crngringd 20068	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ Ring)
185	183	snssd 4812	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈)
186		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (LIdeal‘𝑃) = (LIdeal‘𝑃)
187	153, 18, 186	rspcl 20846	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ Ring ∧ {((𝐸 minPoly 𝐹)‘𝐴)} ⊆ 𝑈) → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
188	184, 185, 187	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (LIdeal‘𝑃))
189	18, 153, 169, 176, 181, 183, 174, 188	mxidlirred 32583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃) ↔ ((𝐸 minPoly 𝐹)‘𝐴) ∈ (Irred‘𝑃)))
190	175, 189	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((RSpan‘𝑃)‘{((𝐸 minPoly 𝐹)‘𝐴)}) ∈ (MaxIdeal‘𝑃))
191	168, 190	eqeltrd 2833	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘𝑃))
192		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (MaxIdeal‘𝑃) = (MaxIdeal‘𝑃)
193	192, 144	crngmxidl 32580	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ CRing → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
194	116, 193	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (MaxIdeal‘𝑃) = (MaxIdeal‘(oppr‘𝑃)))
195	191, 194	eleqtrd 2835	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (MaxIdeal‘(oppr‘𝑃)))
196	144, 80, 149, 191, 195	qsdrngi 32604	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ DivRing)
197	111, 76, 117, 143, 196	rndrhmcl 32391	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 ↾s ran 𝐽) ∈ DivRing)
198	110, 197	eqeltrd 2833	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ↾s ran 𝐺) ∈ DivRing)
199	75, 198	eqeltrrd 2834	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾s ran 𝐺) ∈ DivRing)
200		issdrg 20403	. . . . . . . . 9 ⊢ (ran 𝐺 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ ran 𝐺 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s ran 𝐺) ∈ DivRing))
201	32, 70, 199, 200	syl3anbrc 1343	. . . . . . . 8 ⊢ (𝜑 → ran 𝐺 ∈ (SubDRing‘𝐸))
202	92	drngringd 20364	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Ring)
203		eqid 2732	. . . . . . . . . . . . . 14 ⊢ (var1‘(𝐸 ↾s 𝐹)) = (var1‘(𝐸 ↾s 𝐹))
204	203, 151, 18	vr1cl 21740	. . . . . . . . . . . . 13 ⊢ ((𝐸 ↾s 𝐹) ∈ Ring → (var1‘(𝐸 ↾s 𝐹)) ∈ 𝑈)
205	202, 204	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (var1‘(𝐸 ↾s 𝐹)) ∈ 𝑈)
206		fveq2 6891	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (var1‘(𝐸 ↾s 𝐹)) → (𝑂‘𝑝) = (𝑂‘(var1‘(𝐸 ↾s 𝐹))))
207	206	fveq1d 6893	. . . . . . . . . . . . . 14 ⊢ (𝑝 = (var1‘(𝐸 ↾s 𝐹)) → ((𝑂‘𝑝)‘𝐴) = ((𝑂‘(var1‘(𝐸 ↾s 𝐹)))‘𝐴))
208	207	eqeq2d 2743	. . . . . . . . . . . . 13 ⊢ (𝑝 = (var1‘(𝐸 ↾s 𝐹)) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var1‘(𝐸 ↾s 𝐹)))‘𝐴)))
209	208	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 = (var1‘(𝐸 ↾s 𝐹))) → (𝐴 = ((𝑂‘𝑝)‘𝐴) ↔ 𝐴 = ((𝑂‘(var1‘(𝐸 ↾s 𝐹)))‘𝐴)))
210	91	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var1‘(𝐿 ↾s 𝐹)) = (var1‘(𝐸 ↾s 𝐹)))
211	210	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑂‘(var1‘(𝐿 ↾s 𝐹))) = (𝑂‘(var1‘(𝐸 ↾s 𝐹))))
212		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (var1‘(𝐿 ↾s 𝐹)) = (var1‘(𝐿 ↾s 𝐹))
213		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ↾s 𝐹) = (𝐿 ↾s 𝐹)
214	15, 212, 213, 17, 31, 41	evls1var 21856	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑂‘(var1‘(𝐿 ↾s 𝐹))) = ( I ↾ (Base‘𝐿)))
215	211, 214	eqtr3d 2774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘(var1‘(𝐸 ↾s 𝐹))) = ( I ↾ (Base‘𝐿)))
216	215	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑂‘(var1‘(𝐸 ↾s 𝐹)))‘𝐴) = (( I ↾ (Base‘𝐿))‘𝐴))
217		fvresi 7170	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (Base‘𝐿) → (( I ↾ (Base‘𝐿))‘𝐴) = 𝐴)
218	49, 217	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (( I ↾ (Base‘𝐿))‘𝐴) = 𝐴)
219	216, 218	eqtr2d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 = ((𝑂‘(var1‘(𝐸 ↾s 𝐹)))‘𝐴))
220	205, 209, 219	rspcedvd 3614	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑝 ∈ 𝑈 𝐴 = ((𝑂‘𝑝)‘𝐴))
221	50, 220, 25	elrnmptd 5960	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ran 𝐺)
222	221	snssd 4812	. . . . . . . . 9 ⊢ (𝜑 → {𝐴} ⊆ ran 𝐺)
223	118, 222	unssd 4186	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∪ {𝐴}) ⊆ ran 𝐺)
224	6, 32, 201, 223	fldgenssp 32403	. . . . . . 7 ⊢ (𝜑 → (𝐸 fldGen (𝐹 ∪ {𝐴})) ⊆ ran 𝐺)
225	64, 224	eqssd 3999	. . . . . 6 ⊢ (𝜑 → ran 𝐺 = (𝐸 fldGen (𝐹 ∪ {𝐴})))
226		eqidd 2733	. . . . . . 7 ⊢ (𝜑 → ((subringAlg ‘𝐿)‘𝐹) = ((subringAlg ‘𝐿)‘𝐹))
227	38, 45	sseqtrd 4022	. . . . . . 7 ⊢ (𝜑 → 𝐹 ⊆ (Base‘𝐿))
228	226, 227	srabase 20791	. . . . . 6 ⊢ (𝜑 → (Base‘𝐿) = (Base‘((subringAlg ‘𝐿)‘𝐹)))
229	225, 45, 228	3eqtrd 2776	. . . . 5 ⊢ (𝜑 → ran 𝐺 = (Base‘((subringAlg ‘𝐿)‘𝐹)))
230		imaeq2 6055	. . . . . . 7 ⊢ (𝑞 = 𝑝 → (𝐺 “ 𝑞) = (𝐺 “ 𝑝))
231	230	unieqd 4922	. . . . . 6 ⊢ (𝑞 = 𝑝 → ∪ (𝐺 “ 𝑞) = ∪ (𝐺 “ 𝑝))
232	231	cbvmptv 5261	. . . . 5 ⊢ (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝))
233	14, 52, 53, 54, 229, 232	lmhmqusker 32529	. . . 4 ⊢ (𝜑 → (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)) ∈ ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
234		eqidd 2733	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0g‘𝐿) = (0g‘𝐿))
235	226, 234, 227	sralmod0 20809	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0g‘𝐿) = (0g‘((subringAlg ‘𝐿)‘𝐹)))
236	235	sneqd 4640	. . . . . . . . . . . 12 ⊢ (𝜑 → {(0g‘𝐿)} = {(0g‘((subringAlg ‘𝐿)‘𝐹))})
237	236	imaeq2d 6059	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝐺 “ {(0g‘𝐿)}) = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
238	79, 237	eqtrid 2784	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))
239	238	oveq2d 7424	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ~QG 𝑍) = (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))
240	239	oveq2d 7424	. . . . . . . 8 ⊢ (𝜑 → (𝑃 /s (𝑃 ~QG 𝑍)) = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
241	80, 240	eqtrid 2784	. . . . . . 7 ⊢ (𝜑 → 𝑄 = (𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))))
242	241	fveq2d 6895	. . . . . 6 ⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))))
243	242	mpteq1d 5243	. . . . 5 ⊢ (𝜑 → (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) = (𝑝 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑝)))
244	243, 81, 232	3eqtr4g 2797	. . . 4 ⊢ (𝜑 → 𝐽 = (𝑞 ∈ (Base‘(𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))})))) ↦ ∪ (𝐺 “ 𝑞)))
245	241	oveq1d 7423	. . . 4 ⊢ (𝜑 → (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)) = ((𝑃 /s (𝑃 ~QG (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}))) LMIso ((subringAlg ‘𝐿)‘𝐹)))
246	233, 244, 245	3eltr4d 2848	. . 3 ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso ((subringAlg ‘𝐿)‘𝐹)))
247		eqid 2732	. . . . . . 7 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
248	53, 14, 247	lmhmkerlss 20661	. . . . . 6 ⊢ (𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹)) → (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}) ∈ (LSubSp‘𝑃))
249	52, 248	syl 17	. . . . 5 ⊢ (𝜑 → (◡𝐺 “ {(0g‘((subringAlg ‘𝐿)‘𝐹))}) ∈ (LSubSp‘𝑃))
250	238, 249	eqeltrd 2833	. . . 4 ⊢ (𝜑 → 𝑍 ∈ (LSubSp‘𝑃))
251	80, 94, 250	quslvec 32466	. . 3 ⊢ (𝜑 → 𝑄 ∈ LVec)
252	246, 251	lmimdim 32684	. 2 ⊢ (𝜑 → (dim‘𝑄) = (dim‘((subringAlg ‘𝐿)‘𝐹)))
253	90, 88, 9	3eqtr4g 2797	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾)
254	11	oveq2d 7424	. . . . 5 ⊢ (𝜑 → (𝐿 ↾s 𝐹) = (𝐿 ↾s (Base‘𝐾)))
255	253, 254	eqtr3d 2774	. . . 4 ⊢ (𝜑 → 𝐾 = (𝐿 ↾s (Base‘𝐾)))
256	11, 41	eqeltrrd 2834	. . . 4 ⊢ (𝜑 → (Base‘𝐾) ∈ (SubRing‘𝐿))
257		brfldext 32721	. . . . 5 ⊢ ((𝐿 ∈ Field ∧ 𝐾 ∈ Field) → (𝐿/FldExt𝐾 ↔ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))))
258	257	biimpar 478	. . . 4 ⊢ (((𝐿 ∈ Field ∧ 𝐾 ∈ Field) ∧ (𝐾 = (𝐿 ↾s (Base‘𝐾)) ∧ (Base‘𝐾) ∈ (SubRing‘𝐿))) → 𝐿/FldExt𝐾)
259	30, 179, 255, 256, 258	syl22anc 837	. . 3 ⊢ (𝜑 → 𝐿/FldExt𝐾)
260		extdgval 32728	. . 3 ⊢ (𝐿/FldExt𝐾 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
261	259, 260	syl 17	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) = (dim‘((subringAlg ‘𝐿)‘(Base‘𝐾))))
262	13, 252, 261	3eqtr4d 2782	1 ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  {crab 3432  Vcvv 3474   ∪ cun 3946   ⊆ wss 3948  {csn 4628  ∪ cuni 4908   class class class wbr 5148   ↦ cmpt 5231   I cid 5573  ^◡ccnv 5675  dom cdm 5676  ran crn 5677   ↾ cres 5678   “ cima 5679   ∘ ccom 5680  ‘cfv 6543  (class class class)co 7408  [cec 8700   / cqs 8701  Basecbs 17143   ↾_s cress 17172  0_gc0g 17384   /_s cqus 17450  Mndcmnd 18624  SubGrpcsubg 18999  NrmSGrpcnsg 19000   ~_QG cqg 19001   GrpHom cghm 19088  1_rcur 20003  Ringcrg 20055  CRingccrg 20056  opp_rcoppr 20148  Irredcir 20169   RingHom crh 20247  NzRingcnzr 20290  SubRingcsubrg 20314  DivRingcdr 20356  Fieldcfield 20357  SubDRingcsdrg 20401  LSubSpclss 20541   LMHom clmhm 20629   LMIso clmim 20630  LVecclvec 20712  subringAlg csra 20780  LIdealclidl 20782  RSpancrsp 20783  PIDcpid 20897  var₁cv1 21699  Poly₁cpl1 21700   evalSub₁ ces1 21831  idlGen_1pcig1p 25646   fldGen cfldgen 32395  MaxIdealcmxidl 32570  dimcldim 32679  /_FldExtcfldext 32712  [:]cextdg 32715   IntgRing cirng 32742   minPoly cminply 32751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-reg 9586  ax-inf2 9635  ax-ac2 10457  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187  ax-addf 11188  ax-mulf 11189

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7669  df-ofr 7670  df-rpss 7712  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-tpos 8210  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-2o 8466  df-oadd 8469  df-er 8702  df-ec 8704  df-qs 8708  df-map 8821  df-pm 8822  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-sup 9436  df-inf 9437  df-oi 9504  df-r1 9758  df-rank 9759  df-dju 9895  df-card 9933  df-acn 9936  df-ac 10110  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-xnn0 12544  df-z 12558  df-dec 12677  df-uz 12822  df-fz 13484  df-fzo 13627  df-seq 13966  df-hash 14290  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ocomp 17217  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-0g 17386  df-gsum 17387  df-prds 17392  df-pws 17394  df-imas 17453  df-qus 17454  df-mre 17529  df-mrc 17530  df-mri 17531  df-acs 17532  df-proset 18247  df-drs 18248  df-poset 18265  df-ipo 18480  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-mhm 18670  df-submnd 18671  df-grp 18821  df-minusg 18822  df-sbg 18823  df-mulg 18950  df-subg 19002  df-nsg 19003  df-eqg 19004  df-ghm 19089  df-gim 19132  df-cntz 19180  df-oppg 19209  df-lsm 19503  df-cmn 19649  df-abl 19650  df-mgp 19987  df-ur 20004  df-srg 20009  df-ring 20057  df-cring 20058  df-oppr 20149  df-dvdsr 20170  df-unit 20171  df-irred 20172  df-invr 20201  df-dvr 20214  df-rnghom 20250  df-nzr 20291  df-subrg 20316  df-drng 20358  df-field 20359  df-sdrg 20402  df-lmod 20472  df-lss 20542  df-lsp 20582  df-lmhm 20632  df-lmim 20633  df-lbs 20685  df-lvec 20713  df-sra 20784  df-rgmod 20785  df-lidl 20786  df-rsp 20787  df-2idl 20856  df-lpidl 20880  df-lpir 20881  df-rlreg 20898  df-domn 20899  df-idom 20900  df-pid 20901  df-cnfld 20944  df-dsmm 21286  df-frlm 21301  df-uvc 21337  df-lindf 21360  df-linds 21361  df-assa 21407  df-asp 21408  df-ascl 21409  df-psr 21461  df-mvr 21462  df-mpl 21463  df-opsr 21465  df-evls 21634  df-evl 21635  df-psr1 21703  df-vr1 21704  df-ply1 21705  df-coe1 21706  df-evls1 21833  df-evl1 21834  df-mdeg 25569  df-deg1 25570  df-mon1 25647  df-uc1p 25648  df-q1p 25649  df-r1p 25650  df-ig1p 25651  df-fldgen 32396  df-mxidl 32571  df-dim 32680  df-fldext 32716  df-extdg 32717  df-irng 32743  df-minply 32752

This theorem is referenced by: (None)