algextdeglem8

Description: Lemma for algextdeg . The dimension of the univariate polynomial remainder ring ( H "s P ) is the degree of the minimal polynomial. (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))$
	algextdeglem.t	$⊢ T = {\deg_{1} (K)}^{-1} [[−∞, D (M (A)))]$
Assertion	algextdeglem8	$⊢ φ \to \dim (H “_{𝑠} P) = D (M (A))$

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		algextdeglem.t	$⊢ T = {\deg_{1} (K)}^{-1} [[−∞, D (M (A)))]$
19		eqidd	$⊢ φ \to H “_{𝑠} P = H “_{𝑠} P$
20	10	a1i	$⊢ φ \to U = {Base}_{P}$
21	1	sdrgdrng	$⊢ F \in SubDRing (E) \to K \in DivRing$
22	6 21	syl	$⊢ φ \to K \in DivRing$
23	22	drngringd	$⊢ φ \to K \in Ring$
24	23	adantr	$⊢ (φ \land p \in U) \to K \in Ring$
25		simpr	$⊢ (φ \land p \in U) \to p \in U$
26		eqid	$⊢ 0_{{Poly}_{1} (E)} = 0_{{Poly}_{1} (E)}$
27	1	fveq2i	$⊢ {Monic}_{1p} (K) = {Monic}_{1p} (E ↾_{𝑠} F)$
28	26 5 6 4 7 27	minplym1p	$⊢ φ \to M (A) \in {Monic}_{1p} (K)$
29	28	adantr	$⊢ (φ \land p \in U) \to M (A) \in {Monic}_{1p} (K)$
30		eqid	$⊢ {Unic}_{1p} (K) = {Unic}_{1p} (K)$
31		eqid	$⊢ {Monic}_{1p} (K) = {Monic}_{1p} (K)$
32	30 31	mon1puc1p	$⊢ (K \in Ring \land M (A) \in {Monic}_{1p} (K)) \to M (A) \in {Unic}_{1p} (K)$
33	24 29 32	syl2anc	$⊢ (φ \land p \in U) \to M (A) \in {Unic}_{1p} (K)$
34	16 9 10 30	r1pcl	$⊢ (K \in Ring \land p \in U \land M (A) \in {Unic}_{1p} (K)) \to p R M (A) \in U$
35	24 25 33 34	syl3anc	$⊢ (φ \land p \in U) \to p R M (A) \in U$
36		eqid	$⊢ \deg_{1} (K) = \deg_{1} (K)$
37	16 9 10 30 36	r1pdeglt	$⊢ (K \in Ring \land p \in U \land M (A) \in {Unic}_{1p} (K)) \to \deg_{1} (K) (p R M (A)) < \deg_{1} (K) (M (A))$
38	24 25 33 37	syl3anc	$⊢ (φ \land p \in U) \to \deg_{1} (K) (p R M (A)) < \deg_{1} (K) (M (A))$
39	1	fveq2i	$⊢ {Poly}_{1} (K) = {Poly}_{1} (E ↾_{𝑠} F)$
40	9 39	eqtri	$⊢ P = {Poly}_{1} (E ↾_{𝑠} F)$
41		eqid	$⊢ {Base}_{E} = {Base}_{E}$
42		eqid	$⊢ 0_{E} = 0_{E}$
43	5	fldcrngd	$⊢ φ \to E \in CRing$
44		sdrgsubrg	$⊢ F \in SubDRing (E) \to F \in SubRing (E)$
45	6 44	syl	$⊢ φ \to F \in SubRing (E)$
46	8 1 41 42 43 45	irngssv	$⊢ φ \to E IntgRing F \subseteq {Base}_{E}$
47	46 7	sseldd	$⊢ φ \to A \in {Base}_{E}$
48		eqid	$⊢ \{p \in dom O \| O (p) (A) = 0_{E}\} = \{p \in dom O \| O (p) (A) = 0_{E}\}$
49		eqid	$⊢ RSpan (P) = RSpan (P)$
50		eqid	$⊢ {idlGen}_{1p} (E ↾_{𝑠} F) = {idlGen}_{1p} (E ↾_{𝑠} F)$
51	8 40 41 5 6 47 42 48 49 50 4	minplycl	$⊢ φ \to M (A) \in {Base}_{P}$
52	51 10	eleqtrrdi	$⊢ φ \to M (A) \in U$
53	1 3 9 10 52 45	ressdeg1	$⊢ φ \to D (M (A)) = \deg_{1} (K) (M (A))$
54	53	adantr	$⊢ (φ \land p \in U) \to D (M (A)) = \deg_{1} (K) (M (A))$
55	38 54	breqtrrd	$⊢ (φ \land p \in U) \to \deg_{1} (K) (p R M (A)) < D (M (A))$
56	5	flddrngd	$⊢ φ \to E \in DivRing$
57	56	drngringd	$⊢ φ \to E \in Ring$
58		eqid	$⊢ {Poly}_{1} (E) = {Poly}_{1} (E)$
59		eqid	$⊢ {PwSer}_{1} (K) = {PwSer}_{1} (K)$
60		eqid	$⊢ {Base}_{{PwSer}_{1} (K)} = {Base}_{{PwSer}_{1} (K)}$
61		eqid	$⊢ {Base}_{{Poly}_{1} (E)} = {Base}_{{Poly}_{1} (E)}$
62	58 1 9 10 45 59 60 61	ressply1bas2	$⊢ φ \to U = {Base}_{{PwSer}_{1} (K)} \cap {Base}_{{Poly}_{1} (E)}$
63		inss2	$⊢ {Base}_{{PwSer}_{1} (K)} \cap {Base}_{{Poly}_{1} (E)} \subseteq {Base}_{{Poly}_{1} (E)}$
64	62 63	eqsstrdi	$⊢ φ \to U \subseteq {Base}_{{Poly}_{1} (E)}$
65	64 52	sseldd	$⊢ φ \to M (A) \in {Base}_{{Poly}_{1} (E)}$
66	26 5 6 4 7	irngnminplynz	$⊢ φ \to M (A) \neq 0_{{Poly}_{1} (E)}$
67	3 58 26 61	deg1nn0cl	$⊢ (E \in Ring \land M (A) \in {Base}_{{Poly}_{1} (E)} \land M (A) \neq 0_{{Poly}_{1} (E)}) \to D (M (A)) \in ℕ_{0}$
68	57 65 66 67	syl3anc	$⊢ φ \to D (M (A)) \in ℕ_{0}$
69	9 36 18 68 23 10	ply1degleel	$⊢ φ \to (p R M (A) \in T \leftrightarrow (p R M (A) \in U \land \deg_{1} (K) (p R M (A)) < D (M (A))))$
70	69	adantr	$⊢ (φ \land p \in U) \to (p R M (A) \in T \leftrightarrow (p R M (A) \in U \land \deg_{1} (K) (p R M (A)) < D (M (A))))$
71	35 55 70	mpbir2and	$⊢ (φ \land p \in U) \to p R M (A) \in T$
72	71	ralrimiva	$⊢ φ \to \forall p \in U p R M (A) \in T$
73		oveq1	$⊢ p = q \to p R M (A) = q R M (A)$
74	73	eqeq2d	$⊢ p = q \to (q = p R M (A) \leftrightarrow q = q R M (A))$
75		eqcom	$⊢ q = q R M (A) \leftrightarrow q R M (A) = q$
76	74 75	bitrdi	$⊢ p = q \to (q = p R M (A) \leftrightarrow q R M (A) = q)$
77	9 36 18 68 23 10	ply1degltel	$⊢ φ \to (q \in T \leftrightarrow (q \in U \land \deg_{1} (K) (q) \leq D (M (A)) - 1))$
78	77	simprbda	$⊢ (φ \land q \in T) \to q \in U$
79	77	simplbda	$⊢ (φ \land q \in T) \to \deg_{1} (K) (q) \leq D (M (A)) - 1$
80	53	oveq1d	$⊢ φ \to D (M (A)) - 1 = \deg_{1} (K) (M (A)) - 1$
81	80	adantr	$⊢ (φ \land q \in T) \to D (M (A)) - 1 = \deg_{1} (K) (M (A)) - 1$
82	79 81	breqtrd	$⊢ (φ \land q \in T) \to \deg_{1} (K) (q) \leq \deg_{1} (K) (M (A)) - 1$
83	36 9 10	deg1cl	$⊢ q \in U \to \deg_{1} (K) (q) \in (ℕ_{0} \cup \{−∞\})$
84	78 83	syl	$⊢ (φ \land q \in T) \to \deg_{1} (K) (q) \in (ℕ_{0} \cup \{−∞\})$
85	68	nn0zd	$⊢ φ \to D (M (A)) \in ℤ$
86	53 85	eqeltrrd	$⊢ φ \to \deg_{1} (K) (M (A)) \in ℤ$
87	86	adantr	$⊢ (φ \land q \in T) \to \deg_{1} (K) (M (A)) \in ℤ$
88		degltlem1	$⊢ (\deg_{1} (K) (q) \in (ℕ_{0} \cup \{−∞\}) \land \deg_{1} (K) (M (A)) \in ℤ) \to (\deg_{1} (K) (q) < \deg_{1} (K) (M (A)) \leftrightarrow \deg_{1} (K) (q) \leq \deg_{1} (K) (M (A)) - 1)$
89	84 87 88	syl2anc	$⊢ (φ \land q \in T) \to (\deg_{1} (K) (q) < \deg_{1} (K) (M (A)) \leftrightarrow \deg_{1} (K) (q) \leq \deg_{1} (K) (M (A)) - 1)$
90	82 89	mpbird	$⊢ (φ \land q \in T) \to \deg_{1} (K) (q) < \deg_{1} (K) (M (A))$
91		fldsdrgfld	$⊢ (E \in Field \land F \in SubDRing (E)) \to E ↾_{𝑠} F \in Field$
92	5 6 91	syl2anc	$⊢ φ \to E ↾_{𝑠} F \in Field$
93	1 92	eqeltrid	$⊢ φ \to K \in Field$
94		fldidom	$⊢ K \in Field \to K \in IDomn$
95	93 94	syl	$⊢ φ \to K \in IDomn$
96	95	idomdomd	$⊢ φ \to K \in Domn$
97	96	adantr	$⊢ (φ \land q \in T) \to K \in Domn$
98	23 28 32	syl2anc	$⊢ φ \to M (A) \in {Unic}_{1p} (K)$
99	98	adantr	$⊢ (φ \land q \in T) \to M (A) \in {Unic}_{1p} (K)$
100	9 10 30 16 36 97 78 99	r1pid2	$⊢ (φ \land q \in T) \to (q R M (A) = q \leftrightarrow \deg_{1} (K) (q) < \deg_{1} (K) (M (A)))$
101	90 100	mpbird	$⊢ (φ \land q \in T) \to q R M (A) = q$
102	76 78 101	rspcedvdw	$⊢ (φ \land q \in T) \to \exists p \in U q = p R M (A)$
103	102	ralrimiva	$⊢ φ \to \forall q \in T \exists p \in U q = p R M (A)$
104	17	fompt	$⊢ H : U \underset{onto}{⟶} T \leftrightarrow (\forall p \in U p R M (A) \in T \land \forall q \in T \exists p \in U q = p R M (A))$
105	72 103 104	sylanbrc	$⊢ φ \to H : U \underset{onto}{⟶} T$
106	9	ply1ring	$⊢ K \in Ring \to P \in Ring$
107	23 106	syl	$⊢ φ \to P \in Ring$
108	19 20 105 107	imasbas	$⊢ φ \to T = {Base}_{(H “_{𝑠} P)}$
109	78	ex	$⊢ φ \to (q \in T \to q \in U)$
110	109	ssrdv	$⊢ φ \to T \subseteq U$
111		eqid	$⊢ P ↾_{𝑠} T = P ↾_{𝑠} T$
112	111 10	ressbas2	$⊢ T \subseteq U \to T = {Base}_{(P ↾_{𝑠} T)}$
113	110 112	syl	$⊢ φ \to T = {Base}_{(P ↾_{𝑠} T)}$
114		ssidd	$⊢ φ \to T \subseteq T$
115		eqid	$⊢ H “_{𝑠} P = H “_{𝑠} P$
116		eqid	$⊢ {Base}_{(H “_{𝑠} P)} = {Base}_{(H “_{𝑠} P)}$
117	110	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to T \subseteq U$
118		simplr	$⊢ ((φ \land x \in T) \land y \in T) \to x \in T$
119	117 118	sseldd	$⊢ ((φ \land x \in T) \land y \in T) \to x \in U$
120		simpr	$⊢ ((φ \land x \in T) \land y \in T) \to y \in T$
121	117 120	sseldd	$⊢ ((φ \land x \in T) \land y \in T) \to y \in U$
122		foeq3	$⊢ T = {Base}_{(H “_{𝑠} P)} \to (H : U \underset{onto}{⟶} T \leftrightarrow H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)})$
123	108 122	syl	$⊢ φ \to (H : U \underset{onto}{⟶} T \leftrightarrow H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)})$
124	105 123	mpbid	$⊢ φ \to H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)}$
125	124	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)}$
126	9 10 16 30 17 23 98	r1plmhm	$⊢ φ \to H \in (P LMHom (H “_{𝑠} P))$
127	126	lmhmghmd	$⊢ φ \to H \in (P GrpHom (H “_{𝑠} P))$
128		ghmmhm	$⊢ H \in (P GrpHom (H “_{𝑠} P)) \to H \in (P MndHom (H “_{𝑠} P))$
129	127 128	syl	$⊢ φ \to H \in (P MndHom (H “_{𝑠} P))$
130	129	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to H \in (P MndHom (H “_{𝑠} P))$
131		eqid	$⊢ +_{P} = +_{P}$
132		eqid	$⊢ +_{(H “_{𝑠} P)} = +_{(H “_{𝑠} P)}$
133	115 10 116 119 121 125 130 131 132	mhmimasplusg	$⊢ ((φ \land x \in T) \land y \in T) \to H (x) +_{(H “_{𝑠} P)} H (y) = H (x +_{P} y)$
134	5	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to E \in Field$
135	6	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to F \in SubDRing (E)$
136	7	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to A \in (E IntgRing F)$
137	1 2 3 4 134 135 136 8 9 10 11 12 13 14 15 16 17 18 119	algextdeglem7	$⊢ ((φ \land x \in T) \land y \in T) \to (x \in T \leftrightarrow H (x) = x)$
138	118 137	mpbid	$⊢ ((φ \land x \in T) \land y \in T) \to H (x) = x$
139	1 2 3 4 134 135 136 8 9 10 11 12 13 14 15 16 17 18 121	algextdeglem7	$⊢ ((φ \land x \in T) \land y \in T) \to (y \in T \leftrightarrow H (y) = y)$
140	120 139	mpbid	$⊢ ((φ \land x \in T) \land y \in T) \to H (y) = y$
141	138 140	oveq12d	$⊢ ((φ \land x \in T) \land y \in T) \to H (x) +_{(H “_{𝑠} P)} H (y) = x +_{(H “_{𝑠} P)} y$
142	107	ringgrpd	$⊢ φ \to P \in Grp$
143	9 22	ply1lvec	$⊢ φ \to P \in LVec$
144	9 36 18 68 23	ply1degltlss	$⊢ φ \to T \in LSubSp (P)$
145		eqid	$⊢ LSubSp (P) = LSubSp (P)$
146	111 145	lsslvec	$⊢ (P \in LVec \land T \in LSubSp (P)) \to P ↾_{𝑠} T \in LVec$
147	143 144 146	syl2anc	$⊢ φ \to P ↾_{𝑠} T \in LVec$
148	147	lvecgrpd	$⊢ φ \to P ↾_{𝑠} T \in Grp$
149	10	issubg	$⊢ T \in SubGrp (P) \leftrightarrow (P \in Grp \land T \subseteq U \land P ↾_{𝑠} T \in Grp)$
150	142 110 148 149	syl3anbrc	$⊢ φ \to T \in SubGrp (P)$
151	150	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to T \in SubGrp (P)$
152	131	subgcl	$⊢ (T \in SubGrp (P) \land x \in T \land y \in T) \to x +_{P} y \in T$
153	151 118 120 152	syl3anc	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{P} y \in T$
154	142	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to P \in Grp$
155	10 131 154 119 121	grpcld	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{P} y \in U$
156	1 2 3 4 134 135 136 8 9 10 11 12 13 14 15 16 17 18 155	algextdeglem7	$⊢ ((φ \land x \in T) \land y \in T) \to (x +_{P} y \in T \leftrightarrow H (x +_{P} y) = x +_{P} y)$
157	153 156	mpbid	$⊢ ((φ \land x \in T) \land y \in T) \to H (x +_{P} y) = x +_{P} y$
158	133 141 157	3eqtr3d	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{(H “_{𝑠} P)} y = x +_{P} y$
159		fvex	$⊢ \deg_{1} (K) \in V$
160		cnvexg	$⊢ \deg_{1} (K) \in V \to {\deg_{1} (K)}^{-1} \in V$
161		imaexg	$⊢ {\deg_{1} (K)}^{-1} \in V \to {\deg_{1} (K)}^{-1} [[−∞, D (M (A)))] \in V$
162	159 160 161	mp2b	$⊢ {\deg_{1} (K)}^{-1} [[−∞, D (M (A)))] \in V$
163	18 162	eqeltri	$⊢ T \in V$
164	111 131	ressplusg	$⊢ T \in V \to +_{P} = +_{(P ↾_{𝑠} T)}$
165	163 164	ax-mp	$⊢ +_{P} = +_{(P ↾_{𝑠} T)}$
166	165	oveqi	$⊢ x +_{P} y = x +_{(P ↾_{𝑠} T)} y$
167	158 166	eqtrdi	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{(H “_{𝑠} P)} y = x +_{(P ↾_{𝑠} T)} y$
168	167	anasss	$⊢ (φ \land (x \in T \land y \in T)) \to x +_{(H “_{𝑠} P)} y = x +_{(P ↾_{𝑠} T)} y$
169		simprr	$⊢ (φ \land (x \in F \land y \in T)) \to y \in T$
170	5	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to E \in Field$
171	6	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to F \in SubDRing (E)$
172	7	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to A \in (E IntgRing F)$
173	110	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to T \subseteq U$
174	173 169	sseldd	$⊢ (φ \land (x \in F \land y \in T)) \to y \in U$
175	1 2 3 4 170 171 172 8 9 10 11 12 13 14 15 16 17 18 174	algextdeglem7	$⊢ (φ \land (x \in F \land y \in T)) \to (y \in T \leftrightarrow H (y) = y)$
176	169 175	mpbid	$⊢ (φ \land (x \in F \land y \in T)) \to H (y) = y$
177	176	oveq2d	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} H (y) = x \cdot_{(H “_{𝑠} P)} y$
178		simprl	$⊢ (φ \land (x \in F \land y \in T)) \to x \in F$
179	41	sdrgss	$⊢ F \in SubDRing (E) \to F \subseteq {Base}_{E}$
180	1 41	ressbas2	$⊢ F \subseteq {Base}_{E} \to F = {Base}_{K}$
181	6 179 180	3syl	$⊢ φ \to F = {Base}_{K}$
182	9	ply1sca	$⊢ K \in Ring \to K = Scalar (P)$
183	23 182	syl	$⊢ φ \to K = Scalar (P)$
184	183	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (P)}$
185	181 184	eqtrd	$⊢ φ \to F = {Base}_{Scalar (P)}$
186	185	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to F = {Base}_{Scalar (P)}$
187	178 186	eleqtrd	$⊢ (φ \land (x \in F \land y \in T)) \to x \in {Base}_{Scalar (P)}$
188	124	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)}$
189	126	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to H \in (P LMHom (H “_{𝑠} P))$
190		eqid	$⊢ \cdot_{P} = \cdot_{P}$
191		eqid	$⊢ \cdot_{(H “_{𝑠} P)} = \cdot_{(H “_{𝑠} P)}$
192		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
193	115 10 116 187 174 188 189 190 191 192	lmhmimasvsca	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} H (y) = H (x \cdot_{P} y)$
194	177 193	eqtr3d	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} y = H (x \cdot_{P} y)$
195	71 17	fmptd	$⊢ φ \to H : U ⟶ T$
196	195	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to H : U ⟶ T$
197		eqid	$⊢ Scalar (P) = Scalar (P)$
198	143	lveclmodd	$⊢ φ \to P \in LMod$
199	198	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to P \in LMod$
200	10 197 190 192 199 187 174	lmodvscld	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{P} y \in U$
201	196 200	ffvelcdmd	$⊢ (φ \land (x \in F \land y \in T)) \to H (x \cdot_{P} y) \in T$
202	194 201	eqeltrd	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} y \in T$
203	144	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to T \in LSubSp (P)$
204	197 190 192 145	lssvscl	$⊢ ((P \in LMod \land T \in LSubSp (P)) \land (x \in {Base}_{Scalar (P)} \land y \in T)) \to x \cdot_{P} y \in T$
205	199 203 187 169 204	syl22anc	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{P} y \in T$
206	1 2 3 4 170 171 172 8 9 10 11 12 13 14 15 16 17 18 200	algextdeglem7	$⊢ (φ \land (x \in F \land y \in T)) \to (x \cdot_{P} y \in T \leftrightarrow H (x \cdot_{P} y) = x \cdot_{P} y)$
207	205 206	mpbid	$⊢ (φ \land (x \in F \land y \in T)) \to H (x \cdot_{P} y) = x \cdot_{P} y$
208	111 190	ressvsca	$⊢ T \in V \to \cdot_{P} = \cdot_{(P ↾_{𝑠} T)}$
209	163 208	mp1i	$⊢ (φ \land (x \in F \land y \in T)) \to \cdot_{P} = \cdot_{(P ↾_{𝑠} T)}$
210	209	oveqd	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{P} y = x \cdot_{(P ↾_{𝑠} T)} y$
211	194 207 210	3eqtrd	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} y = x \cdot_{(P ↾_{𝑠} T)} y$
212		eqid	$⊢ Scalar (H “_{𝑠} P) = Scalar (H “_{𝑠} P)$
213	111 197	resssca	$⊢ T \in V \to Scalar (P) = Scalar (P ↾_{𝑠} T)$
214	163 213	ax-mp	$⊢ Scalar (P) = Scalar (P ↾_{𝑠} T)$
215	19 20 105 107 197	imassca	$⊢ φ \to Scalar (P) = Scalar (H “_{𝑠} P)$
216	183 215	eqtrd	$⊢ φ \to K = Scalar (H “_{𝑠} P)$
217	216	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (H “_{𝑠} P)}$
218	181 217	eqtrd	$⊢ φ \to F = {Base}_{Scalar (H “_{𝑠} P)}$
219	215	fveq2d	$⊢ φ \to +_{Scalar (P)} = +_{Scalar (H “_{𝑠} P)}$
220	219	oveqd	$⊢ φ \to x +_{Scalar (P)} y = x +_{Scalar (H “_{𝑠} P)} y$
221	220	eqcomd	$⊢ φ \to x +_{Scalar (H “_{𝑠} P)} y = x +_{Scalar (P)} y$
222	221	adantr	$⊢ (φ \land (x \in F \land y \in F)) \to x +_{Scalar (H “_{𝑠} P)} y = x +_{Scalar (P)} y$
223		lmhmlvec2	$⊢ (P \in LVec \land H \in (P LMHom (H “_{𝑠} P))) \to H “_{𝑠} P \in LVec$
224	143 126 223	syl2anc	$⊢ φ \to H “_{𝑠} P \in LVec$
225	108 113 114 168 202 211 212 214 218 185 222 224 147	dimpropd	$⊢ φ \to \dim (H “_{𝑠} P) = \dim (P ↾_{𝑠} T)$
226	9 36 18 68 22 111	ply1degltdim	$⊢ φ \to \dim (P ↾_{𝑠} T) = D (M (A))$
227	225 226	eqtrd	$⊢ φ \to \dim (H “_{𝑠} P) = D (M (A))$

Metamath Proof Explorer

Theorem algextdeglem8

Proof