Metamath Proof Explorer

Theorem extdgfialg

Description: A finite field extension E / F is algebraic. Part of the proof of Proposition 1.1 of Lang, p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses extdgfialg.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
extdgfialg.d ⊢ 𝐷 = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) )
extdgfialg.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
extdgfialg.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
extdgfialg.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
Assertion extdgfialg ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 extdgfialg.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
2 extdgfialg.d ⊢ 𝐷 = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) )
3 extdgfialg.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
4 extdgfialg.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
5 extdgfialg.1 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
6 eqid ⊢ ( 𝐸 evalSub1 𝐹 ) = ( 𝐸 evalSub1 𝐹 )
7 eqid ⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
8 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
9 3 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
10 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
11 4 10 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
12 6 7 1 8 9 11 irngssv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ 𝐵 )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐸 ∈ Field )
14 13 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝐸 ∈ Field )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
16 15 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℕ0 )
18 17 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝐷 ∈ ℕ0 )
19 eqid ⊢ ( .r ‘ 𝐸 ) = ( .r ‘ 𝐸 )
20 oveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) = ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) )
21 20 cbvmptv ⊢ ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) = ( 𝑛 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
23 22 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝑥 ∈ 𝐵 )
24 ovexd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → ( 0 ... 𝐷 ) ∈ V )
25 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) )
26 24 16 25 elmaprd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝑎 : ( 0 ... 𝐷 ) ⟶ 𝐹 )
27 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝑎 finSupp ( 0g ‘ 𝐸 ) )
28 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) )
29 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) )
30 1 2 14 16 18 8 19 21 23 26 27 28 29 extdgfialglem2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
31 30 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ 𝐸 ) ) ∧ ( ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
32 31 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ) ∧ ( 𝑎 finSupp ( 0g ‘ 𝐸 ) ∧ ( ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
33 1 2 13 15 17 8 19 21 22 extdgfialglem1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ ( 𝐹 ↑m ( 0 ... 𝐷 ) ) ( 𝑎 finSupp ( 0g ‘ 𝐸 ) ∧ ( ( 𝐸 Σg ( 𝑎 ∘f ( .r ‘ 𝐸 ) ( 𝑚 ∈ ( 0 ... 𝐷 ) ↦ ( 𝑚 ( .g ‘ ( mulGrp ‘ ( ( subringAlg ‘ 𝐸 ) ‘ 𝐹 ) ) ) 𝑥 ) ) ) ) = ( 0g ‘ 𝐸 ) ∧ 𝑎 ≠ ( ( 0 ... 𝐷 ) × { ( 0g ‘ 𝐸 ) } ) ) ) )
34 32 33 r19.29a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
35 12 34 eqelssd ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = 𝐵 )