This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 |`s F )
algextdeg.l 
|- L = ( E |`s ( E fldGen ( F u. { A } ) ) )
algextdeg.d 
|- D = ( deg1 ` E )
algextdeg.m 
|- M = ( E minPoly F )
algextdeg.f 
|- ( ph -> E e. Field )
algextdeg.e 
|- ( ph -> F e. ( SubDRing ` E ) )
algextdeg.a 
|- ( ph -> A e. ( E IntgRing F ) )
algextdeglem.o 
|- O = ( E evalSub1 F )
algextdeglem.y 
|- P = ( Poly1 ` K )
algextdeglem.u 
|- U = ( Base ` P )
algextdeglem.g 
|- G = ( p e. U |-> ( ( O ` p ) ` A ) )
algextdeglem.n 
|- N = ( x e. U |-> [ x ] ( P ~QG Z ) )
algextdeglem.z 
|- Z = ( `' G " { ( 0g ` L ) } )
algextdeglem.q 
|- Q = ( P /s ( P ~QG Z ) )
algextdeglem.j 
|- J = ( p e. ( Base ` Q ) |-> U. ( G " p ) )
algextdeglem.r 
|- R = ( rem1p ` K )
algextdeglem.h 
|- H = ( p e. U |-> ( p R ( M ` A ) ) )
algextdeglem.t 
|- T = ( `' ( deg1 ` K ) " ( -oo [,) ( D ` ( M ` A ) ) ) )
Assertion algextdeglem8 
|- ( ph -> ( dim ` ( H "s P ) ) = ( D ` ( M ` A ) ) )

Proof

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