algextdeglem8 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > algextdeglem8		Structured version Visualization version GIF version

Theorem algextdeglem8 33069

Description: Lemma for algextdeg 33070. (Contributed by Thierry Arnoux, 2-Apr-2025.)

**Hypotheses**
Ref	Expression
algextdeg.k	⊢ 𝐾 = (𝐸 ↾_s 𝐹)
algextdeg.l	⊢ 𝐿 = (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴})))
algextdeg.d	⊢ 𝐷 = ( deg₁ ‘𝐸)
algextdeg.m	⊢ 𝑀 = (𝐸 minPoly 𝐹)
algextdeg.f	⊢ (𝜑 → 𝐸 ∈ Field)
algextdeg.e	⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
algextdeg.a	⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
algextdeglem.o	⊢ 𝑂 = (𝐸 evalSub₁ 𝐹)
algextdeglem.y	⊢ 𝑃 = (Poly₁‘𝐾)
algextdeglem.u	⊢ 𝑈 = (Base‘𝑃)
algextdeglem.g	⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
algextdeglem.n	⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~_QG 𝑍))
algextdeglem.z	⊢ 𝑍 = (^◡𝐺 “ {(0_g‘𝐿)})
algextdeglem.q	⊢ 𝑄 = (𝑃 /_s (𝑃 ~_QG 𝑍))
algextdeglem.j	⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))
algextdeglem.r	⊢ 𝑅 = (rem_1p‘𝐾)
algextdeglem.h	⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))
algextdeglem.t	⊢ 𝑇 = (^◡( deg₁ ‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴))))

