algextdeg

Description: The degree of an algebraic field extension (noted [ L : K ] ) is the degree of the minimal polynomial M ( A ) , whereas L is the field generated by K and the algebraic element A . Part of Proposition 1.4 of Lang, p. 225. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	algextdeg.k	⊢ 𝐾 = ( 𝐸 ↾_s 𝐹 )
	algextdeg.l	⊢ 𝐿 = ( 𝐸 ↾_s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
	algextdeg.d	⊢ 𝐷 = ( deg₁ ‘ 𝐸 )
	algextdeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	algextdeg.f	⊢ ( 𝜑 → 𝐸 ∈ Field )
	algextdeg.e	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	algextdeg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
Assertion	algextdeg	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) = ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	⊢ 𝐾 = ( 𝐸 ↾_s 𝐹 )
2		algextdeg.l	⊢ 𝐿 = ( 𝐸 ↾_s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
3		algextdeg.d	⊢ 𝐷 = ( deg₁ ‘ 𝐸 )
4		algextdeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
5		algextdeg.f	⊢ ( 𝜑 → 𝐸 ∈ Field )
6		algextdeg.e	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
7		algextdeg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
8		eqid	⊢ ( 𝐸 evalSub₁ 𝐹 ) = ( 𝐸 evalSub₁ 𝐹 )
9		eqid	⊢ ( Poly₁ ‘ 𝐾 ) = ( Poly₁ ‘ 𝐾 )
10		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) = ( Base ‘ ( Poly₁ ‘ 𝐾 ) )
11		fveq2	⊢ ( 𝑞 = 𝑝 → ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) = ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) )
12	11	fveq1d	⊢ ( 𝑞 = 𝑝 → ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) )
13	12	cbvmptv	⊢ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑝 ) ‘ 𝐴 ) )
14		eceq1	⊢ ( 𝑦 = 𝑥 → [ 𝑦 ] ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) = [ 𝑥 ] ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) )
15	14	cbvmptv	⊢ ( 𝑦 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ [ 𝑦 ] ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) ) = ( 𝑥 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ [ 𝑥 ] ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) )
16		eqid	⊢ ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) = ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } )
17		eqid	⊢ ( ( Poly₁ ‘ 𝐾 ) /_s ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) ) = ( ( Poly₁ ‘ 𝐾 ) /_s ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) )
18		imaeq2	⊢ ( 𝑟 = 𝑝 → ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ 𝑟 ) = ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ 𝑝 ) )
19	18	unieqd	⊢ ( 𝑟 = 𝑝 → ∪ ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ 𝑟 ) = ∪ ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ 𝑝 ) )
20	19	cbvmptv	⊢ ( 𝑟 ∈ ( Base ‘ ( ( Poly₁ ‘ 𝐾 ) /_s ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) ) ) ↦ ∪ ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ 𝑟 ) ) = ( 𝑝 ∈ ( Base ‘ ( ( Poly₁ ‘ 𝐾 ) /_s ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) ) ) ↦ ∪ ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ 𝑝 ) )
21		eqid	⊢ ( rem_1p ‘ 𝐾 ) = ( rem_1p ‘ 𝐾 )
22		oveq1	⊢ ( 𝑞 = 𝑝 → ( 𝑞 ( rem_1p ‘ 𝐾 ) ( 𝑀 ‘ 𝐴 ) ) = ( 𝑝 ( rem_1p ‘ 𝐾 ) ( 𝑀 ‘ 𝐴 ) ) )
23	22	cbvmptv	⊢ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( 𝑞 ( rem_1p ‘ 𝐾 ) ( 𝑀 ‘ 𝐴 ) ) ) = ( 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( 𝑝 ( rem_1p ‘ 𝐾 ) ( 𝑀 ‘ 𝐴 ) ) )
24	1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 21 23	algextdeglem6	⊢ ( 𝜑 → ( dim ‘ ( ( Poly₁ ‘ 𝐾 ) /_s ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) ) ) = ( dim ‘ ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( 𝑞 ( rem_1p ‘ 𝐾 ) ( 𝑀 ‘ 𝐴 ) ) ) “_s ( Poly₁ ‘ 𝐾 ) ) ) )
25	1 2 3 4 5 6 7 8 9 10 13 15 16 17 20	algextdeglem4	⊢ ( 𝜑 → ( dim ‘ ( ( Poly₁ ‘ 𝐾 ) /_s ( ( Poly₁ ‘ 𝐾 ) ~_QG ( ^◡ ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) ) “ { ( 0_g ‘ 𝐿 ) } ) ) ) ) = ( 𝐿 [:] 𝐾 ) )
26		eqid	⊢ ( ^◡ ( deg₁ ‘ 𝐾 ) “ ( -∞ [,) ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) ) = ( ^◡ ( deg₁ ‘ 𝐾 ) “ ( -∞ [,) ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
27	1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 21 23 26	algextdeglem8	⊢ ( 𝜑 → ( dim ‘ ( ( 𝑞 ∈ ( Base ‘ ( Poly₁ ‘ 𝐾 ) ) ↦ ( 𝑞 ( rem_1p ‘ 𝐾 ) ( 𝑀 ‘ 𝐴 ) ) ) “_s ( Poly₁ ‘ 𝐾 ) ) ) = ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) )
28	24 25 27	3eqtr3d	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) = ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem algextdeg

Proof