Theorem rtelextdg2lem

Description: Lemma for rtelextdg2 : If an element X is a solution of a quadratic equation, then the degree of its field extension is at most 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}$$
	rtelextdg2lem.1	$$⊢Y={\mathrm{var}}_1\left(K\right)$$
	rtelextdg2lem.2	$$⊢\underset{\dot{}}{\oplus }={+}_P$$
	rtelextdg2lem.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_P$$
	rtelextdg2lem.4	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	rtelextdg2lem.5	$$⊢U=\mathrm{algSc}\left(P\right)$$
	rtelextdg2lem.6	$$⊢G=\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)$$
Assertion	rtelextdg2lem	$$⊢\phi \to L\left[.:.\right]K\le 2$$

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		rtelextdg2lem.1	$$⊢Y={\mathrm{var}}_1\left(K\right)$$
16		rtelextdg2lem.2	$$⊢\underset{\dot{}}{\oplus }={+}_P$$
17		rtelextdg2lem.3	$$⊢\underset{\dot{}}{\otimes }={\cdot }_P$$
18		rtelextdg2lem.4	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_P}$$
19		rtelextdg2lem.5	$$⊢U=\mathrm{algSc}\left(P\right)$$
20		rtelextdg2lem.6	$$⊢G=\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)$$
21		eqid	$$⊢{\mathrm{deg}}_1\left(E\right)={\mathrm{deg}}_1\left(E\right)$$
22		eqid	$$⊢E\mathrm{minPoly}F=E\mathrm{minPoly}F$$
23		fveq2	$$⊢p=G\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)=\left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)$$
24	23	fveq1d	$$⊢p=G\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(X\right)=\left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)\left(X\right)$$
25	24	eqeq1d	$$⊢p=G\to \left(\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(X\right)=\underset{\dot{}}{0}\leftrightarrow \left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)\left(X\right)=\underset{\dot{}}{0}\right)$$
26		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
27		fldsdrgfld	$$⊢\left(E\in \mathrm{Field}\wedge F\in \mathrm{SubDRing}\left(E\right)\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{Field}$$
28	9 10 27	syl2anc	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{Field}$$
29	28	fldcrngd	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{CRing}$$
30	1 29	eqeltrid	$$⊢\phi \to K\in \mathrm{CRing}$$
31	30	crngringd	$$⊢\phi \to K\in \mathrm{Ring}$$
32	4	ply1ring	$$⊢K\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
33	31 32	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
34	33	ringgrpd	$$⊢\phi \to P\in \mathrm{Grp}$$
35		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
36	35 26	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
37	35	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
38	33 37	syl	$$⊢\phi \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
39		2nn0	$$⊢2\in {\mathbb{N}}_0$$
40	39	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
41	15 4 26	vr1cl	$$⊢K\in \mathrm{Ring}\to Y\in {\mathrm{Base}}_P$$
42	31 41	syl	$$⊢\phi \to Y\in {\mathrm{Base}}_P$$
43	36 18 38 40 42	mulgnn0cld	$$⊢\phi \to 2\underset{\dot{}}{\wedge }Y\in {\mathrm{Base}}_P$$
44	9	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
45		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
46	10 45	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
47	4 1 19 26 44 46 12	ressasclcl	$$⊢\phi \to U\left(A\right)\in {\mathrm{Base}}_P$$
48	26 17 33 47 42	ringcld	$$⊢\phi \to U\left(A\right)\underset{\dot{}}{\otimes }Y\in {\mathrm{Base}}_P$$
49	4 1 19 26 44 46 13	ressasclcl	$$⊢\phi \to U\left(B\right)\in {\mathrm{Base}}_P$$
50	26 16 34 48 49	grpcld	$$⊢\phi \to \left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\in {\mathrm{Base}}_P$$
51	26 16 34 43 50	grpcld	$$⊢\phi \to \left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\in {\mathrm{Base}}_P$$
52	20 51	eqeltrid	$$⊢\phi \to G\in {\mathrm{Base}}_P$$
53	20	fveq2i	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)$$
54	53	fveq1i	$$⊢{\mathrm{coe}}_1\left(G\right)\left(2\right)={\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(2\right)$$
55		eqid	$$⊢{+}_K={+}_K$$
56	4 26 16 55	coe1addfv	$$⊢\left(\left(K\in \mathrm{Ring}\wedge 2\underset{\dot{}}{\wedge }Y\in {\mathrm{Base}}_P\wedge \left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\in {\mathrm{Base}}_P\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(2\right)={\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(2\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(2\right)$$
57	31 43 50 40 56	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(2\right)={\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(2\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(2\right)$$
58		eqid	$$⊢0_K=0_K$$
59		eqid	$$⊢1_K=1_K$$
60	4 15 18 31 40 58 59	coe1mon	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=2,1_K,0_K\right)\right)$$
61		simpr	$$⊢\left(\phi \wedge i=2\right)\to i=2$$
62	61	iftrued	$$⊢\left(\phi \wedge i=2\right)\to if\left(i=2,1_K,0_K\right)=1_K$$
63		fvexd	$$⊢\phi \to 1_K\in \mathrm{V}$$
64	60 62 40 63	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(2\right)=1_K$$
65	4 26 16 55	coe1addfv	$$⊢\left(\left(K\in \mathrm{Ring}\wedge U\left(A\right)\underset{\dot{}}{\otimes }Y\in {\mathrm{Base}}_P\wedge U\left(B\right)\in {\mathrm{Base}}_P\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(2\right)={\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(2\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(2\right)$$
66	31 48 49 40 65	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(2\right)={\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(2\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(2\right)$$
67	5	sdrgss	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\subseteq V$$
68	1 5	ressbas2	$$⊢F\subseteq V\to F={\mathrm{Base}}_K$$
69	10 67 68	3syl	$$⊢\phi \to F={\mathrm{Base}}_K$$
70	12 69	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_K$$
71		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
72		eqid	$$⊢{\cdot }_K={\cdot }_K$$
73	4 26 71 19 17 72	coe1sclmulfv	$$⊢\left(K\in \mathrm{Ring}\wedge \left(A\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_P\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(2\right)=A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(2\right)$$
74	31 70 42 40 73	syl121anc	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(2\right)=A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(2\right)$$
75	4 15 31 58 59	coe1vr1	$$⊢\phi \to {\mathrm{coe}}_1\left(Y\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=1,1_K,0_K\right)\right)$$
76		1ne2	$$⊢1\ne 2$$
77	76	nesymi	$$⊢\neg 2=1$$
78		eqeq1	$$⊢i=2\to \left(i=1\leftrightarrow 2=1\right)$$
79	77 78	mtbiri	$$⊢i=2\to \neg i=1$$
80	79	adantl	$$⊢\left(\phi \wedge i=2\right)\to \neg i=1$$
81	80	iffalsed	$$⊢\left(\phi \wedge i=2\right)\to if\left(i=1,1_K,0_K\right)=0_K$$
82		fvexd	$$⊢\phi \to 0_K\in \mathrm{V}$$
83	75 81 40 82	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(Y\right)\left(2\right)=0_K$$
84	83	oveq2d	$$⊢\phi \to A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(2\right)=A{\cdot }_K{0}_K$$
85	71 72 58 31 70	ringrzd	$$⊢\phi \to A{\cdot }_K{0}_K=0_K$$
86	74 84 85	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(2\right)=0_K$$
87	13 69	eleqtrd	$$⊢\phi \to B\in {\mathrm{Base}}_K$$
88	4 19 71 58	coe1scl	$$⊢\left(K\in \mathrm{Ring}\wedge B\in {\mathrm{Base}}_K\right)\to {\mathrm{coe}}_1\left(U\left(B\right)\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=0,B,0_K\right)\right)$$
89	31 87 88	syl2anc	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(B\right)\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=0,B,0_K\right)\right)$$
90		0ne2	$$⊢0\ne 2$$
91	90	neii	$$⊢\neg 0=2$$
92		eqeq1	$$⊢i=0\to \left(i=2\leftrightarrow 0=2\right)$$
93	91 92	mtbiri	$$⊢i=0\to \neg i=2$$
94	93 61	nsyl3	$$⊢\left(\phi \wedge i=2\right)\to \neg i=0$$
95	94	iffalsed	$$⊢\left(\phi \wedge i=2\right)\to if\left(i=0,B,0_K\right)=0_K$$
96	89 95 40 82	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(B\right)\right)\left(2\right)=0_K$$
97	86 96	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(2\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(2\right)=0_K{+}_K{0}_K$$
98	31	ringgrpd	$$⊢\phi \to K\in \mathrm{Grp}$$
99	71 58	grpidcl	$$⊢K\in \mathrm{Grp}\to 0_K\in {\mathrm{Base}}_K$$
100	98 99	syl	$$⊢\phi \to 0_K\in {\mathrm{Base}}_K$$
101	71 55 58 98 100	grpridd	$$⊢\phi \to 0_K{+}_K{0}_K=0_K$$
102	66 97 101	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(2\right)=0_K$$
103	64 102	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(2\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(2\right)=1_K{+}_K{0}_K$$
104	71 59	ringidcl	$$⊢K\in \mathrm{Ring}\to 1_K\in {\mathrm{Base}}_K$$
105	31 104	syl	$$⊢\phi \to 1_K\in {\mathrm{Base}}_K$$
106	71 55 58 98 105	grpridd	$$⊢\phi \to 1_K{+}_K{0}_K=1_K$$
107	44	crngringd	$$⊢\phi \to E\in \mathrm{Ring}$$
108		eqid	$$⊢1_E=1_E$$
109	108	subrg1cl	$$⊢F\in \mathrm{SubRing}\left(E\right)\to 1_E\in F$$
110	46 109	syl	$$⊢\phi \to 1_E\in F$$
111	10 67	syl	$$⊢\phi \to F\subseteq V$$
112	1 5 108	ress1r	$$⊢\left(E\in \mathrm{Ring}\wedge 1_E\in F\wedge F\subseteq V\right)\to 1_E=1_K$$
113	107 110 111 112	syl3anc	$$⊢\phi \to 1_E=1_K$$
114	106 113	eqtr4d	$$⊢\phi \to 1_K{+}_K{0}_K=1_E$$
115	57 103 114	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(2\right)=1_E$$
116	54 115	eqtrid	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(2\right)=1_E$$
117	9	flddrngd	$$⊢\phi \to E\in \mathrm{DivRing}$$
118		drngnzr	$$⊢E\in \mathrm{DivRing}\to E\in \mathrm{NzRing}$$
119	108 3	nzrnz	$$⊢E\in \mathrm{NzRing}\to 1_E\ne \underset{\dot{}}{0}$$
120	117 118 119	3syl	$$⊢\phi \to 1_E\ne \underset{\dot{}}{0}$$
121	116 120	eqnetrd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(2\right)\ne \underset{\dot{}}{0}$$
122		fveq2	$$⊢G=0_P\to {\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(0_P\right)$$
123	122	fveq1d	$$⊢G=0_P\to {\mathrm{coe}}_1\left(G\right)\left(2\right)={\mathrm{coe}}_1\left(0_P\right)\left(2\right)$$
124		eqid	$$⊢0_P=0_P$$
125	4 124 58 31 40	coe1zfv	$$⊢\phi \to {\mathrm{coe}}_1\left(0_P\right)\left(2\right)=0_K$$
126	107	ringgrpd	$$⊢\phi \to E\in \mathrm{Grp}$$
127	126	grpmndd	$$⊢\phi \to E\in \mathrm{Mnd}$$
128		subrgsubg	$$⊢F\in \mathrm{SubRing}\left(E\right)\to F\in \mathrm{SubGrp}\left(E\right)$$
129	46 128	syl	$$⊢\phi \to F\in \mathrm{SubGrp}\left(E\right)$$
130	3	subg0cl	$$⊢F\in \mathrm{SubGrp}\left(E\right)\to \underset{\dot{}}{0}\in F$$
131	129 130	syl	$$⊢\phi \to \underset{\dot{}}{0}\in F$$
132	1 5 3	ress0g	$$⊢\left(E\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in F\wedge F\subseteq V\right)\to \underset{\dot{}}{0}=0_K$$
133	127 131 111 132	syl3anc	$$⊢\phi \to \underset{\dot{}}{0}=0_K$$
134	125 133	eqtr4d	$$⊢\phi \to {\mathrm{coe}}_1\left(0_P\right)\left(2\right)=\underset{\dot{}}{0}$$
135	123 134	sylan9eqr	$$⊢\left(\phi \wedge G=0_P\right)\to {\mathrm{coe}}_1\left(G\right)\left(2\right)=\underset{\dot{}}{0}$$
136	121 135	mteqand	$$⊢\phi \to G\ne 0_P$$
137	20	fveq2i	$$⊢{\mathrm{deg}}_1\left(K\right)\left(G\right)={\mathrm{deg}}_1\left(K\right)\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)$$
138		eqid	$$⊢{\mathrm{deg}}_1\left(K\right)={\mathrm{deg}}_1\left(K\right)$$
139		2re	$$⊢2\in ℝ$$
140	139	rexri	$$⊢2\in {ℝ}^{*}$$
141	140	a1i	$$⊢\phi \to 2\in {ℝ}^{*}$$
142	138 4 26	deg1xrcl	$$⊢U\left(A\right)\underset{\dot{}}{\otimes }Y\in {\mathrm{Base}}_P\to {\mathrm{deg}}_1\left(K\right)\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\in {ℝ}^{*}$$
143	48 142	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\in {ℝ}^{*}$$
144		1xr	$$⊢1\in {ℝ}^{*}$$
145	144	a1i	$$⊢\phi \to 1\in {ℝ}^{*}$$
146	138 4 71 26 17 19	deg1mul3le	$$⊢\left(K\in \mathrm{Ring}\wedge A\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_P\right)\to {\mathrm{deg}}_1\left(K\right)\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\le {\mathrm{deg}}_1\left(K\right)\left(Y\right)$$
147	31 70 42 146	syl3anc	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\le {\mathrm{deg}}_1\left(K\right)\left(Y\right)$$
148	1 28	eqeltrid	$$⊢\phi \to K\in \mathrm{Field}$$
149	148	flddrngd	$$⊢\phi \to K\in \mathrm{DivRing}$$
150		drngnzr	$$⊢K\in \mathrm{DivRing}\to K\in \mathrm{NzRing}$$
151	149 150	syl	$$⊢\phi \to K\in \mathrm{NzRing}$$
152	138 4 15 151	deg1vr	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(Y\right)=1$$
153	147 152	breqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\le 1$$
154		1lt2	$$⊢1<2$$
155	154	a1i	$$⊢\phi \to 1<2$$
156	143 145 141 153 155	xrlelttrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)<2$$
157	138 4 26	deg1xrcl	$$⊢U\left(B\right)\in {\mathrm{Base}}_P\to {\mathrm{deg}}_1\left(K\right)\left(U\left(B\right)\right)\in {ℝ}^{*}$$
158	49 157	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(B\right)\right)\in {ℝ}^{*}$$
159		0xr	$$⊢0\in {ℝ}^{*}$$
160	159	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
161	138 4 71 19	deg1sclle	$$⊢\left(K\in \mathrm{Ring}\wedge B\in {\mathrm{Base}}_K\right)\to {\mathrm{deg}}_1\left(K\right)\left(U\left(B\right)\right)\le 0$$
162	31 87 161	syl2anc	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(B\right)\right)\le 0$$
163		2pos	$$⊢0<2$$
164	163	a1i	$$⊢\phi \to 0<2$$
165	158 160 141 162 164	xrlelttrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(U\left(B\right)\right)<2$$
166	4 138 31 26 16 48 49 141 156 165	deg1addlt	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)<2$$
167	138 4 15 35 18	deg1pw	$$⊢\left(K\in \mathrm{NzRing}\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left(K\right)\left(2\underset{\dot{}}{\wedge }Y\right)=2$$
168	151 40 167	syl2anc	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(2\underset{\dot{}}{\wedge }Y\right)=2$$
169	166 168	breqtrrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)<{\mathrm{deg}}_1\left(K\right)\left(2\underset{\dot{}}{\wedge }Y\right)$$
170	4 138 31 26 16 43 50 169	deg1add	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)={\mathrm{deg}}_1\left(K\right)\left(2\underset{\dot{}}{\wedge }Y\right)$$
171	170 168	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)=2$$
172	137 171	eqtrid	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(G\right)=2$$
173	172	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left({\mathrm{deg}}_1\left(K\right)\left(G\right)\right)={\mathrm{coe}}_1\left(G\right)\left(2\right)$$
174	173 116 113	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left({\mathrm{deg}}_1\left(K\right)\left(G\right)\right)=1_K$$
175		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(K\right)={Monic}_{\mathrm{1p}}\left(K\right)$$
176	4 26 124 138 175 59	ismon1p	$$⊢G\in {Monic}_{\mathrm{1p}}\left(K\right)\leftrightarrow \left(G\in {\mathrm{Base}}_P\wedge G\ne 0_P\wedge {\mathrm{coe}}_1\left(G\right)\left({\mathrm{deg}}_1\left(K\right)\left(G\right)\right)=1_K\right)$$
177	52 136 174 176	syl3anbrc	$$⊢\phi \to G\in {Monic}_{\mathrm{1p}}\left(K\right)$$
178		eqid	$$⊢E{\mathrm{evalSub}}_{1}F=E{\mathrm{evalSub}}_{1}F$$
179		eqid	$$⊢{\mathrm{eval}}_1\left(E\right)={\mathrm{eval}}_1\left(E\right)$$
180	178 5 4 1 26 179 44 46	ressply1evl	$$⊢\phi \to E{\mathrm{evalSub}}_{1}F={{\mathrm{eval}}_1\left(E\right)\upharpoonright }_{{\mathrm{Base}}_P}$$
181	180	fveq1d	$$⊢\phi \to \left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)=\left({{\mathrm{eval}}_1\left(E\right)\upharpoonright }_{{\mathrm{Base}}_P}\right)\left(G\right)$$
182	52	fvresd	$$⊢\phi \to \left({{\mathrm{eval}}_1\left(E\right)\upharpoonright }_{{\mathrm{Base}}_P}\right)\left(G\right)={\mathrm{eval}}_1\left(E\right)\left(G\right)$$
183	181 182	eqtrd	$$⊢\phi \to \left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)={\mathrm{eval}}_1\left(E\right)\left(G\right)$$
184	183	fveq1d	$$⊢\phi \to \left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)\left(X\right)={\mathrm{eval}}_1\left(E\right)\left(G\right)\left(X\right)$$
185		eqid	$$⊢{\mathrm{Poly}}_1\left(E\right)={\mathrm{Poly}}_1\left(E\right)$$
186		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
187		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
188		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)\left(2\right)={\mathrm{coe}}_1\left(G\right)\left(2\right)$$
189		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)\left(1\right)={\mathrm{coe}}_1\left(G\right)\left(1\right)$$
190		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)\left(0\right)={\mathrm{coe}}_1\left(G\right)\left(0\right)$$
191		eqid	$$⊢{\mathrm{PwSer}}_1\left(K\right)={\mathrm{PwSer}}_1\left(K\right)$$
192		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}$$
193	185 1 4 26 46 191 192 186	ressply1bas2	$$⊢\phi \to {\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
194	52 193	eleqtrd	$$⊢\phi \to G\in \left({\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}\right)$$
195	194	elin2d	$$⊢\phi \to G\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
196	1 21 4 26 52 46	ressdeg1	$$⊢\phi \to {\mathrm{deg}}_1\left(E\right)\left(G\right)={\mathrm{deg}}_1\left(K\right)\left(G\right)$$
197	196 172	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(E\right)\left(G\right)=2$$
198	185 179 5 186 6 7 8 187 21 188 189 190 44 195 197 11	evl1deg2	$$⊢\phi \to {\mathrm{eval}}_1\left(E\right)\left(G\right)\left(X\right)=\left({\mathrm{coe}}_1\left(G\right)\left(2\right)\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)\right)\underset{\dot{}}{+}\left(\left({\mathrm{coe}}_1\left(G\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(G\right)\left(0\right)\right)$$
199	116	oveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(2\right)\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)=1_E\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)$$
200		eqid	$$⊢{\mathrm{mulGrp}}_E={\mathrm{mulGrp}}_E$$
201	200 5	mgpbas	$$⊢V={\mathrm{Base}}_{{\mathrm{mulGrp}}_E}$$
202	200	ringmgp	$$⊢E\in \mathrm{Ring}\to {\mathrm{mulGrp}}_E\in \mathrm{Mnd}$$
203	107 202	syl	$$⊢\phi \to {\mathrm{mulGrp}}_E\in \mathrm{Mnd}$$
204	201 8 203 40 11	mulgnn0cld	$$⊢\phi \to 2\underset{\dot{}}{\times }X\in V$$
205	5 6 108 107 204	ringlidmd	$$⊢\phi \to 1_E\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)=2\underset{\dot{}}{\times }X$$
206	199 205	eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(2\right)\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)=2\underset{\dot{}}{\times }X$$
207	53	fveq1i	$$⊢{\mathrm{coe}}_1\left(G\right)\left(1\right)={\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(1\right)$$
208		1nn0	$$⊢1\in {\mathbb{N}}_0$$
209	208	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
210	4 26 16 55	coe1addfv	$$⊢\left(\left(K\in \mathrm{Ring}\wedge 2\underset{\dot{}}{\wedge }Y\in {\mathrm{Base}}_P\wedge \left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\in {\mathrm{Base}}_P\right)\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(1\right)={\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(1\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(1\right)$$
211	31 43 50 209 210	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(1\right)={\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(1\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(1\right)$$
212	76	neii	$$⊢\neg 1=2$$
213		eqeq1	$$⊢i=1\to \left(i=2\leftrightarrow 1=2\right)$$
214	213	notbid	$$⊢i=1\to \left(\neg i=2\leftrightarrow \neg 1=2\right)$$
215	214	adantl	$$⊢\left(\phi \wedge i=1\right)\to \left(\neg i=2\leftrightarrow \neg 1=2\right)$$
216	212 215	mpbiri	$$⊢\left(\phi \wedge i=1\right)\to \neg i=2$$
217	216	iffalsed	$$⊢\left(\phi \wedge i=1\right)\to if\left(i=2,1_K,0_K\right)=0_K$$
218	60 217 209 82	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(1\right)=0_K$$
219	4 26 16 55	coe1addfv	$$⊢\left(\left(K\in \mathrm{Ring}\wedge U\left(A\right)\underset{\dot{}}{\otimes }Y\in {\mathrm{Base}}_P\wedge U\left(B\right)\in {\mathrm{Base}}_P\right)\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(1\right)={\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(1\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(1\right)$$
220	31 48 49 209 219	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(1\right)={\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(1\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(1\right)$$
221	4 26 71 19 17 72	coe1sclmulfv	$$⊢\left(K\in \mathrm{Ring}\wedge \left(A\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_P\right)\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(1\right)=A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(1\right)$$
222	31 70 42 209 221	syl121anc	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(1\right)=A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(1\right)$$
223		simpr	$$⊢\left(\phi \wedge i=1\right)\to i=1$$
224	223	iftrued	$$⊢\left(\phi \wedge i=1\right)\to if\left(i=1,1_K,0_K\right)=1_K$$
225	75 224 209 63	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(Y\right)\left(1\right)=1_K$$
226	225	oveq2d	$$⊢\phi \to A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(1\right)=A{\cdot }_K{1}_K$$
227	71 72 59 31 70	ringridmd	$$⊢\phi \to A{\cdot }_K{1}_K=A$$
228	222 226 227	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(1\right)=A$$
229		0ne1	$$⊢0\ne 1$$
230	229	nesymi	$$⊢\neg 1=0$$
231		eqeq1	$$⊢i=1\to \left(i=0\leftrightarrow 1=0\right)$$
232	230 231	mtbiri	$$⊢i=1\to \neg i=0$$
233	232	adantl	$$⊢\left(\phi \wedge i=1\right)\to \neg i=0$$
234	233	iffalsed	$$⊢\left(\phi \wedge i=1\right)\to if\left(i=0,B,0_K\right)=0_K$$
235	89 234 209 82	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(B\right)\right)\left(1\right)=0_K$$
236	228 235	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(1\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(1\right)=A{+}_K{0}_K$$
237	71 55 58 98 70	grpridd	$$⊢\phi \to A{+}_K{0}_K=A$$
238	220 236 237	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(1\right)=A$$
239	218 238	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(1\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(1\right)=0_K{+}_{K}A$$
240	71 55 58 98 70	grplidd	$$⊢\phi \to 0_K{+}_{K}A=A$$
241	211 239 240	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(1\right)=A$$
242	207 241	eqtrid	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(1\right)=A$$
243	242	oveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(1\right)\underset{\dot{}}{·}X=A\underset{\dot{}}{·}X$$
244	53	fveq1i	$$⊢{\mathrm{coe}}_1\left(G\right)\left(0\right)={\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(0\right)$$
245		0nn0	$$⊢0\in {\mathbb{N}}_0$$
246	245	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
247	4 26 16 55	coe1addfv	$$⊢\left(\left(K\in \mathrm{Ring}\wedge 2\underset{\dot{}}{\wedge }Y\in {\mathrm{Base}}_P\wedge \left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\in {\mathrm{Base}}_P\right)\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(0\right)={\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(0\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(0\right)$$
248	31 43 50 246 247	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(0\right)={\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(0\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(0\right)$$
249	93	adantl	$$⊢\left(\phi \wedge i=0\right)\to \neg i=2$$
250	249	iffalsed	$$⊢\left(\phi \wedge i=0\right)\to if\left(i=2,1_K,0_K\right)=0_K$$
251	60 250 246 82	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(0\right)=0_K$$
252	4 26 16 55	coe1addfv	$$⊢\left(\left(K\in \mathrm{Ring}\wedge U\left(A\right)\underset{\dot{}}{\otimes }Y\in {\mathrm{Base}}_P\wedge U\left(B\right)\in {\mathrm{Base}}_P\right)\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(0\right)={\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(0\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(0\right)$$
253	31 48 49 246 252	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(0\right)={\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(0\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(0\right)$$
254	4 26 71 19 17 72	coe1sclmulfv	$$⊢\left(K\in \mathrm{Ring}\wedge \left(A\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_P\right)\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(0\right)=A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(0\right)$$
255	31 70 42 246 254	syl121anc	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(0\right)=A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(0\right)$$
256	229	neii	$$⊢\neg 0=1$$
257		eqeq1	$$⊢i=0\to \left(i=1\leftrightarrow 0=1\right)$$
258	256 257	mtbiri	$$⊢i=0\to \neg i=1$$
259	258	adantl	$$⊢\left(\phi \wedge i=0\right)\to \neg i=1$$
260	259	iffalsed	$$⊢\left(\phi \wedge i=0\right)\to if\left(i=1,1_K,0_K\right)=0_K$$
261	75 260 246 82	fvmptd	$$⊢\phi \to {\mathrm{coe}}_1\left(Y\right)\left(0\right)=0_K$$
262	261	oveq2d	$$⊢\phi \to A{\cdot }_K{\mathrm{coe}}_1\left(Y\right)\left(0\right)=A{\cdot }_K{0}_K$$
263	255 262 85	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(0\right)=0_K$$
264	4 19 71	ply1sclid	$$⊢\left(K\in \mathrm{Ring}\wedge B\in {\mathrm{Base}}_K\right)\to B={\mathrm{coe}}_1\left(U\left(B\right)\right)\left(0\right)$$
265	31 87 264	syl2anc	$$⊢\phi \to B={\mathrm{coe}}_1\left(U\left(B\right)\right)\left(0\right)$$
266	265	eqcomd	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(B\right)\right)\left(0\right)=B$$
267	263 266	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\left(0\right){+}_K{\mathrm{coe}}_1\left(U\left(B\right)\right)\left(0\right)=0_K{+}_{K}B$$
268	71 55 58 98 87	grplidd	$$⊢\phi \to 0_K{+}_{K}B=B$$
269	253 267 268	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(0\right)=B$$
270	251 269	oveq12d	$$⊢\phi \to {\mathrm{coe}}_1\left(2\underset{\dot{}}{\wedge }Y\right)\left(0\right){+}_K{\mathrm{coe}}_1\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\left(0\right)=0_K{+}_{K}B$$
271	248 270 268	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\left(2\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\oplus }\left(\left(U\left(A\right)\underset{\dot{}}{\otimes }Y\right)\underset{\dot{}}{\oplus }U\left(B\right)\right)\right)\left(0\right)=B$$
272	244 271	eqtrid	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(0\right)=B$$
273	243 272	oveq12d	$$⊢\phi \to \left({\mathrm{coe}}_1\left(G\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(G\right)\left(0\right)=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
274	206 273	oveq12d	$$⊢\phi \to \left({\mathrm{coe}}_1\left(G\right)\left(2\right)\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)\right)\underset{\dot{}}{+}\left(\left({\mathrm{coe}}_1\left(G\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(G\right)\left(0\right)\right)=\left(2\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B\right)$$
275	274 14	eqtrd	$$⊢\phi \to \left({\mathrm{coe}}_1\left(G\right)\left(2\right)\underset{\dot{}}{·}\left(2\underset{\dot{}}{\times }X\right)\right)\underset{\dot{}}{+}\left(\left({\mathrm{coe}}_1\left(G\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(G\right)\left(0\right)\right)=\underset{\dot{}}{0}$$
276	184 198 275	3eqtrd	$$⊢\phi \to \left(E{\mathrm{evalSub}}_{1}F\right)\left(G\right)\left(X\right)=\underset{\dot{}}{0}$$
277	25 177 276	rspcedvdw	$$⊢\phi \to \exists p\in {Monic}_{\mathrm{1p}}\left(K\right)\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(X\right)=\underset{\dot{}}{0}$$
278	178 1 5 3 44 46	elirng	$$⊢\phi \to \left(X\in \left(E\mathrm{IntgRing}F\right)\leftrightarrow \left(X\in V\wedge \exists p\in {Monic}_{\mathrm{1p}}\left(K\right)\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
279	11 277 278	mpbir2and	$$⊢\phi \to X\in \left(E\mathrm{IntgRing}F\right)$$
280	1 2 21 22 9 10 279	algextdeg	$$⊢\phi \to L\left[.:.\right]K={\mathrm{deg}}_1\left(E\right)\left(\left(E\mathrm{minPoly}F\right)\left(X\right)\right)$$
281	1	fveq2i	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
282	4 281	eqtri	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
283		eqid	$$⊢\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(X\right)=\underset{\dot{}}{0}\right\}=\left\{q\in \mathrm{dom}\left(E{\mathrm{evalSub}}_{1}F\right)|\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(X\right)=\underset{\dot{}}{0}\right\}$$
284		eqid	$$⊢\mathrm{RSpan}\left(P\right)=\mathrm{RSpan}\left(P\right)$$
285		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
286	178 282 5 9 10 11 3 283 284 285 22	minplycl	$$⊢\phi \to \left(E\mathrm{minPoly}F\right)\left(X\right)\in {\mathrm{Base}}_P$$
287	1 21 4 26 286 46	ressdeg1	$$⊢\phi \to {\mathrm{deg}}_1\left(E\right)\left(\left(E\mathrm{minPoly}F\right)\left(X\right)\right)={\mathrm{deg}}_1\left(K\right)\left(\left(E\mathrm{minPoly}F\right)\left(X\right)\right)$$
288	280 287	eqtrd	$$⊢\phi \to L\left[.:.\right]K={\mathrm{deg}}_1\left(K\right)\left(\left(E\mathrm{minPoly}F\right)\left(X\right)\right)$$
289	1	fveq2i	$$⊢{\mathrm{deg}}_1\left(K\right)={\mathrm{deg}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
290	178 282 5 9 10 11 3 22 289 124 26 276 52 136	minplymindeg	$$⊢\phi \to {\mathrm{deg}}_1\left(K\right)\left(\left(E\mathrm{minPoly}F\right)\left(X\right)\right)\le {\mathrm{deg}}_1\left(K\right)\left(G\right)$$
291	288 290	eqbrtrd	$$⊢\phi \to L\left[.:.\right]K\le {\mathrm{deg}}_1\left(K\right)\left(G\right)$$
292	291 172	breqtrd	$$⊢\phi \to L\left[.:.\right]K\le 2$$