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	$⊢ B = {Base}_{E}$
	extdgfialg.d	$⊢ D = \dim (subringAlg (E) (F))$
	extdgfialg.e	$⊢ φ \to E \in Field$
	extdgfialg.f	$⊢ φ \to F \in SubDRing (E)$
	extdgfialg.1	$⊢ φ \to D \in ℕ_{0}$
Assertion	extdgfialg	$⊢ φ \to E IntgRing F = B$

Proof

Step	Hyp	Ref	Expression
1		extdgfialg.b	$⊢ B = {Base}_{E}$
2		extdgfialg.d	$⊢ D = \dim (subringAlg (E) (F))$
3		extdgfialg.e	$⊢ φ \to E \in Field$
4		extdgfialg.f	$⊢ φ \to F \in SubDRing (E)$
5		extdgfialg.1	$⊢ φ \to D \in ℕ_{0}$
6		eqid	$⊢ E {evalSub}_{1} F = E {evalSub}_{1} F$
7		eqid	$⊢ E ↾_{𝑠} F = E ↾_{𝑠} F$
8		eqid	$⊢ 0_{E} = 0_{E}$
9	3	fldcrngd	$⊢ φ \to E \in CRing$
10		sdrgsubrg	$⊢ F \in SubDRing (E) \to F \in SubRing (E)$
11	4 10	syl	$⊢ φ \to F \in SubRing (E)$
12	6 7 1 8 9 11	irngssv	$⊢ φ \to E IntgRing F \subseteq B$
13	3	adantr	$⊢ (φ \land x \in B) \to E \in Field$
14	13	ad4antr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to E \in Field$
15	4	adantr	$⊢ (φ \land x \in B) \to F \in SubDRing (E)$
16	15	ad4antr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to F \in SubDRing (E)$
17	5	adantr	$⊢ (φ \land x \in B) \to D \in ℕ_{0}$
18	17	ad4antr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to D \in ℕ_{0}$
19		eqid	$⊢ \cdot_{E} = \cdot_{E}$
20		oveq1	$⊢ m = n \to m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x = n \cdot_{{mulGrp}_{subringAlg (E) (F)}} x$
21	20	cbvmptv	$⊢ (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x) = (n \in (0 \dots D) ⟼ n \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)$
22		simpr	$⊢ (φ \land x \in B) \to x \in B$
23	22	ad4antr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to x \in B$
24		ovexd	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to (0 \dots D) \in V$
25		simp-4r	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to a \in (F^{(0 \dots D)})$
26	24 16 25	elmaprd	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to a : (0 \dots D) ⟶ F$
27		simpllr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to {finSupp}_{0_{E}} (a)$
28		simplr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}$
29		simpr	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to a \neq (0 \dots D) \times \{0_{E}\}$
30	1 2 14 16 18 8 19 21 23 26 27 28 29	extdgfialglem2	$⊢ (((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land \sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E}) \land a \neq (0 \dots D) \times \{0_{E}\}) \to x \in (E IntgRing F)$
31	30	anasss	$⊢ ((((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land {finSupp}_{0_{E}} (a)) \land (\sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E} \land a \neq (0 \dots D) \times \{0_{E}\})) \to x \in (E IntgRing F)$
32	31	anasss	$⊢ (((φ \land x \in B) \land a \in (F^{(0 \dots D)})) \land ({finSupp}_{0_{E}} (a) \land (\sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E} \land a \neq (0 \dots D) \times \{0_{E}\}))) \to x \in (E IntgRing F)$
33	1 2 13 15 17 8 19 21 22	extdgfialglem1	$⊢ (φ \land x \in B) \to \exists a \in (F^{(0 \dots D)}) ({finSupp}_{0_{E}} (a) \land (\sum_{E} (a {\cdot_{E}}_{f} (m \in (0 \dots D) ⟼ m \cdot_{{mulGrp}_{subringAlg (E) (F)}} x)) = 0_{E} \land a \neq (0 \dots D) \times \{0_{E}\}))$
34	32 33	r19.29a	$⊢ (φ \land x \in B) \to x \in (E IntgRing F)$
35	12 34	eqelssd	$⊢ φ \to E IntgRing F = B$

Metamath Proof Explorer

Theorem extdgfialg

Proof