Theorem algextdeglem8 33902

Description: Lemma for algextdeg 33903. The dimension of the univariate polynomial remainder ring (𝐻 “_s 𝑃) is the degree of the minimal polynomial. (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‘𝑄) ↦ ∪ (𝐺 “ 𝑝))
algextdeglem.r	⊢ 𝑅 = (rem1p‘𝐾)
algextdeglem.h	⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))
algextdeglem.t	⊢ 𝑇 = (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴))))

Assertion

Ref	Expression
algextdeglem8	⊢ (𝜑 → (dim‘(𝐻 “s 𝑃)) = (𝐷‘(𝑀‘𝐴)))

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

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

Proof of Theorem algextdeglem8

Dummy variables 𝑞 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2738	. . . 4 ⊢ (𝜑 → (𝐻 “s 𝑃) = (𝐻 “s 𝑃))
2		algextdeglem.u	. . . . 5 ⊢ 𝑈 = (Base‘𝑃)
3	2	a1i 11	. . . 4 ⊢ (𝜑 → 𝑈 = (Base‘𝑃))
4		algextdeg.e	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
5		algextdeg.k	. . . . . . . . . . . 12 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
6	5	sdrgdrng 20735	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
7	4, 6	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ DivRing)
8	7	drngringd 20682	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
9	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐾 ∈ Ring)
10		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
11		eqid 2737	. . . . . . . . . . 11 ⊢ (0g‘(Poly1‘𝐸)) = (0g‘(Poly1‘𝐸))
12		algextdeg.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ Field)
13		algextdeg.m	. . . . . . . . . . 11 ⊢ 𝑀 = (𝐸 minPoly 𝐹)
14		algextdeg.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
15	5	fveq2i 6845	. . . . . . . . . . 11 ⊢ (Monic1p‘𝐾) = (Monic1p‘(𝐸 ↾s 𝐹))
16	11, 12, 4, 13, 14, 15	minplym1p 33891	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Monic1p‘𝐾))
17	16	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑀‘𝐴) ∈ (Monic1p‘𝐾))
18		eqid 2737	. . . . . . . . . 10 ⊢ (Unic1p‘𝐾) = (Unic1p‘𝐾)
19		eqid 2737	. . . . . . . . . 10 ⊢ (Monic1p‘𝐾) = (Monic1p‘𝐾)
20	18, 19	mon1puc1p 26124	. . . . . . . . 9 ⊢ ((𝐾 ∈ Ring ∧ (𝑀‘𝐴) ∈ (Monic1p‘𝐾)) → (𝑀‘𝐴) ∈ (Unic1p‘𝐾))
21	9, 17, 20	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑀‘𝐴) ∈ (Unic1p‘𝐾))
22		algextdeglem.r	. . . . . . . . 9 ⊢ 𝑅 = (rem1p‘𝐾)
23		algextdeglem.y	. . . . . . . . 9 ⊢ 𝑃 = (Poly1‘𝐾)
24	22, 23, 2, 18	r1pcl 26132	. . . . . . . 8 ⊢ ((𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈)
25	9, 10, 21, 24	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈)
26		eqid 2737	. . . . . . . . . 10 ⊢ (deg1‘𝐾) = (deg1‘𝐾)
27	22, 23, 2, 18, 26	r1pdeglt 26133	. . . . . . . . 9 ⊢ ((𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ (𝑀‘𝐴) ∈ (Unic1p‘𝐾)) → ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < ((deg1‘𝐾)‘(𝑀‘𝐴)))
28	9, 10, 21, 27	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < ((deg1‘𝐾)‘(𝑀‘𝐴)))
29		algextdeg.d	. . . . . . . . . 10 ⊢ 𝐷 = (deg1‘𝐸)
30		algextdeglem.o	. . . . . . . . . . . 12 ⊢ 𝑂 = (𝐸 evalSub1 𝐹)
31	5	fveq2i 6845	. . . . . . . . . . . . 13 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
32	23, 31	eqtri 2760	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
33		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘𝐸) = (Base‘𝐸)
34		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (0g‘𝐸) = (0g‘𝐸)
35	12	fldcrngd 20687	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ CRing)
36		sdrgsubrg 20736	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
37	4, 36	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
38	30, 5, 33, 34, 35, 37	irngssv 33866	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
39	38, 14	sseldd 3936	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
40		eqid 2737	. . . . . . . . . . . 12 ⊢ {𝑝 ∈ dom 𝑂 ∣ ((𝑂‘𝑝)‘𝐴) = (0g‘𝐸)} = {𝑝 ∈ dom 𝑂 ∣ ((𝑂‘𝑝)‘𝐴) = (0g‘𝐸)}
41		eqid 2737	. . . . . . . . . . . 12 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
42		eqid 2737	. . . . . . . . . . . 12 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
43	30, 32, 33, 12, 4, 39, 34, 40, 41, 42, 13	minplycl 33884	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃))
44	43, 2	eleqtrrdi 2848	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
45	5, 29, 23, 2, 44, 37	ressdeg1 33659	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) = ((deg1‘𝐾)‘(𝑀‘𝐴)))
46	45	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝐷‘(𝑀‘𝐴)) = ((deg1‘𝐾)‘(𝑀‘𝐴)))
47	28, 46	breqtrrd 5128	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴)))
48		algextdeglem.t	. . . . . . . . 9 ⊢ 𝑇 = (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴))))
49	12	flddrngd 20686	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
50	49	drngringd 20682	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
51		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
52		eqid 2737	. . . . . . . . . . . . 13 ⊢ (PwSer1‘𝐾) = (PwSer1‘𝐾)
53		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Base‘(PwSer1‘𝐾)) = (Base‘(PwSer1‘𝐾))
54		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly1‘𝐸)) = (Base‘(Poly1‘𝐸))
55	51, 5, 23, 2, 37, 52, 53, 54	ressply1bas2 22180	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
56		inss2 4192	. . . . . . . . . . . 12 ⊢ ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))) ⊆ (Base‘(Poly1‘𝐸))
57	55, 56	eqsstrdi 3980	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘(Poly1‘𝐸)))
58	57, 44	sseldd 3936	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘(Poly1‘𝐸)))
59	11, 12, 4, 13, 14	irngnminplynz 33890	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ≠ (0g‘(Poly1‘𝐸)))
60	29, 51, 11, 54	deg1nn0cl 26061	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Ring ∧ (𝑀‘𝐴) ∈ (Base‘(Poly1‘𝐸)) ∧ (𝑀‘𝐴) ≠ (0g‘(Poly1‘𝐸))) → (𝐷‘(𝑀‘𝐴)) ∈ ℕ0)
61	50, 58, 59, 60	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℕ0)
62	23, 26, 48, 61, 8, 2	ply1degleel 33688	. . . . . . . 8 ⊢ (𝜑 → ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ↔ ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈 ∧ ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴)))))
63	62	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ↔ ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈 ∧ ((deg1‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴)))))
64	25, 47, 63	mpbir2and 714	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇)
65	64	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇)
66		oveq1 7375	. . . . . . . . 9 ⊢ (𝑝 = 𝑞 → (𝑝𝑅(𝑀‘𝐴)) = (𝑞𝑅(𝑀‘𝐴)))
67	66	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑝 = 𝑞 → (𝑞 = (𝑝𝑅(𝑀‘𝐴)) ↔ 𝑞 = (𝑞𝑅(𝑀‘𝐴))))
68		eqcom 2744	. . . . . . . 8 ⊢ (𝑞 = (𝑞𝑅(𝑀‘𝐴)) ↔ (𝑞𝑅(𝑀‘𝐴)) = 𝑞)
69	67, 68	bitrdi 287	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (𝑞 = (𝑝𝑅(𝑀‘𝐴)) ↔ (𝑞𝑅(𝑀‘𝐴)) = 𝑞))
70	23, 26, 48, 61, 8, 2	ply1degltel 33687	. . . . . . . 8 ⊢ (𝜑 → (𝑞 ∈ 𝑇 ↔ (𝑞 ∈ 𝑈 ∧ ((deg1‘𝐾)‘𝑞) ≤ ((𝐷‘(𝑀‘𝐴)) − 1))))
71	70	simprbda 498	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → 𝑞 ∈ 𝑈)
72	70	simplbda 499	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) ≤ ((𝐷‘(𝑀‘𝐴)) − 1))
73	45	oveq1d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘(𝑀‘𝐴)) − 1) = (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1))
74	73	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((𝐷‘(𝑀‘𝐴)) − 1) = (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1))
75	72, 74	breqtrd 5126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) ≤ (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1))
76	26, 23, 2	deg1cl 26056	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝑈 → ((deg1‘𝐾)‘𝑞) ∈ (ℕ0 ∪ {-∞}))
77	71, 76	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) ∈ (ℕ0 ∪ {-∞}))
78	61	nn0zd 12525	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℤ)
79	45, 78	eqeltrrd 2838	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ)
80	79	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ)
81		degltlem1 26045	. . . . . . . . . 10 ⊢ ((((deg1‘𝐾)‘𝑞) ∈ (ℕ0 ∪ {-∞}) ∧ ((deg1‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ) → (((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴)) ↔ ((deg1‘𝐾)‘𝑞) ≤ (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1)))
82	77, 80, 81	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴)) ↔ ((deg1‘𝐾)‘𝑞) ≤ (((deg1‘𝐾)‘(𝑀‘𝐴)) − 1)))
83	75, 82	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴)))
84		fldsdrgfld 20743	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
85	12, 4, 84	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
86	5, 85	eqeltrid 2841	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Field)
87		fldidom 20716	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
88	86, 87	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ IDomn)
89	88	idomdomd 20671	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ Domn)
90	89	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → 𝐾 ∈ Domn)
91	8, 16, 20	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Unic1p‘𝐾))
92	91	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (𝑀‘𝐴) ∈ (Unic1p‘𝐾))
93	23, 2, 18, 22, 26, 90, 71, 92	r1pid2 26135	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((𝑞𝑅(𝑀‘𝐴)) = 𝑞 ↔ ((deg1‘𝐾)‘𝑞) < ((deg1‘𝐾)‘(𝑀‘𝐴))))
94	83, 93	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (𝑞𝑅(𝑀‘𝐴)) = 𝑞)
95	69, 71, 94	rspcedvdw 3581	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴)))
96	95	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ 𝑇 ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴)))
97		algextdeglem.h	. . . . . 6 ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))
98	97	fompt 7072	. . . . 5 ⊢ (𝐻:𝑈–onto→𝑇 ↔ (∀𝑝 ∈ 𝑈 (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ∧ ∀𝑞 ∈ 𝑇 ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴))))
99	65, 96, 98	sylanbrc 584	. . . 4 ⊢ (𝜑 → 𝐻:𝑈–onto→𝑇)
100	23	ply1ring 22200	. . . . 5 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
101	8, 100	syl 17	. . . 4 ⊢ (𝜑 → 𝑃 ∈ Ring)
102	1, 3, 99, 101	imasbas 17445	. . 3 ⊢ (𝜑 → 𝑇 = (Base‘(𝐻 “s 𝑃)))
103	71	ex 412	. . . . 5 ⊢ (𝜑 → (𝑞 ∈ 𝑇 → 𝑞 ∈ 𝑈))
104	103	ssrdv 3941	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ 𝑈)
105		eqid 2737	. . . . 5 ⊢ (𝑃 ↾s 𝑇) = (𝑃 ↾s 𝑇)
106	105, 2	ressbas2 17177	. . . 4 ⊢ (𝑇 ⊆ 𝑈 → 𝑇 = (Base‘(𝑃 ↾s 𝑇)))
107	104, 106	syl 17	. . 3 ⊢ (𝜑 → 𝑇 = (Base‘(𝑃 ↾s 𝑇)))
108		ssidd 3959	. . 3 ⊢ (𝜑 → 𝑇 ⊆ 𝑇)
109		eqid 2737	. . . . . . 7 ⊢ (𝐻 “s 𝑃) = (𝐻 “s 𝑃)
110		eqid 2737	. . . . . . 7 ⊢ (Base‘(𝐻 “s 𝑃)) = (Base‘(𝐻 “s 𝑃))
111	104	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑇 ⊆ 𝑈)
112		simplr 769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑥 ∈ 𝑇)
113	111, 112	sseldd 3936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑥 ∈ 𝑈)
114		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑇)
115	111, 114	sseldd 3936	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑈)
116		foeq3 6752	. . . . . . . . . 10 ⊢ (𝑇 = (Base‘(𝐻 “s 𝑃)) → (𝐻:𝑈–onto→𝑇 ↔ 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃))))
117	102, 116	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐻:𝑈–onto→𝑇 ↔ 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃))))
118	99, 117	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃)))
119	118	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃)))
120	23, 2, 22, 18, 97, 8, 91	r1plmhm 33703	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ (𝑃 LMHom (𝐻 “s 𝑃)))
121	120	lmhmghmd 33130	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ (𝑃 GrpHom (𝐻 “s 𝑃)))
122		ghmmhm 19167	. . . . . . . . 9 ⊢ (𝐻 ∈ (𝑃 GrpHom (𝐻 “s 𝑃)) → 𝐻 ∈ (𝑃 MndHom (𝐻 “s 𝑃)))
123	121, 122	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ (𝑃 MndHom (𝐻 “s 𝑃)))
124	123	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐻 ∈ (𝑃 MndHom (𝐻 “s 𝑃)))
125		eqid 2737	. . . . . . 7 ⊢ (+g‘𝑃) = (+g‘𝑃)
126		eqid 2737	. . . . . . 7 ⊢ (+g‘(𝐻 “s 𝑃)) = (+g‘(𝐻 “s 𝑃))
127	109, 2, 110, 113, 115, 119, 124, 125, 126	mhmimasplusg 33131	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝐻‘𝑥)(+g‘(𝐻 “s 𝑃))(𝐻‘𝑦)) = (𝐻‘(𝑥(+g‘𝑃)𝑦)))
128		algextdeg.l	. . . . . . . . 9 ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴})))
129	12	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐸 ∈ Field)
130	4	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐹 ∈ (SubDRing‘𝐸))
131	14	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐴 ∈ (𝐸 IntgRing 𝐹))
132		algextdeglem.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
133		algextdeglem.n	. . . . . . . . 9 ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍))
134		algextdeglem.z	. . . . . . . . 9 ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)})
135		algextdeglem.q	. . . . . . . . 9 ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍))
136		algextdeglem.j	. . . . . . . . 9 ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))
137	5, 128, 29, 13, 129, 130, 131, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 113	algextdeglem7 33901	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥 ∈ 𝑇 ↔ (𝐻‘𝑥) = 𝑥))
138	112, 137	mpbid 232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘𝑥) = 𝑥)
139	5, 128, 29, 13, 129, 130, 131, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 115	algextdeglem7 33901	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑦 ∈ 𝑇 ↔ (𝐻‘𝑦) = 𝑦))
140	114, 139	mpbid 232	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘𝑦) = 𝑦)
141	138, 140	oveq12d 7386	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝐻‘𝑥)(+g‘(𝐻 “s 𝑃))(𝐻‘𝑦)) = (𝑥(+g‘(𝐻 “s 𝑃))𝑦))
142	101	ringgrpd 20189	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
143	23, 7	ply1lvec 33652	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
144	23, 26, 48, 61, 8	ply1degltlss 33689	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ (LSubSp‘𝑃))
145		eqid 2737	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
146	105, 145	lsslvec 21073	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ LVec ∧ 𝑇 ∈ (LSubSp‘𝑃)) → (𝑃 ↾s 𝑇) ∈ LVec)
147	143, 144, 146	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 ↾s 𝑇) ∈ LVec)
148	147	lvecgrpd 21072	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 ↾s 𝑇) ∈ Grp)
149	2	issubg 19068	. . . . . . . . . 10 ⊢ (𝑇 ∈ (SubGrp‘𝑃) ↔ (𝑃 ∈ Grp ∧ 𝑇 ⊆ 𝑈 ∧ (𝑃 ↾s 𝑇) ∈ Grp))
150	142, 104, 148, 149	syl3anbrc 1345	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝑃))
151	150	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑇 ∈ (SubGrp‘𝑃))
152	125	subgcl 19078	. . . . . . . 8 ⊢ ((𝑇 ∈ (SubGrp‘𝑃) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘𝑃)𝑦) ∈ 𝑇)
153	151, 112, 114, 152	syl3anc 1374	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘𝑃)𝑦) ∈ 𝑇)
154	142	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑃 ∈ Grp)
155	2, 125, 154, 113, 115	grpcld 18889	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘𝑃)𝑦) ∈ 𝑈)
156	5, 128, 29, 13, 129, 130, 131, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 155	algextdeglem7 33901	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝑥(+g‘𝑃)𝑦) ∈ 𝑇 ↔ (𝐻‘(𝑥(+g‘𝑃)𝑦)) = (𝑥(+g‘𝑃)𝑦)))
157	153, 156	mpbid 232	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘(𝑥(+g‘𝑃)𝑦)) = (𝑥(+g‘𝑃)𝑦))
158	127, 141, 157	3eqtr3d 2780	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘(𝐻 “s 𝑃))𝑦) = (𝑥(+g‘𝑃)𝑦))
159		fvex 6855	. . . . . . . . 9 ⊢ (deg1‘𝐾) ∈ V
160		cnvexg 7876	. . . . . . . . 9 ⊢ ((deg1‘𝐾) ∈ V → ◡(deg1‘𝐾) ∈ V)
161		imaexg 7865	. . . . . . . . 9 ⊢ (◡(deg1‘𝐾) ∈ V → (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ∈ V)
162	159, 160, 161	mp2b 10	. . . . . . . 8 ⊢ (◡(deg1‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ∈ V
163	48, 162	eqeltri 2833	. . . . . . 7 ⊢ 𝑇 ∈ V
164	105, 125	ressplusg 17223	. . . . . . 7 ⊢ (𝑇 ∈ V → (+g‘𝑃) = (+g‘(𝑃 ↾s 𝑇)))
165	163, 164	ax-mp 5	. . . . . 6 ⊢ (+g‘𝑃) = (+g‘(𝑃 ↾s 𝑇))
166	165	oveqi 7381	. . . . 5 ⊢ (𝑥(+g‘𝑃)𝑦) = (𝑥(+g‘(𝑃 ↾s 𝑇))𝑦)
167	158, 166	eqtrdi 2788	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+g‘(𝐻 “s 𝑃))𝑦) = (𝑥(+g‘(𝑃 ↾s 𝑇))𝑦))
168	167	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥(+g‘(𝐻 “s 𝑃))𝑦) = (𝑥(+g‘(𝑃 ↾s 𝑇))𝑦))
169		simprr 773	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑦 ∈ 𝑇)
170	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐸 ∈ Field)
171	4	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐹 ∈ (SubDRing‘𝐸))
172	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐴 ∈ (𝐸 IntgRing 𝐹))
173	104	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑇 ⊆ 𝑈)
174	173, 169	sseldd 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑦 ∈ 𝑈)
175	5, 128, 29, 13, 170, 171, 172, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 174	algextdeglem7 33901	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑦 ∈ 𝑇 ↔ (𝐻‘𝑦) = 𝑦))
176	169, 175	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘𝑦) = 𝑦)
177	176	oveq2d 7384	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘(𝐻 “s 𝑃))(𝐻‘𝑦)) = (𝑥( ·𝑠 ‘(𝐻 “s 𝑃))𝑦))
178		simprl 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑥 ∈ 𝐹)
179	33	sdrgss 20738	. . . . . . . . . 10 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
180	5, 33	ressbas2 17177	. . . . . . . . . 10 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
181	4, 179, 180	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
182	23	ply1sca 22205	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Ring → 𝐾 = (Scalar‘𝑃))
183	8, 182	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 = (Scalar‘𝑃))
184	183	fveq2d 6846	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝑃)))
185	181, 184	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(Scalar‘𝑃)))
186	185	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐹 = (Base‘(Scalar‘𝑃)))
187	178, 186	eleqtrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑥 ∈ (Base‘(Scalar‘𝑃)))
188	118	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻:𝑈–onto→(Base‘(𝐻 “s 𝑃)))
189	120	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻 ∈ (𝑃 LMHom (𝐻 “s 𝑃)))
190		eqid 2737	. . . . . 6 ⊢ ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘𝑃)
191		eqid 2737	. . . . . 6 ⊢ ( ·𝑠 ‘(𝐻 “s 𝑃)) = ( ·𝑠 ‘(𝐻 “s 𝑃))
192		eqid 2737	. . . . . 6 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
193	109, 2, 110, 187, 174, 188, 189, 190, 191, 192	lmhmimasvsca 33132	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘(𝐻 “s 𝑃))(𝐻‘𝑦)) = (𝐻‘(𝑥( ·𝑠 ‘𝑃)𝑦)))
194	177, 193	eqtr3d 2774	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘(𝐻 “s 𝑃))𝑦) = (𝐻‘(𝑥( ·𝑠 ‘𝑃)𝑦)))
195	64, 97	fmptd 7068	. . . . . 6 ⊢ (𝜑 → 𝐻:𝑈⟶𝑇)
196	195	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻:𝑈⟶𝑇)
197		eqid 2737	. . . . . 6 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
198	143	lveclmodd 21071	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ LMod)
199	198	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑃 ∈ LMod)
200	2, 197, 190, 192, 199, 187, 174	lmodvscld 20842	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘𝑃)𝑦) ∈ 𝑈)
201	196, 200	ffvelcdmd 7039	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘(𝑥( ·𝑠 ‘𝑃)𝑦)) ∈ 𝑇)
202	194, 201	eqeltrd 2837	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘(𝐻 “s 𝑃))𝑦) ∈ 𝑇)
203	144	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑇 ∈ (LSubSp‘𝑃))
204	197, 190, 192, 145	lssvscl 20918	. . . . . 6 ⊢ (((𝑃 ∈ LMod ∧ 𝑇 ∈ (LSubSp‘𝑃)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘𝑃)𝑦) ∈ 𝑇)
205	199, 203, 187, 169, 204	syl22anc 839	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘𝑃)𝑦) ∈ 𝑇)
206	5, 128, 29, 13, 170, 171, 172, 30, 23, 2, 132, 133, 134, 135, 136, 22, 97, 48, 200	algextdeglem7 33901	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → ((𝑥( ·𝑠 ‘𝑃)𝑦) ∈ 𝑇 ↔ (𝐻‘(𝑥( ·𝑠 ‘𝑃)𝑦)) = (𝑥( ·𝑠 ‘𝑃)𝑦)))
207	205, 206	mpbid 232	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘(𝑥( ·𝑠 ‘𝑃)𝑦)) = (𝑥( ·𝑠 ‘𝑃)𝑦))
208	105, 190	ressvsca 17276	. . . . . 6 ⊢ (𝑇 ∈ V → ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘(𝑃 ↾s 𝑇)))
209	163, 208	mp1i 13	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘(𝑃 ↾s 𝑇)))
210	209	oveqd 7385	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘𝑃)𝑦) = (𝑥( ·𝑠 ‘(𝑃 ↾s 𝑇))𝑦))
211	194, 207, 210	3eqtrd 2776	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·𝑠 ‘(𝐻 “s 𝑃))𝑦) = (𝑥( ·𝑠 ‘(𝑃 ↾s 𝑇))𝑦))
212		eqid 2737	. . 3 ⊢ (Scalar‘(𝐻 “s 𝑃)) = (Scalar‘(𝐻 “s 𝑃))
213	105, 197	resssca 17275	. . . 4 ⊢ (𝑇 ∈ V → (Scalar‘𝑃) = (Scalar‘(𝑃 ↾s 𝑇)))
214	163, 213	ax-mp 5	. . 3 ⊢ (Scalar‘𝑃) = (Scalar‘(𝑃 ↾s 𝑇))
215	1, 3, 99, 101, 197	imassca 17452	. . . . . 6 ⊢ (𝜑 → (Scalar‘𝑃) = (Scalar‘(𝐻 “s 𝑃)))
216	183, 215	eqtrd 2772	. . . . 5 ⊢ (𝜑 → 𝐾 = (Scalar‘(𝐻 “s 𝑃)))
217	216	fveq2d 6846	. . . 4 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(𝐻 “s 𝑃))))
218	181, 217	eqtrd 2772	. . 3 ⊢ (𝜑 → 𝐹 = (Base‘(Scalar‘(𝐻 “s 𝑃))))
219	215	fveq2d 6846	. . . . . 6 ⊢ (𝜑 → (+g‘(Scalar‘𝑃)) = (+g‘(Scalar‘(𝐻 “s 𝑃))))
220	219	oveqd 7385	. . . . 5 ⊢ (𝜑 → (𝑥(+g‘(Scalar‘𝑃))𝑦) = (𝑥(+g‘(Scalar‘(𝐻 “s 𝑃)))𝑦))
221	220	eqcomd 2743	. . . 4 ⊢ (𝜑 → (𝑥(+g‘(Scalar‘(𝐻 “s 𝑃)))𝑦) = (𝑥(+g‘(Scalar‘𝑃))𝑦))
222	221	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥(+g‘(Scalar‘(𝐻 “s 𝑃)))𝑦) = (𝑥(+g‘(Scalar‘𝑃))𝑦))
223		lmhmlvec2 33797	. . . 4 ⊢ ((𝑃 ∈ LVec ∧ 𝐻 ∈ (𝑃 LMHom (𝐻 “s 𝑃))) → (𝐻 “s 𝑃) ∈ LVec)
224	143, 120, 223	syl2anc 585	. . 3 ⊢ (𝜑 → (𝐻 “s 𝑃) ∈ LVec)
225	102, 107, 108, 168, 202, 211, 212, 214, 218, 185, 222, 224, 147	dimpropd 33786	. 2 ⊢ (𝜑 → (dim‘(𝐻 “s 𝑃)) = (dim‘(𝑃 ↾s 𝑇)))
226	23, 26, 48, 61, 7, 105	ply1degltdim 33801	. 2 ⊢ (𝜑 → (dim‘(𝑃 ↾s 𝑇)) = (𝐷‘(𝑀‘𝐴)))
227	225, 226	eqtrd 2772	1 ⊢ (𝜑 → (dim‘(𝐻 “s 𝑃)) = (𝐷‘(𝑀‘𝐴)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  {csn 4582  ∪ cuni 4865   class class class wbr 5100   ↦ cmpt 5181  ^◡ccnv 5631  dom cdm 5632   “ cima 5635  ⟶wf 6496  –onto→wfo 6498  ‘cfv 6500  (class class class)co 7368  [cec 8643  1c1 11039  -∞cmnf 11176   < clt 11178   ≤ cle 11179   − cmin 11376  ℕ₀cn0 12413  ℤcz 12500  [,)cico 13275  Basecbs 17148   ↾_s cress 17169  +_gcplusg 17189  Scalarcsca 17192   ·_𝑠 cvsca 17193  0_gc0g 17371   “_s cimas 17437   /_s cqus 17438   MndHom cmhm 18718  Grpcgrp 18875  SubGrpcsubg 19062   ~_QG cqg 19064   GrpHom cghm 19153  Ringcrg 20180  SubRingcsubrg 20514  Domncdomn 20637  IDomncidom 20638  DivRingcdr 20674  Fieldcfield 20675  SubDRingcsdrg 20731  LModclmod 20823  LSubSpclss 20894   LMHom clmhm 20983  LVecclvec 21066  RSpancrsp 21174  PwSer₁cps1 22127  Poly₁cpl1 22129   evalSub₁ ces1 22269  deg₁cdg1 26027  Monic_1pcmn1 26099  Unic_1pcuc1p 26100  rem_1pcr1p 26102  idlGen_1pcig1p 26103   fldGen cfldgen 33404  dimcldim 33776   IntgRing cirng 33861   minPoly cminply 33877

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-reg 9509  ax-inf2 9562  ax-ac2 10385  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-ofr 7633  df-rpss 7678  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-tpos 8178  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-oadd 8411  df-er 8645  df-map 8777  df-pm 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-sup 9357  df-inf 9358  df-oi 9427  df-r1 9688  df-rank 9689  df-dju 9825  df-card 9863  df-acn 9866  df-ac 10038  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-ico 13279  df-fz 13436  df-fzo 13583  df-seq 13937  df-hash 14266  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ocomp 17210  df-ds 17211  df-unif 17212  df-hom 17213  df-cco 17214  df-0g 17373  df-gsum 17374  df-prds 17379  df-pws 17381  df-imas 17441  df-mre 17517  df-mrc 17518  df-mri 17519  df-acs 17520  df-proset 18229  df-drs 18230  df-poset 18248  df-ipo 18463  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-grp 18878  df-minusg 18879  df-sbg 18880  df-mulg 19010  df-subg 19065  df-ghm 19154  df-cntz 19258  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-srg 20134  df-ring 20182  df-cring 20183  df-oppr 20285  df-dvdsr 20305  df-unit 20306  df-invr 20336  df-rhm 20420  df-nzr 20458  df-subrng 20491  df-subrg 20515  df-rlreg 20639  df-domn 20640  df-idom 20641  df-drng 20676  df-field 20677  df-sdrg 20732  df-lmod 20825  df-lss 20895  df-lsp 20935  df-lmhm 20986  df-lbs 21039  df-lvec 21067  df-sra 21137  df-rgmod 21138  df-lidl 21175  df-rsp 21176  df-cnfld 21322  df-dsmm 21699  df-frlm 21714  df-uvc 21750  df-lindf 21773  df-linds 21774  df-assa 21820  df-asp 21821  df-ascl 21822  df-psr 21877  df-mvr 21878  df-mpl 21879  df-opsr 21881  df-evls 22041  df-evl 22042  df-psr1 22132  df-vr1 22133  df-ply1 22134  df-coe1 22135  df-evls1 22271  df-evl1 22272  df-mdeg 26028  df-deg1 26029  df-mon1 26104  df-uc1p 26105  df-q1p 26106  df-r1p 26107  df-ig1p 26108  df-dim 33777  df-irng 33862  df-minply 33878

This theorem is referenced by:  algextdeg  33903