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	$$⊢K=E{\upharpoonright }_{𝑠}F$$
	rtelextdg2.2	$$⊢L=E{\upharpoonright }_{𝑠}\left(E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)\right)$$
	rtelextdg2.3	$$⊢\underset{\dot{}}{0}=0_E$$
	rtelextdg2.4	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
	rtelextdg2.5	$$⊢V={\mathrm{Base}}_E$$
	rtelextdg2.6	$$⊢\underset{\dot{}}{·}={\cdot }_E$$
	rtelextdg2.7	$$⊢\underset{\dot{}}{+}={+}_E$$
	rtelextdg2.8	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_E}$$
	rtelextdg2.9	$$⊢\phi \to E\in \mathrm{Field}$$
	rtelextdg2.10	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	rtelextdg2.11	$$⊢\phi \to X\in V$$
	rtelextdg2.12	$$⊢\phi \to A\in F$$
	rtelextdg2.13	$$⊢\phi \to B\in F$$
	rtelextdg2.14	$$⊢\phi \to \left(2\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B\right)=\underset{\dot{}}{0}$$
Assertion	rtelextdg2	$$⊢\phi \to \left(X\in F\vee L\left[.:.\right]K=2\right)$$

Proof

Step	Hyp	Ref	Expression
1		rtelextdg2.1	$$⊢K=E{\upharpoonright }_{𝑠}F$$
2		rtelextdg2.2	$$⊢L=E{\upharpoonright }_{𝑠}\left(E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)\right)$$
3		rtelextdg2.3	$$⊢\underset{\dot{}}{0}=0_E$$
4		rtelextdg2.4	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
5		rtelextdg2.5	$$⊢V={\mathrm{Base}}_E$$
6		rtelextdg2.6	$$⊢\underset{\dot{}}{·}={\cdot }_E$$
7		rtelextdg2.7	$$⊢\underset{\dot{}}{+}={+}_E$$
8		rtelextdg2.8	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_E}$$
9		rtelextdg2.9	$$⊢\phi \to E\in \mathrm{Field}$$
10		rtelextdg2.10	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
11		rtelextdg2.11	$$⊢\phi \to X\in V$$
12		rtelextdg2.12	$$⊢\phi \to A\in F$$
13		rtelextdg2.13	$$⊢\phi \to B\in F$$
14		rtelextdg2.14	$$⊢\phi \to \left(2\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B\right)=\underset{\dot{}}{0}$$
15	9	flddrngd	$$⊢\phi \to E\in \mathrm{DivRing}$$
16	5	sdrgss	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\subseteq V$$
17	10 16	syl	$$⊢\phi \to F\subseteq V$$
18	11	snssd	$$⊢\phi \to \left\{X\right\}\subseteq V$$
19	17 18	unssd	$$⊢\phi \to F\cup \left\{X\right\}\subseteq V$$
20	5 15 19	fldgenssid	$$⊢\phi \to F\cup \left\{X\right\}\subseteq E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)$$
21		ssun2	$$⊢\left\{X\right\}\subseteq F\cup \left\{X\right\}$$
22		snidg	$$⊢X\in V\to X\in \left\{X\right\}$$
23	11 22	syl	$$⊢\phi \to X\in \left\{X\right\}$$
24	21 23	sselid	$$⊢\phi \to X\in \left(F\cup \left\{X\right\}\right)$$
25	20 24	sseldd	$$⊢\phi \to X\in \left(E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)\right)$$
26	25	adantr	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to X\in \left(E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)\right)$$
27	5 1 2 9 10 18	fldgenfldext	$$⊢\phi \to L{/}_{\mathrm{FldExt}}K$$
28		extdg1id	$$⊢\left(L{/}_{\mathrm{FldExt}}K\wedge L\left[.:.\right]K=1\right)\to L=K$$
29	27 28	sylan	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to L=K$$
30	29	fveq2d	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to {\mathrm{Base}}_L={\mathrm{Base}}_K$$
31	5 15 19	fldgenssv	$$⊢\phi \to E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)\subseteq V$$
32	2 5	ressbas2	$$⊢E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)\subseteq V\to E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)={\mathrm{Base}}_L$$
33	31 32	syl	$$⊢\phi \to E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)={\mathrm{Base}}_L$$
34	33	adantr	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)={\mathrm{Base}}_L$$
35	1 5	ressbas2	$$⊢F\subseteq V\to F={\mathrm{Base}}_K$$
36	17 35	syl	$$⊢\phi \to F={\mathrm{Base}}_K$$
37	36	adantr	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to F={\mathrm{Base}}_K$$
38	30 34 37	3eqtr4d	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to E\mathrm{fldGen}\left(F\cup \left\{X\right\}\right)=F$$
39	26 38	eleqtrd	$$⊢\left(\phi \wedge L\left[.:.\right]K=1\right)\to X\in F$$
40		simpr	$$⊢\left(\phi \wedge L\left[.:.\right]K=2\right)\to L\left[.:.\right]K=2$$
41		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
42		2z	$$⊢2\in \mathbb{Z}$$
43	42	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
44		extdgcl	$$⊢L{/}_{\mathrm{FldExt}}K\to L\left[.:.\right]K\in {\mathbb{N}}_0^{*}$$
45	27 44	syl	$$⊢\phi \to L\left[.:.\right]K\in {\mathbb{N}}_0^{*}$$
46		2nn0	$$⊢2\in {\mathbb{N}}_0$$
47	46	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
48		eqid	$$⊢{\mathrm{var}}_1\left(K\right)={\mathrm{var}}_1\left(K\right)$$
49		eqid	$$⊢{+}_P={+}_P$$
50		eqid	$$⊢{\cdot }_P={\cdot }_P$$
51		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
52		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
53		eqid	$$⊢\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(K\right)\right){+}_P\left(\left(\mathrm{algSc}\left(P\right)\left(A\right){\cdot }_P{\mathrm{var}}_1\left(K\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)=\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(K\right)\right){+}_P\left(\left(\mathrm{algSc}\left(P\right)\left(A\right){\cdot }_P{\mathrm{var}}_1\left(K\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)$$
54	1 2 3 4 5 6 7 8 9 10 11 12 13 14 48 49 50 51 52 53	rtelextdg2lem	$$⊢\phi \to L\left[.:.\right]K\le 2$$
55		xnn0lenn0nn0	$$⊢\left(L\left[.:.\right]K\in {\mathbb{N}}_0^{*}\wedge 2\in {\mathbb{N}}_0\wedge L\left[.:.\right]K\le 2\right)\to L\left[.:.\right]K\in {\mathbb{N}}_0$$
56	45 47 54 55	syl3anc	$$⊢\phi \to L\left[.:.\right]K\in {\mathbb{N}}_0$$
57	56	nn0zd	$$⊢\phi \to L\left[.:.\right]K\in \mathbb{Z}$$
58		extdggt0	$$⊢L{/}_{\mathrm{FldExt}}K\to 0<L\left[.:.\right]K$$
59	27 58	syl	$$⊢\phi \to 0<L\left[.:.\right]K$$
60		zgt0ge1	$$⊢L\left[.:.\right]K\in \mathbb{Z}\to \left(0<L\left[.:.\right]K\leftrightarrow 1\le L\left[.:.\right]K\right)$$
61	60	biimpa	$$⊢\left(L\left[.:.\right]K\in \mathbb{Z}\wedge 0<L\left[.:.\right]K\right)\to 1\le L\left[.:.\right]K$$
62	57 59 61	syl2anc	$$⊢\phi \to 1\le L\left[.:.\right]K$$
63	41 43 57 62 54	elfzd	$$⊢\phi \to L\left[.:.\right]K\in \left(1\dots 2\right)$$
64		fz12pr	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$
65	63 64	eleqtrdi	$$⊢\phi \to L\left[.:.\right]K\in \left\{1,2\right\}$$
66		elpri	$$⊢L\left[.:.\right]K\in \left\{1,2\right\}\to \left(L\left[.:.\right]K=1\vee L\left[.:.\right]K=2\right)$$
67	65 66	syl	$$⊢\phi \to \left(L\left[.:.\right]K=1\vee L\left[.:.\right]K=2\right)$$
68	39 40 67	orim12da	$$⊢\phi \to \left(X\in F\vee L\left[.:.\right]K=2\right)$$