algextdeglem8

	Ref	Expression
Hypotheses	algextdeg.k	$⊢ K = E ↾_{𝑠} F$
	algextdeg.l	No typesetting found for \|- L = ( E \|`s ( E fldGen ( F u. { A } ) ) ) with typecode \|-
	algextdeg.d	$⊢ D = \deg_{1} (E)$
	algextdeg.m	No typesetting found for \|- M = ( E minPoly F ) with typecode \|-
	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	Could not format L = ( E \|`s ( E fldGen ( F u. { A } ) ) ) : No typesetting found for \|- L = ( E \|`s ( E fldGen ( F u. { A } ) ) ) with typecode \|-
3		algextdeg.d	$⊢ D = \deg_{1} (E)$
4		algextdeg.m	Could not format M = ( E minPoly F ) : No typesetting found for \|- M = ( E minPoly F ) with typecode \|-
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	adantr	$⊢ (φ \land q \in T) \to K \in IDomn$
97	23 28 32	syl2anc	$⊢ φ \to M (A) \in {Unic}_{1p} (K)$
98	97	adantr	$⊢ (φ \land q \in T) \to M (A) \in {Unic}_{1p} (K)$
99	9 10 30 16 96 36 78 98	r1pid2	$⊢ (φ \land q \in T) \to (q R M (A) = q \leftrightarrow \deg_{1} (K) (q) < \deg_{1} (K) (M (A)))$
100	90 99	mpbird	$⊢ (φ \land q \in T) \to q R M (A) = q$
101	76 78 100	rspcedvdw	$⊢ (φ \land q \in T) \to \exists p \in U q = p R M (A)$
102	101	ralrimiva	$⊢ φ \to \forall q \in T \exists p \in U q = p R M (A)$
103	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))$
104	72 102 103	sylanbrc	$⊢ φ \to H : U \underset{onto}{⟶} T$
105	9	ply1ring	$⊢ K \in Ring \to P \in Ring$
106	23 105	syl	$⊢ φ \to P \in Ring$
107	19 20 104 106	imasbas	$⊢ φ \to T = {Base}_{(H “_{𝑠} P)}$
108	78	ex	$⊢ φ \to (q \in T \to q \in U)$
109	108	ssrdv	$⊢ φ \to T \subseteq U$
110		eqid	$⊢ P ↾_{𝑠} T = P ↾_{𝑠} T$
111	110 10	ressbas2	$⊢ T \subseteq U \to T = {Base}_{(P ↾_{𝑠} T)}$
112	109 111	syl	$⊢ φ \to T = {Base}_{(P ↾_{𝑠} T)}$
113		ssidd	$⊢ φ \to T \subseteq T$
114		eqid	$⊢ H “_{𝑠} P = H “_{𝑠} P$
115		eqid	$⊢ {Base}_{(H “_{𝑠} P)} = {Base}_{(H “_{𝑠} P)}$
116	109	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to T \subseteq U$
117		simplr	$⊢ ((φ \land x \in T) \land y \in T) \to x \in T$
118	116 117	sseldd	$⊢ ((φ \land x \in T) \land y \in T) \to x \in U$
119		simpr	$⊢ ((φ \land x \in T) \land y \in T) \to y \in T$
120	116 119	sseldd	$⊢ ((φ \land x \in T) \land y \in T) \to y \in U$
121		foeq3	$⊢ T = {Base}_{(H “_{𝑠} P)} \to (H : U \underset{onto}{⟶} T \leftrightarrow H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)})$
122	107 121	syl	$⊢ φ \to (H : U \underset{onto}{⟶} T \leftrightarrow H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)})$
123	104 122	mpbid	$⊢ φ \to H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)}$
124	123	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)}$
125	9 10 16 30 17 23 97	r1plmhm	$⊢ φ \to H \in (P LMHom (H “_{𝑠} P))$
126	125	lmhmghmd	$⊢ φ \to H \in (P GrpHom (H “_{𝑠} P))$
127		ghmmhm	$⊢ H \in (P GrpHom (H “_{𝑠} P)) \to H \in (P MndHom (H “_{𝑠} P))$
128	126 127	syl	$⊢ φ \to H \in (P MndHom (H “_{𝑠} P))$
129	128	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to H \in (P MndHom (H “_{𝑠} P))$
130		eqid	$⊢ +_{P} = +_{P}$
131		eqid	$⊢ +_{(H “_{𝑠} P)} = +_{(H “_{𝑠} P)}$
132	114 10 115 118 120 124 129 130 131	mhmimasplusg	$⊢ ((φ \land x \in T) \land y \in T) \to H (x) +_{(H “_{𝑠} P)} H (y) = H (x +_{P} y)$
133	5	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to E \in Field$
134	6	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to F \in SubDRing (E)$
135	7	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to A \in (E IntgRing F)$
136	1 2 3 4 133 134 135 8 9 10 11 12 13 14 15 16 17 18 118	algextdeglem7	$⊢ ((φ \land x \in T) \land y \in T) \to (x \in T \leftrightarrow H (x) = x)$
137	117 136	mpbid	$⊢ ((φ \land x \in T) \land y \in T) \to H (x) = x$
138	1 2 3 4 133 134 135 8 9 10 11 12 13 14 15 16 17 18 120	algextdeglem7	$⊢ ((φ \land x \in T) \land y \in T) \to (y \in T \leftrightarrow H (y) = y)$
139	119 138	mpbid	$⊢ ((φ \land x \in T) \land y \in T) \to H (y) = y$
140	137 139	oveq12d	$⊢ ((φ \land x \in T) \land y \in T) \to H (x) +_{(H “_{𝑠} P)} H (y) = x +_{(H “_{𝑠} P)} y$
141	106	ringgrpd	$⊢ φ \to P \in Grp$
142	9 22	ply1lvec	$⊢ φ \to P \in LVec$
143	9 36 18 68 23	ply1degltlss	$⊢ φ \to T \in LSubSp (P)$
144		eqid	$⊢ LSubSp (P) = LSubSp (P)$
145	110 144	lsslvec	$⊢ (P \in LVec \land T \in LSubSp (P)) \to P ↾_{𝑠} T \in LVec$
146	142 143 145	syl2anc	$⊢ φ \to P ↾_{𝑠} T \in LVec$
147	146	lvecgrpd	$⊢ φ \to P ↾_{𝑠} T \in Grp$
148	10	issubg	$⊢ T \in SubGrp (P) \leftrightarrow (P \in Grp \land T \subseteq U \land P ↾_{𝑠} T \in Grp)$
149	141 109 147 148	syl3anbrc	$⊢ φ \to T \in SubGrp (P)$
150	149	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to T \in SubGrp (P)$
151	130	subgcl	$⊢ (T \in SubGrp (P) \land x \in T \land y \in T) \to x +_{P} y \in T$
152	150 117 119 151	syl3anc	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{P} y \in T$
153	141	ad2antrr	$⊢ ((φ \land x \in T) \land y \in T) \to P \in Grp$
154	10 130 153 118 120	grpcld	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{P} y \in U$
155	1 2 3 4 133 134 135 8 9 10 11 12 13 14 15 16 17 18 154	algextdeglem7	$⊢ ((φ \land x \in T) \land y \in T) \to (x +_{P} y \in T \leftrightarrow H (x +_{P} y) = x +_{P} y)$
156	152 155	mpbid	$⊢ ((φ \land x \in T) \land y \in T) \to H (x +_{P} y) = x +_{P} y$
157	132 140 156	3eqtr3d	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{(H “_{𝑠} P)} y = x +_{P} y$
158		fvex	$⊢ \deg_{1} (K) \in V$
159		cnvexg	$⊢ \deg_{1} (K) \in V \to {\deg_{1} (K)}^{-1} \in V$
160		imaexg	$⊢ {\deg_{1} (K)}^{-1} \in V \to {\deg_{1} (K)}^{-1} [[−∞, D (M (A)))] \in V$
161	158 159 160	mp2b	$⊢ {\deg_{1} (K)}^{-1} [[−∞, D (M (A)))] \in V$
162	18 161	eqeltri	$⊢ T \in V$
163	110 130	ressplusg	$⊢ T \in V \to +_{P} = +_{(P ↾_{𝑠} T)}$
164	162 163	ax-mp	$⊢ +_{P} = +_{(P ↾_{𝑠} T)}$
165	164	oveqi	$⊢ x +_{P} y = x +_{(P ↾_{𝑠} T)} y$
166	157 165	eqtrdi	$⊢ ((φ \land x \in T) \land y \in T) \to x +_{(H “_{𝑠} P)} y = x +_{(P ↾_{𝑠} T)} y$
167	166	anasss	$⊢ (φ \land (x \in T \land y \in T)) \to x +_{(H “_{𝑠} P)} y = x +_{(P ↾_{𝑠} T)} y$
168		simprr	$⊢ (φ \land (x \in F \land y \in T)) \to y \in T$
169	5	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to E \in Field$
170	6	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to F \in SubDRing (E)$
171	7	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to A \in (E IntgRing F)$
172	109	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to T \subseteq U$
173	172 168	sseldd	$⊢ (φ \land (x \in F \land y \in T)) \to y \in U$
174	1 2 3 4 169 170 171 8 9 10 11 12 13 14 15 16 17 18 173	algextdeglem7	$⊢ (φ \land (x \in F \land y \in T)) \to (y \in T \leftrightarrow H (y) = y)$
175	168 174	mpbid	$⊢ (φ \land (x \in F \land y \in T)) \to H (y) = y$
176	175	oveq2d	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} H (y) = x \cdot_{(H “_{𝑠} P)} y$
177		simprl	$⊢ (φ \land (x \in F \land y \in T)) \to x \in F$
178	41	sdrgss	$⊢ F \in SubDRing (E) \to F \subseteq {Base}_{E}$
179	1 41	ressbas2	$⊢ F \subseteq {Base}_{E} \to F = {Base}_{K}$
180	6 178 179	3syl	$⊢ φ \to F = {Base}_{K}$
181	9	ply1sca	$⊢ K \in Ring \to K = Scalar (P)$
182	23 181	syl	$⊢ φ \to K = Scalar (P)$
183	182	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (P)}$
184	180 183	eqtrd	$⊢ φ \to F = {Base}_{Scalar (P)}$
185	184	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to F = {Base}_{Scalar (P)}$
186	177 185	eleqtrd	$⊢ (φ \land (x \in F \land y \in T)) \to x \in {Base}_{Scalar (P)}$
187	123	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to H : U \underset{onto}{⟶} {Base}_{(H “_{𝑠} P)}$
188	125	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to H \in (P LMHom (H “_{𝑠} P))$
189		eqid	$⊢ \cdot_{P} = \cdot_{P}$
190		eqid	$⊢ \cdot_{(H “_{𝑠} P)} = \cdot_{(H “_{𝑠} P)}$
191		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
192	114 10 115 186 173 187 188 189 190 191	lmhmimasvsca	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} H (y) = H (x \cdot_{P} y)$
193	176 192	eqtr3d	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} y = H (x \cdot_{P} y)$
194	71 17	fmptd	$⊢ φ \to H : U ⟶ T$
195	194	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to H : U ⟶ T$
196		eqid	$⊢ Scalar (P) = Scalar (P)$
197	142	lveclmodd	$⊢ φ \to P \in LMod$
198	197	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to P \in LMod$
199	10 196 189 191 198 186 173	lmodvscld	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{P} y \in U$
200	195 199	ffvelcdmd	$⊢ (φ \land (x \in F \land y \in T)) \to H (x \cdot_{P} y) \in T$
201	193 200	eqeltrd	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} y \in T$
202	143	adantr	$⊢ (φ \land (x \in F \land y \in T)) \to T \in LSubSp (P)$
203	196 189 191 144	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$
204	198 202 186 168 203	syl22anc	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{P} y \in T$
205	1 2 3 4 169 170 171 8 9 10 11 12 13 14 15 16 17 18 199	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)$
206	204 205	mpbid	$⊢ (φ \land (x \in F \land y \in T)) \to H (x \cdot_{P} y) = x \cdot_{P} y$
207	110 189	ressvsca	$⊢ T \in V \to \cdot_{P} = \cdot_{(P ↾_{𝑠} T)}$
208	162 207	mp1i	$⊢ (φ \land (x \in F \land y \in T)) \to \cdot_{P} = \cdot_{(P ↾_{𝑠} T)}$
209	208	oveqd	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{P} y = x \cdot_{(P ↾_{𝑠} T)} y$
210	193 206 209	3eqtrd	$⊢ (φ \land (x \in F \land y \in T)) \to x \cdot_{(H “_{𝑠} P)} y = x \cdot_{(P ↾_{𝑠} T)} y$
211		eqid	$⊢ Scalar (H “_{𝑠} P) = Scalar (H “_{𝑠} P)$
212	110 196	resssca	$⊢ T \in V \to Scalar (P) = Scalar (P ↾_{𝑠} T)$
213	162 212	ax-mp	$⊢ Scalar (P) = Scalar (P ↾_{𝑠} T)$
214	19 20 104 106 196	imassca	$⊢ φ \to Scalar (P) = Scalar (H “_{𝑠} P)$
215	182 214	eqtrd	$⊢ φ \to K = Scalar (H “_{𝑠} P)$
216	215	fveq2d	$⊢ φ \to {Base}_{K} = {Base}_{Scalar (H “_{𝑠} P)}$
217	180 216	eqtrd	$⊢ φ \to F = {Base}_{Scalar (H “_{𝑠} P)}$
218	214	fveq2d	$⊢ φ \to +_{Scalar (P)} = +_{Scalar (H “_{𝑠} P)}$
219	218	oveqd	$⊢ φ \to x +_{Scalar (P)} y = x +_{Scalar (H “_{𝑠} P)} y$
220	219	eqcomd	$⊢ φ \to x +_{Scalar (H “_{𝑠} P)} y = x +_{Scalar (P)} y$
221	220	adantr	$⊢ (φ \land (x \in F \land y \in F)) \to x +_{Scalar (H “_{𝑠} P)} y = x +_{Scalar (P)} y$
222		lmhmlvec2	$⊢ (P \in LVec \land H \in (P LMHom (H “_{𝑠} P))) \to H “_{𝑠} P \in LVec$
223	142 125 222	syl2anc	$⊢ φ \to H “_{𝑠} P \in LVec$
224	107 112 113 167 201 210 211 213 217 184 221 223 146	dimpropd	$⊢ φ \to \dim (H “_{𝑠} P) = \dim (P ↾_{𝑠} T)$
225	9 36 18 68 22 110	ply1degltdim	$⊢ φ \to \dim (P ↾_{𝑠} T) = D (M (A))$
226	224 225	eqtrd	$⊢ φ \to \dim (H “_{𝑠} P) = D (M (A))$

Metamath Proof Explorer

Theorem algextdeglem8

Proof