**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 2731	. . . 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 20549	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐾 ∈ DivRing)
7	4, 6	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ DivRing)
8	7	drngringd 20508	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Ring)
9	8	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝐾 ∈ Ring)
10		simpr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈)
11		eqid 2730	. . . . . . . . . . 11 ⊢ (0_g‘(Poly₁‘𝐸)) = (0_g‘(Poly₁‘𝐸))
12		algextdeg.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ Field)
13		algextdeg.m	. . . . . . . . . . 11 ⊢ 𝑀 = (𝐸 minPoly 𝐹)
14		algextdeg.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹))
15	5	fveq2i 6893	. . . . . . . . . . 11 ⊢ (Monic_1p‘𝐾) = (Monic_1p‘(𝐸 ↾_s 𝐹))
16	11, 12, 4, 13, 14, 15	minplym1p 33061	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Monic_1p‘𝐾))
17	16	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑀‘𝐴) ∈ (Monic_1p‘𝐾))
18		eqid 2730	. . . . . . . . . 10 ⊢ (Unic_1p‘𝐾) = (Unic_1p‘𝐾)
19		eqid 2730	. . . . . . . . . 10 ⊢ (Monic_1p‘𝐾) = (Monic_1p‘𝐾)
20	18, 19	mon1puc1p 25903	. . . . . . . . 9 ⊢ ((𝐾 ∈ Ring ∧ (𝑀‘𝐴) ∈ (Monic_1p‘𝐾)) → (𝑀‘𝐴) ∈ (Unic_1p‘𝐾))
21	9, 17, 20	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑀‘𝐴) ∈ (Unic_1p‘𝐾))
22		algextdeglem.r	. . . . . . . . 9 ⊢ 𝑅 = (rem_1p‘𝐾)
23		algextdeglem.y	. . . . . . . . 9 ⊢ 𝑃 = (Poly₁‘𝐾)
24	22, 23, 2, 18	r1pcl 25910	. . . . . . . 8 ⊢ ((𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ (𝑀‘𝐴) ∈ (Unic_1p‘𝐾)) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈)
25	9, 10, 21, 24	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈)
26		eqid 2730	. . . . . . . . . 10 ⊢ ( deg₁ ‘𝐾) = ( deg₁ ‘𝐾)
27	22, 23, 2, 18, 26	r1pdeglt 25911	. . . . . . . . 9 ⊢ ((𝐾 ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ (𝑀‘𝐴) ∈ (Unic_1p‘𝐾)) → (( deg₁ ‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (( deg₁ ‘𝐾)‘(𝑀‘𝐴)))
28	9, 10, 21, 27	syl3anc 1369	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (( deg₁ ‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (( deg₁ ‘𝐾)‘(𝑀‘𝐴)))
29		algextdeg.d	. . . . . . . . . 10 ⊢ 𝐷 = ( deg₁ ‘𝐸)
30		algextdeglem.o	. . . . . . . . . . . 12 ⊢ 𝑂 = (𝐸 evalSub₁ 𝐹)
31	5	fveq2i 6893	. . . . . . . . . . . . 13 ⊢ (Poly₁‘𝐾) = (Poly₁‘(𝐸 ↾_s 𝐹))
32	23, 31	eqtri 2758	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly₁‘(𝐸 ↾_s 𝐹))
33		eqid 2730	. . . . . . . . . . . 12 ⊢ (Base‘𝐸) = (Base‘𝐸)
34		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
35	12	fldcrngd 20513	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ CRing)
36		sdrgsubrg 20550	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
37	4, 36	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
38	30, 5, 33, 34, 35, 37	irngssv 33041	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸))
39	38, 14	sseldd 3982	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸))
40		eqid 2730	. . . . . . . . . . . 12 ⊢ {𝑝 ∈ dom 𝑂 ∣ ((𝑂‘𝑝)‘𝐴) = (0_g‘𝐸)} = {𝑝 ∈ dom 𝑂 ∣ ((𝑂‘𝑝)‘𝐴) = (0_g‘𝐸)}
41		eqid 2730	. . . . . . . . . . . 12 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
42		eqid 2730	. . . . . . . . . . . 12 ⊢ (idlGen_1p‘(𝐸 ↾_s 𝐹)) = (idlGen_1p‘(𝐸 ↾_s 𝐹))
43	30, 32, 33, 12, 4, 39, 34, 40, 41, 42, 13	minplycl 33056	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃))
44	43, 2	eleqtrrdi 2842	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈)
45	5, 29, 23, 2, 44, 37	ressdeg1 32925	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) = (( deg₁ ‘𝐾)‘(𝑀‘𝐴)))
46	45	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝐷‘(𝑀‘𝐴)) = (( deg₁ ‘𝐾)‘(𝑀‘𝐴)))
47	28, 46	breqtrrd 5175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (( deg₁ ‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴)))
48		algextdeglem.t	. . . . . . . . 9 ⊢ 𝑇 = (^◡( deg₁ ‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴))))
49	12	flddrngd 20512	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
50	49	drngringd 20508	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ Ring)
51		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Poly₁‘𝐸) = (Poly₁‘𝐸)
52		eqid 2730	. . . . . . . . . . . . 13 ⊢ (PwSer₁‘𝐾) = (PwSer₁‘𝐾)
53		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Base‘(PwSer₁‘𝐾)) = (Base‘(PwSer₁‘𝐾))
54		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Base‘(Poly₁‘𝐸)) = (Base‘(Poly₁‘𝐸))
55	51, 5, 23, 2, 37, 52, 53, 54	ressply1bas2 21970	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = ((Base‘(PwSer₁‘𝐾)) ∩ (Base‘(Poly₁‘𝐸))))
56		inss2 4228	. . . . . . . . . . . 12 ⊢ ((Base‘(PwSer₁‘𝐾)) ∩ (Base‘(Poly₁‘𝐸))) ⊆ (Base‘(Poly₁‘𝐸))
57	55, 56	eqsstrdi 4035	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ (Base‘(Poly₁‘𝐸)))
58	57, 44	sseldd 3982	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘(Poly₁‘𝐸)))
59	11, 12, 4, 13, 14	irngnminplynz 33060	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ≠ (0_g‘(Poly₁‘𝐸)))
60	29, 51, 11, 54	deg1nn0cl 25841	. . . . . . . . . 10 ⊢ ((𝐸 ∈ Ring ∧ (𝑀‘𝐴) ∈ (Base‘(Poly₁‘𝐸)) ∧ (𝑀‘𝐴) ≠ (0_g‘(Poly₁‘𝐸))) → (𝐷‘(𝑀‘𝐴)) ∈ ℕ₀)
61	50, 58, 59, 60	syl3anc 1369	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℕ₀)
62	23, 26, 48, 61, 8, 2	ply1degleel 32941	. . . . . . . 8 ⊢ (𝜑 → ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ↔ ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈 ∧ (( deg₁ ‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴)))))
63	62	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ↔ ((𝑝𝑅(𝑀‘𝐴)) ∈ 𝑈 ∧ (( deg₁ ‘𝐾)‘(𝑝𝑅(𝑀‘𝐴))) < (𝐷‘(𝑀‘𝐴)))))
64	25, 47, 63	mpbir2and 709	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑈) → (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇)
65	64	ralrimiva 3144	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ 𝑈 (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇)
66		oveq1 7418	. . . . . . . . 9 ⊢ (𝑝 = 𝑞 → (𝑝𝑅(𝑀‘𝐴)) = (𝑞𝑅(𝑀‘𝐴)))
67	66	eqeq2d 2741	. . . . . . . 8 ⊢ (𝑝 = 𝑞 → (𝑞 = (𝑝𝑅(𝑀‘𝐴)) ↔ 𝑞 = (𝑞𝑅(𝑀‘𝐴))))
68		eqcom 2737	. . . . . . . 8 ⊢ (𝑞 = (𝑞𝑅(𝑀‘𝐴)) ↔ (𝑞𝑅(𝑀‘𝐴)) = 𝑞)
69	67, 68	bitrdi 286	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (𝑞 = (𝑝𝑅(𝑀‘𝐴)) ↔ (𝑞𝑅(𝑀‘𝐴)) = 𝑞))
70	23, 26, 48, 61, 8, 2	ply1degltel 32940	. . . . . . . 8 ⊢ (𝜑 → (𝑞 ∈ 𝑇 ↔ (𝑞 ∈ 𝑈 ∧ (( deg₁ ‘𝐾)‘𝑞) ≤ ((𝐷‘(𝑀‘𝐴)) − 1))))
71	70	simprbda 497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → 𝑞 ∈ 𝑈)
72	70	simplbda 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (( deg₁ ‘𝐾)‘𝑞) ≤ ((𝐷‘(𝑀‘𝐴)) − 1))
73	45	oveq1d 7426	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘(𝑀‘𝐴)) − 1) = ((( deg₁ ‘𝐾)‘(𝑀‘𝐴)) − 1))
74	73	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((𝐷‘(𝑀‘𝐴)) − 1) = ((( deg₁ ‘𝐾)‘(𝑀‘𝐴)) − 1))
75	72, 74	breqtrd 5173	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (( deg₁ ‘𝐾)‘𝑞) ≤ ((( deg₁ ‘𝐾)‘(𝑀‘𝐴)) − 1))
76	26, 23, 2	deg1cl 25836	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝑈 → (( deg₁ ‘𝐾)‘𝑞) ∈ (ℕ₀ ∪ {-∞}))
77	71, 76	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (( deg₁ ‘𝐾)‘𝑞) ∈ (ℕ₀ ∪ {-∞}))
78	61	nn0zd 12588	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ∈ ℤ)
79	45, 78	eqeltrrd 2832	. . . . . . . . . . 11 ⊢ (𝜑 → (( deg₁ ‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ)
80	79	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (( deg₁ ‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ)
81		degltlem1 25825	. . . . . . . . . 10 ⊢ (((( deg₁ ‘𝐾)‘𝑞) ∈ (ℕ₀ ∪ {-∞}) ∧ (( deg₁ ‘𝐾)‘(𝑀‘𝐴)) ∈ ℤ) → ((( deg₁ ‘𝐾)‘𝑞) < (( deg₁ ‘𝐾)‘(𝑀‘𝐴)) ↔ (( deg₁ ‘𝐾)‘𝑞) ≤ ((( deg₁ ‘𝐾)‘(𝑀‘𝐴)) − 1)))
82	77, 80, 81	syl2anc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((( deg₁ ‘𝐾)‘𝑞) < (( deg₁ ‘𝐾)‘(𝑀‘𝐴)) ↔ (( deg₁ ‘𝐾)‘𝑞) ≤ ((( deg₁ ‘𝐾)‘(𝑀‘𝐴)) − 1)))
83	75, 82	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (( deg₁ ‘𝐾)‘𝑞) < (( deg₁ ‘𝐾)‘(𝑀‘𝐴)))
84		fldsdrgfld 20557	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾_s 𝐹) ∈ Field)
85	12, 4, 84	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ↾_s 𝐹) ∈ Field)
86	5, 85	eqeltrid 2835	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ Field)
87		fldidom 21123	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Field → 𝐾 ∈ IDomn)
88	86, 87	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ IDomn)
89	88	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → 𝐾 ∈ IDomn)
90	8, 16, 20	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Unic_1p‘𝐾))
91	90	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (𝑀‘𝐴) ∈ (Unic_1p‘𝐾))
92	23, 2, 18, 22, 89, 26, 71, 91	r1pid2 32954	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ((𝑞𝑅(𝑀‘𝐴)) = 𝑞 ↔ (( deg₁ ‘𝐾)‘𝑞) < (( deg₁ ‘𝐾)‘(𝑀‘𝐴))))
93	83, 92	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → (𝑞𝑅(𝑀‘𝐴)) = 𝑞)
94	69, 71, 93	rspcedvdw 3614	. . . . . 6 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑇) → ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴)))
95	94	ralrimiva 3144	. . . . 5 ⊢ (𝜑 → ∀𝑞 ∈ 𝑇 ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴)))
96		algextdeglem.h	. . . . . 6 ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴)))
97	96	fompt 7118	. . . . 5 ⊢ (𝐻:𝑈–onto→𝑇 ↔ (∀𝑝 ∈ 𝑈 (𝑝𝑅(𝑀‘𝐴)) ∈ 𝑇 ∧ ∀𝑞 ∈ 𝑇 ∃𝑝 ∈ 𝑈 𝑞 = (𝑝𝑅(𝑀‘𝐴))))
98	65, 95, 97	sylanbrc 581	. . . 4 ⊢ (𝜑 → 𝐻:𝑈–onto→𝑇)
99	23	ply1ring 21990	. . . . 5 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
100	8, 99	syl 17	. . . 4 ⊢ (𝜑 → 𝑃 ∈ Ring)
101	1, 3, 98, 100	imasbas 17462	. . 3 ⊢ (𝜑 → 𝑇 = (Base‘(𝐻 “_s 𝑃)))
102	71	ex 411	. . . . 5 ⊢ (𝜑 → (𝑞 ∈ 𝑇 → 𝑞 ∈ 𝑈))
103	102	ssrdv 3987	. . . 4 ⊢ (𝜑 → 𝑇 ⊆ 𝑈)
104		eqid 2730	. . . . 5 ⊢ (𝑃 ↾_s 𝑇) = (𝑃 ↾_s 𝑇)
105	104, 2	ressbas2 17186	. . . 4 ⊢ (𝑇 ⊆ 𝑈 → 𝑇 = (Base‘(𝑃 ↾_s 𝑇)))
106	103, 105	syl 17	. . 3 ⊢ (𝜑 → 𝑇 = (Base‘(𝑃 ↾_s 𝑇)))
107		ssidd 4004	. . 3 ⊢ (𝜑 → 𝑇 ⊆ 𝑇)
108		eqid 2730	. . . . . . 7 ⊢ (𝐻 “_s 𝑃) = (𝐻 “_s 𝑃)
109		eqid 2730	. . . . . . 7 ⊢ (Base‘(𝐻 “_s 𝑃)) = (Base‘(𝐻 “_s 𝑃))
110	103	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑇 ⊆ 𝑈)
111		simplr 765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑥 ∈ 𝑇)
112	110, 111	sseldd 3982	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑥 ∈ 𝑈)
113		simpr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑇)
114	110, 113	sseldd 3982	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑈)
115		foeq3 6802	. . . . . . . . . 10 ⊢ (𝑇 = (Base‘(𝐻 “_s 𝑃)) → (𝐻:𝑈–onto→𝑇 ↔ 𝐻:𝑈–onto→(Base‘(𝐻 “_s 𝑃))))
116	101, 115	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐻:𝑈–onto→𝑇 ↔ 𝐻:𝑈–onto→(Base‘(𝐻 “_s 𝑃))))
117	98, 116	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → 𝐻:𝑈–onto→(Base‘(𝐻 “_s 𝑃)))
118	117	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐻:𝑈–onto→(Base‘(𝐻 “_s 𝑃)))
119	23, 2, 22, 18, 96, 8, 90	r1plmhm 32955	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ (𝑃 LMHom (𝐻 “_s 𝑃)))
120	119	lmhmghmd 32465	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ (𝑃 GrpHom (𝐻 “_s 𝑃)))
121		ghmmhm 19140	. . . . . . . . 9 ⊢ (𝐻 ∈ (𝑃 GrpHom (𝐻 “_s 𝑃)) → 𝐻 ∈ (𝑃 MndHom (𝐻 “_s 𝑃)))
122	120, 121	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ (𝑃 MndHom (𝐻 “_s 𝑃)))
123	122	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐻 ∈ (𝑃 MndHom (𝐻 “_s 𝑃)))
124		eqid 2730	. . . . . . 7 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
125		eqid 2730	. . . . . . 7 ⊢ (+_g‘(𝐻 “_s 𝑃)) = (+_g‘(𝐻 “_s 𝑃))
126	108, 2, 109, 112, 114, 118, 123, 124, 125	mhmimasplusg 32466	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝐻‘𝑥)(+_g‘(𝐻 “_s 𝑃))(𝐻‘𝑦)) = (𝐻‘(𝑥(+_g‘𝑃)𝑦)))
127		algextdeg.l	. . . . . . . . 9 ⊢ 𝐿 = (𝐸 ↾_s (𝐸 fldGen (𝐹 ∪ {𝐴})))
128	12	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐸 ∈ Field)
129	4	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐹 ∈ (SubDRing‘𝐸))
130	14	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝐴 ∈ (𝐸 IntgRing 𝐹))
131		algextdeglem.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴))
132		algextdeglem.n	. . . . . . . . 9 ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~_QG 𝑍))
133		algextdeglem.z	. . . . . . . . 9 ⊢ 𝑍 = (^◡𝐺 “ {(0_g‘𝐿)})
134		algextdeglem.q	. . . . . . . . 9 ⊢ 𝑄 = (𝑃 /_s (𝑃 ~_QG 𝑍))
135		algextdeglem.j	. . . . . . . . 9 ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝))
136	5, 127, 29, 13, 128, 129, 130, 30, 23, 2, 131, 132, 133, 134, 135, 22, 96, 48, 112	algextdeglem7 33068	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥 ∈ 𝑇 ↔ (𝐻‘𝑥) = 𝑥))
137	111, 136	mpbid 231	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘𝑥) = 𝑥)
138	5, 127, 29, 13, 128, 129, 130, 30, 23, 2, 131, 132, 133, 134, 135, 22, 96, 48, 114	algextdeglem7 33068	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑦 ∈ 𝑇 ↔ (𝐻‘𝑦) = 𝑦))
139	113, 138	mpbid 231	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘𝑦) = 𝑦)
140	137, 139	oveq12d 7429	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝐻‘𝑥)(+_g‘(𝐻 “_s 𝑃))(𝐻‘𝑦)) = (𝑥(+_g‘(𝐻 “_s 𝑃))𝑦))
141	100	ringgrpd 20136	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
142	23, 7	ply1lvec 32912	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
143	23, 26, 48, 61, 8	ply1degltlss 32942	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ (LSubSp‘𝑃))
144		eqid 2730	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
145	104, 144	lsslvec 20864	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ LVec ∧ 𝑇 ∈ (LSubSp‘𝑃)) → (𝑃 ↾_s 𝑇) ∈ LVec)
146	142, 143, 145	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 ↾_s 𝑇) ∈ LVec)
147	146	lvecgrpd 20863	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 ↾_s 𝑇) ∈ Grp)
148	2	issubg 19042	. . . . . . . . . 10 ⊢ (𝑇 ∈ (SubGrp‘𝑃) ↔ (𝑃 ∈ Grp ∧ 𝑇 ⊆ 𝑈 ∧ (𝑃 ↾_s 𝑇) ∈ Grp))
149	141, 103, 147, 148	syl3anbrc 1341	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝑃))
150	149	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑇 ∈ (SubGrp‘𝑃))
151	124	subgcl 19052	. . . . . . . 8 ⊢ ((𝑇 ∈ (SubGrp‘𝑃) ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇) → (𝑥(+_g‘𝑃)𝑦) ∈ 𝑇)
152	150, 111, 113, 151	syl3anc 1369	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+_g‘𝑃)𝑦) ∈ 𝑇)
153	141	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → 𝑃 ∈ Grp)
154	2, 124, 153, 112, 114	grpcld 18869	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+_g‘𝑃)𝑦) ∈ 𝑈)
155	5, 127, 29, 13, 128, 129, 130, 30, 23, 2, 131, 132, 133, 134, 135, 22, 96, 48, 154	algextdeglem7 33068	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → ((𝑥(+_g‘𝑃)𝑦) ∈ 𝑇 ↔ (𝐻‘(𝑥(+_g‘𝑃)𝑦)) = (𝑥(+_g‘𝑃)𝑦)))
156	152, 155	mpbid 231	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝐻‘(𝑥(+_g‘𝑃)𝑦)) = (𝑥(+_g‘𝑃)𝑦))
157	126, 140, 156	3eqtr3d 2778	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+_g‘(𝐻 “_s 𝑃))𝑦) = (𝑥(+_g‘𝑃)𝑦))
158		fvex 6903	. . . . . . . . 9 ⊢ ( deg₁ ‘𝐾) ∈ V
159		cnvexg 7917	. . . . . . . . 9 ⊢ (( deg₁ ‘𝐾) ∈ V → ^◡( deg₁ ‘𝐾) ∈ V)
160		imaexg 7908	. . . . . . . . 9 ⊢ (^◡( deg₁ ‘𝐾) ∈ V → (^◡( deg₁ ‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ∈ V)
161	158, 159, 160	mp2b 10	. . . . . . . 8 ⊢ (^◡( deg₁ ‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ∈ V
162	48, 161	eqeltri 2827	. . . . . . 7 ⊢ 𝑇 ∈ V
163	104, 124	ressplusg 17239	. . . . . . 7 ⊢ (𝑇 ∈ V → (+_g‘𝑃) = (+_g‘(𝑃 ↾_s 𝑇)))
164	162, 163	ax-mp 5	. . . . . 6 ⊢ (+_g‘𝑃) = (+_g‘(𝑃 ↾_s 𝑇))
165	164	oveqi 7424	. . . . 5 ⊢ (𝑥(+_g‘𝑃)𝑦) = (𝑥(+_g‘(𝑃 ↾_s 𝑇))𝑦)
166	157, 165	eqtrdi 2786	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑇) ∧ 𝑦 ∈ 𝑇) → (𝑥(+_g‘(𝐻 “_s 𝑃))𝑦) = (𝑥(+_g‘(𝑃 ↾_s 𝑇))𝑦))
167	166	anasss 465	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑇)) → (𝑥(+_g‘(𝐻 “_s 𝑃))𝑦) = (𝑥(+_g‘(𝑃 ↾_s 𝑇))𝑦))
168		simprr 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑦 ∈ 𝑇)
169	12	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐸 ∈ Field)
170	4	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐹 ∈ (SubDRing‘𝐸))
171	14	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐴 ∈ (𝐸 IntgRing 𝐹))
172	103	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑇 ⊆ 𝑈)
173	172, 168	sseldd 3982	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑦 ∈ 𝑈)
174	5, 127, 29, 13, 169, 170, 171, 30, 23, 2, 131, 132, 133, 134, 135, 22, 96, 48, 173	algextdeglem7 33068	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑦 ∈ 𝑇 ↔ (𝐻‘𝑦) = 𝑦))
175	168, 174	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘𝑦) = 𝑦)
176	175	oveq2d 7427	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘(𝐻 “_s 𝑃))(𝐻‘𝑦)) = (𝑥( ·_𝑠 ‘(𝐻 “_s 𝑃))𝑦))
177		simprl 767	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑥 ∈ 𝐹)
178	33	sdrgss 20552	. . . . . . . . . 10 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ (Base‘𝐸))
179	5, 33	ressbas2 17186	. . . . . . . . . 10 ⊢ (𝐹 ⊆ (Base‘𝐸) → 𝐹 = (Base‘𝐾))
180	4, 178, 179	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
181	23	ply1sca 21995	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Ring → 𝐾 = (Scalar‘𝑃))
182	8, 181	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 = (Scalar‘𝑃))
183	182	fveq2d 6894	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘𝑃)))
184	180, 183	eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (Base‘(Scalar‘𝑃)))
185	184	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐹 = (Base‘(Scalar‘𝑃)))
186	177, 185	eleqtrd 2833	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑥 ∈ (Base‘(Scalar‘𝑃)))
187	117	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻:𝑈–onto→(Base‘(𝐻 “_s 𝑃)))
188	119	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻 ∈ (𝑃 LMHom (𝐻 “_s 𝑃)))
189		eqid 2730	. . . . . 6 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
190		eqid 2730	. . . . . 6 ⊢ ( ·_𝑠 ‘(𝐻 “_s 𝑃)) = ( ·_𝑠 ‘(𝐻 “_s 𝑃))
191		eqid 2730	. . . . . 6 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
192	108, 2, 109, 186, 173, 187, 188, 189, 190, 191	lmhmimasvsca 32467	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘(𝐻 “_s 𝑃))(𝐻‘𝑦)) = (𝐻‘(𝑥( ·_𝑠 ‘𝑃)𝑦)))
193	176, 192	eqtr3d 2772	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘(𝐻 “_s 𝑃))𝑦) = (𝐻‘(𝑥( ·_𝑠 ‘𝑃)𝑦)))
194	64, 96	fmptd 7114	. . . . . 6 ⊢ (𝜑 → 𝐻:𝑈⟶𝑇)
195	194	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝐻:𝑈⟶𝑇)
196		eqid 2730	. . . . . 6 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
197	142	lveclmodd 20862	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ LMod)
198	197	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑃 ∈ LMod)
199	2, 196, 189, 191, 198, 186, 173	lmodvscld 20633	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘𝑃)𝑦) ∈ 𝑈)
200	195, 199	ffvelcdmd 7086	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘(𝑥( ·_𝑠 ‘𝑃)𝑦)) ∈ 𝑇)
201	193, 200	eqeltrd 2831	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘(𝐻 “_s 𝑃))𝑦) ∈ 𝑇)
202	143	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → 𝑇 ∈ (LSubSp‘𝑃))
203	196, 189, 191, 144	lssvscl 20710	. . . . . 6 ⊢ (((𝑃 ∈ LMod ∧ 𝑇 ∈ (LSubSp‘𝑃)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘𝑃)𝑦) ∈ 𝑇)
204	198, 202, 186, 168, 203	syl22anc 835	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘𝑃)𝑦) ∈ 𝑇)
205	5, 127, 29, 13, 169, 170, 171, 30, 23, 2, 131, 132, 133, 134, 135, 22, 96, 48, 199	algextdeglem7 33068	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → ((𝑥( ·_𝑠 ‘𝑃)𝑦) ∈ 𝑇 ↔ (𝐻‘(𝑥( ·_𝑠 ‘𝑃)𝑦)) = (𝑥( ·_𝑠 ‘𝑃)𝑦)))
206	204, 205	mpbid 231	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝐻‘(𝑥( ·_𝑠 ‘𝑃)𝑦)) = (𝑥( ·_𝑠 ‘𝑃)𝑦))
207	104, 189	ressvsca 17293	. . . . . 6 ⊢ (𝑇 ∈ V → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘(𝑃 ↾_s 𝑇)))
208	162, 207	mp1i 13	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘(𝑃 ↾_s 𝑇)))
209	208	oveqd 7428	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘𝑃)𝑦) = (𝑥( ·_𝑠 ‘(𝑃 ↾_s 𝑇))𝑦))
210	193, 206, 209	3eqtrd 2774	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝑇)) → (𝑥( ·_𝑠 ‘(𝐻 “_s 𝑃))𝑦) = (𝑥( ·_𝑠 ‘(𝑃 ↾_s 𝑇))𝑦))
211		eqid 2730	. . 3 ⊢ (Scalar‘(𝐻 “_s 𝑃)) = (Scalar‘(𝐻 “_s 𝑃))
212	104, 196	resssca 17292	. . . 4 ⊢ (𝑇 ∈ V → (Scalar‘𝑃) = (Scalar‘(𝑃 ↾_s 𝑇)))
213	162, 212	ax-mp 5	. . 3 ⊢ (Scalar‘𝑃) = (Scalar‘(𝑃 ↾_s 𝑇))
214	1, 3, 98, 100, 196	imassca 17469	. . . . . 6 ⊢ (𝜑 → (Scalar‘𝑃) = (Scalar‘(𝐻 “_s 𝑃)))
215	182, 214	eqtrd 2770	. . . . 5 ⊢ (𝜑 → 𝐾 = (Scalar‘(𝐻 “_s 𝑃)))
216	215	fveq2d 6894	. . . 4 ⊢ (𝜑 → (Base‘𝐾) = (Base‘(Scalar‘(𝐻 “_s 𝑃))))
217	180, 216	eqtrd 2770	. . 3 ⊢ (𝜑 → 𝐹 = (Base‘(Scalar‘(𝐻 “_s 𝑃))))
218	214	fveq2d 6894	. . . . . 6 ⊢ (𝜑 → (+_g‘(Scalar‘𝑃)) = (+_g‘(Scalar‘(𝐻 “_s 𝑃))))
219	218	oveqd 7428	. . . . 5 ⊢ (𝜑 → (𝑥(+_g‘(Scalar‘𝑃))𝑦) = (𝑥(+_g‘(Scalar‘(𝐻 “_s 𝑃)))𝑦))
220	219	eqcomd 2736	. . . 4 ⊢ (𝜑 → (𝑥(+_g‘(Scalar‘(𝐻 “_s 𝑃)))𝑦) = (𝑥(+_g‘(Scalar‘𝑃))𝑦))
221	220	adantr 479	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥(+_g‘(Scalar‘(𝐻 “_s 𝑃)))𝑦) = (𝑥(+_g‘(Scalar‘𝑃))𝑦))
222		lmhmlvec2 32992	. . . 4 ⊢ ((𝑃 ∈ LVec ∧ 𝐻 ∈ (𝑃 LMHom (𝐻 “_s 𝑃))) → (𝐻 “_s 𝑃) ∈ LVec)
223	142, 119, 222	syl2anc 582	. . 3 ⊢ (𝜑 → (𝐻 “_s 𝑃) ∈ LVec)
224	101, 106, 107, 167, 201, 210, 211, 213, 217, 184, 221, 223, 146	dimpropd 32981	. 2 ⊢ (𝜑 → (dim‘(𝐻 “_s 𝑃)) = (dim‘(𝑃 ↾_s 𝑇)))
225	23, 26, 48, 61, 7, 104	ply1degltdim 32996	. 2 ⊢ (𝜑 → (dim‘(𝑃 ↾_s 𝑇)) = (𝐷‘(𝑀‘𝐴)))
226	224, 225	eqtrd 2770	1 ⊢ (𝜑 → (dim‘(𝐻 “_s 𝑃)) = (𝐷‘(𝑀‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 {crab 3430 Vcvv 3472 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 {csn 4627 ∪ cuni 4907 class class class wbr 5147 ↦ cmpt 5230 ^◡ccnv 5674 dom cdm 5675 “ cima 5678 ⟶wf 6538 –onto→wfo 6540 ‘cfv 6542 (class class class)co 7411 [cec 8703 1c1 11113 -∞cmnf 11250 < clt 11252 ≤ cle 11253 − cmin 11448 ℕ₀cn0 12476 ℤcz 12562 [,)cico 13330 Basecbs 17148 ↾_s cress 17177 +_gcplusg 17201 Scalarcsca 17204 ·_𝑠 cvsca 17205 0_gc0g 17389 “_s cimas 17454 /_s cqus 17455 MndHom cmhm 18703 Grpcgrp 18855 SubGrpcsubg 19036 ~_QG cqg 19038 GrpHom cghm 19127 Ringcrg 20127 SubRingcsubrg 20457 DivRingcdr 20500 Fieldcfield 20501 SubDRingcsdrg 20545 LModclmod 20614 LSubSpclss 20686 LMHom clmhm 20774 LVecclvec 20857 RSpancrsp 20929 IDomncidom 21097 PwSer₁cps1 21918 Poly₁cpl1 21920 evalSub₁ ces1 22052 deg₁ cdg1 25804 Monic_1pcmn1 25878 Unic_1pcuc1p 25879 rem_1pcr1p 25881 idlGen_1pcig1p 25882 fldGen cfldgen 32670 dimcldim 32971 IntgRing cirng 33036 minPoly cminply 33045

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-reg 9589 ax-inf2 9638 ax-ac2 10460 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-ofr 7673 df-rpss 7715 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-tpos 8213 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-oadd 8472 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-sup 9439 df-inf 9440 df-oi 9507 df-r1 9761 df-rank 9762 df-dju 9898 df-card 9936 df-acn 9939 df-ac 10113 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-xnn0 12549 df-z 12563 df-dec 12682 df-uz 12827 df-ico 13334 df-fz 13489 df-fzo 13632 df-seq 13971 df-hash 14295 df-struct 17084 df-sets 17101 df-slot 17119 df-ndx 17131 df-base 17149 df-ress 17178 df-plusg 17214 df-mulr 17215 df-starv 17216 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ocomp 17222 df-ds 17223 df-unif 17224 df-hom 17225 df-cco 17226 df-0g 17391 df-gsum 17392 df-prds 17397 df-pws 17399 df-imas 17458 df-mre 17534 df-mrc 17535 df-mri 17536 df-acs 17537 df-proset 18252 df-drs 18253 df-poset 18270 df-ipo 18485 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mhm 18705 df-submnd 18706 df-grp 18858 df-minusg 18859 df-sbg 18860 df-mulg 18987 df-subg 19039 df-ghm 19128 df-cntz 19222 df-cmn 19691 df-abl 19692 df-mgp 20029 df-rng 20047 df-ur 20076 df-srg 20081 df-ring 20129 df-cring 20130 df-oppr 20225 df-dvdsr 20248 df-unit 20249 df-invr 20279 df-rhm 20363 df-nzr 20404 df-subrng 20434 df-subrg 20459 df-drng 20502 df-field 20503 df-sdrg 20546 df-lmod 20616 df-lss 20687 df-lsp 20727 df-lmhm 20777 df-lbs 20830 df-lvec 20858 df-sra 20930 df-rgmod 20931 df-lidl 20932 df-rsp 20933 df-rlreg 21099 df-domn 21100 df-idom 21101 df-cnfld 21145 df-dsmm 21506 df-frlm 21521 df-uvc 21557 df-lindf 21580 df-linds 21581 df-assa 21627 df-asp 21628 df-ascl 21629 df-psr 21681 df-mvr 21682 df-mpl 21683 df-opsr 21685 df-evls 21854 df-evl 21855 df-psr1 21923 df-vr1 21924 df-ply1 21925 df-coe1 21926 df-evls1 22054 df-evl1 22055 df-mdeg 25805 df-deg1 25806 df-mon1 25883 df-uc1p 25884 df-q1p 25885 df-r1p 25886 df-ig1p 25887 df-dim 32972 df-irng 33037 df-minply 33046

This theorem is referenced by: algextdeg 33070

W3C validator