Theorem rtelextdg2

Description: If an element X is a solution of a quadratic equation, then it is either in the base field, or the degree of its field extension is exactly 2. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	rtelextdg2.1	⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
	rtelextdg2.2	⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
	rtelextdg2.3	⊢ 0 = ( 0g ‘ 𝐸 )
	rtelextdg2.4	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
	rtelextdg2.5	⊢ 𝑉 = ( Base ‘ 𝐸 )
	rtelextdg2.6	⊢ · = ( .r ‘ 𝐸 )
	rtelextdg2.7	⊢ + = ( +g ‘ 𝐸 )
	rtelextdg2.8	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐸 ) )
	rtelextdg2.9	⊢ ( 𝜑 → 𝐸 ∈ Field )
	rtelextdg2.10	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	rtelextdg2.11	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	rtelextdg2.12	⊢ ( 𝜑 → 𝐴 ∈ 𝐹 )
	rtelextdg2.13	⊢ ( 𝜑 → 𝐵 ∈ 𝐹 )
	rtelextdg2.14	⊢ ( 𝜑 → ( ( 2 ↑ 𝑋 ) + ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = 0 )
Assertion	rtelextdg2	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )

Proof

Step	Hyp	Ref	Expression
1		rtelextdg2.1	⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
2		rtelextdg2.2	⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
3		rtelextdg2.3	⊢ 0 = ( 0g ‘ 𝐸 )
4		rtelextdg2.4	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
5		rtelextdg2.5	⊢ 𝑉 = ( Base ‘ 𝐸 )
6		rtelextdg2.6	⊢ · = ( .r ‘ 𝐸 )
7		rtelextdg2.7	⊢ + = ( +g ‘ 𝐸 )
8		rtelextdg2.8	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐸 ) )
9		rtelextdg2.9	⊢ ( 𝜑 → 𝐸 ∈ Field )
10		rtelextdg2.10	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
11		rtelextdg2.11	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
12		rtelextdg2.12	⊢ ( 𝜑 → 𝐴 ∈ 𝐹 )
13		rtelextdg2.13	⊢ ( 𝜑 → 𝐵 ∈ 𝐹 )
14		rtelextdg2.14	⊢ ( 𝜑 → ( ( 2 ↑ 𝑋 ) + ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = 0 )
15	9	flddrngd	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
16	5	sdrgss	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ⊆ 𝑉 )
17	10 16	syl	⊢ ( 𝜑 → 𝐹 ⊆ 𝑉 )
18	11	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
19	17 18	unssd	⊢ ( 𝜑 → ( 𝐹 ∪ { 𝑋 } ) ⊆ 𝑉 )
20	5 15 19	fldgenssid	⊢ ( 𝜑 → ( 𝐹 ∪ { 𝑋 } ) ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
21		ssun2	⊢ { 𝑋 } ⊆ ( 𝐹 ∪ { 𝑋 } )
22		snidg	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
23	11 22	syl	⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
24	21 23	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 ∪ { 𝑋 } ) )
25	20 24	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → 𝑋 ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) )
27	5 1 2 9 10 18	fldgenfldext	⊢ ( 𝜑 → 𝐿 /FldExt 𝐾 )
28		extdg1id	⊢ ( ( 𝐿 /FldExt 𝐾 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → 𝐿 = 𝐾 )
29	27 28	sylan	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → 𝐿 = 𝐾 )
30	29	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → ( Base ‘ 𝐿 ) = ( Base ‘ 𝐾 ) )
31	5 15 19	fldgenssv	⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) ⊆ 𝑉 )
32	2 5	ressbas2	⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) ⊆ 𝑉 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) = ( Base ‘ 𝐿 ) )
33	31 32	syl	⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) = ( Base ‘ 𝐿 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) = ( Base ‘ 𝐿 ) )
35	1 5	ressbas2	⊢ ( 𝐹 ⊆ 𝑉 → 𝐹 = ( Base ‘ 𝐾 ) )
36	17 35	syl	⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐾 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → 𝐹 = ( Base ‘ 𝐾 ) )
38	30 34 37	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝑋 } ) ) = 𝐹 )
39	26 38	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 1 ) → 𝑋 ∈ 𝐹 )
40		simpr	⊢ ( ( 𝜑 ∧ ( 𝐿 [:] 𝐾 ) = 2 ) → ( 𝐿 [:] 𝐾 ) = 2 )
41		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
42		2z	⊢ 2 ∈ ℤ
43	42	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
44		extdgcl	⊢ ( 𝐿 /FldExt 𝐾 → ( 𝐿 [:] 𝐾 ) ∈ ℕ0* )
45	27 44	syl	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ∈ ℕ0* )
46		2nn0	⊢ 2 ∈ ℕ0
47	46	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
48		eqid	⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
49		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
50		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
51		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
52		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
53		eqid	⊢ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ 𝑃 ) ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝐴 ) ( .r ‘ 𝑃 ) ( var1 ‘ 𝐾 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) = ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ 𝑃 ) ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝐴 ) ( .r ‘ 𝑃 ) ( var1 ‘ 𝐾 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) )
54	1 2 3 4 5 6 7 8 9 10 11 12 13 14 48 49 50 51 52 53	rtelextdg2lem	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ≤ 2 )
55		xnn0lenn0nn0	⊢ ( ( ( 𝐿 [:] 𝐾 ) ∈ ℕ0* ∧ 2 ∈ ℕ0 ∧ ( 𝐿 [:] 𝐾 ) ≤ 2 ) → ( 𝐿 [:] 𝐾 ) ∈ ℕ0 )
56	45 47 54 55	syl3anc	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ∈ ℕ0 )
57	56	nn0zd	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ∈ ℤ )
58		extdggt0	⊢ ( 𝐿 /FldExt 𝐾 → 0 < ( 𝐿 [:] 𝐾 ) )
59	27 58	syl	⊢ ( 𝜑 → 0 < ( 𝐿 [:] 𝐾 ) )
60		zgt0ge1	⊢ ( ( 𝐿 [:] 𝐾 ) ∈ ℤ → ( 0 < ( 𝐿 [:] 𝐾 ) ↔ 1 ≤ ( 𝐿 [:] 𝐾 ) ) )
61	60	biimpa	⊢ ( ( ( 𝐿 [:] 𝐾 ) ∈ ℤ ∧ 0 < ( 𝐿 [:] 𝐾 ) ) → 1 ≤ ( 𝐿 [:] 𝐾 ) )
62	57 59 61	syl2anc	⊢ ( 𝜑 → 1 ≤ ( 𝐿 [:] 𝐾 ) )
63	41 43 57 62 54	elfzd	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ∈ ( 1 ... 2 ) )
64		fz12pr	⊢ ( 1 ... 2 ) = { 1 , 2 }
65	63 64	eleqtrdi	⊢ ( 𝜑 → ( 𝐿 [:] 𝐾 ) ∈ { 1 , 2 } )
66		elpri	⊢ ( ( 𝐿 [:] 𝐾 ) ∈ { 1 , 2 } → ( ( 𝐿 [:] 𝐾 ) = 1 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
67	65 66	syl	⊢ ( 𝜑 → ( ( 𝐿 [:] 𝐾 ) = 1 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )
68	39 40 67	orim12da	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐹 ∨ ( 𝐿 [:] 𝐾 ) = 2 ) )