Metamath Proof Explorer

Theorem algextdeglem3

Description: Lemma for algextdeg . The quotient P / Z of the vector space P of polynomials by the subspace Z of polynomials annihilating A is itself a vector space. (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 ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
Assertion algextdeglem3 ( 𝜑 → 𝑄 ∈ LVec )

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 1 fveq2i ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
17 9 16 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
18 issdrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
19 6 18 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
20 19 simp3d ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
21 17 20 ply1lvec ⊢ ( 𝜑 → 𝑃 ∈ LVec )
22 eqidd ⊢ ( 𝜑 → ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) = ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) )
23 eqidd ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = ( 0g ‘ 𝐿 ) )
24 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
25 5 flddrngd ⊢ ( 𝜑 → 𝐸 ∈ DivRing )
26 19 simp2d ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
27 subrgsubg ⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
28 24 subgss ⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
29 26 27 28 3syl ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
30 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
31 5 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
32 8 1 24 30 31 26 irngssv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
33 32 7 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
34 33 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( Base ‘ 𝐸 ) )
35 29 34 unssd ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( Base ‘ 𝐸 ) )
36 24 25 35 fldgenssid ⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
37 36 unssad ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
38 24 25 35 fldgenssv ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) )
39 2 24 ressbas2 ⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) = ( Base ‘ 𝐿 ) )
40 38 39 syl ⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) = ( Base ‘ 𝐿 ) )
41 37 40 sseqtrd ⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐿 ) )
42 22 23 41 sralmod0 ⊢ ( 𝜑 → ( 0g ‘ 𝐿 ) = ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
43 42 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝐿 ) } = { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } )
44 43 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } ) = ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) )
45 13 44 eqtrid ⊢ ( 𝜑 → 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) )
46 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 algextdeglem2 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) )
47 eqid ⊢ ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) = ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } )
48 eqid ⊢ ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) = ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) )
49 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
50 47 48 49 lmhmkerlss ⊢ ( 𝐺 ∈ ( 𝑃 LMHom ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) → ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ∈ ( LSubSp ‘ 𝑃 ) )
51 46 50 syl ⊢ ( 𝜑 → ( ◡ 𝐺 “ { ( 0g ‘ ( ( subringAlg ‘ 𝐿 ) ‘ 𝐹 ) ) } ) ∈ ( LSubSp ‘ 𝑃 ) )
52 45 51 eqeltrd ⊢ ( 𝜑 → 𝑍 ∈ ( LSubSp ‘ 𝑃 ) )
53 14 21 52 quslvec ⊢ ( 𝜑 → 𝑄 ∈ LVec )