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 ⊢ 𝐾 = ( 𝐸 ↾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 algextdeglem8 ( 𝜑 → ( dim ‘ ( 𝐻 “s 𝑃 ) ) = ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) )

Proof

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