Theorem rtelextdg2lem 33984

Description: Lemma for rtelextdg2 33985: If an element 𝑋 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.)

Hypotheses

Ref	Expression
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 )
rtelextdg2lem.1	⊢ 𝑌 = (var1‘𝐾)
rtelextdg2lem.2	⊢ ⊕ = (+g‘𝑃)
rtelextdg2lem.3	⊢ ⊗ = (.r‘𝑃)
rtelextdg2lem.4	⊢ ∧ = (.g‘(mulGrp‘𝑃))
rtelextdg2lem.5	⊢ 𝑈 = (algSc‘𝑃)
rtelextdg2lem.6	⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))

Assertion

Ref	Expression
rtelextdg2lem	⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)

Proof of Theorem rtelextdg2lem

Dummy variables 𝑖 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rtelextdg2.1	. . . . 5 ⊢ 𝐾 = (𝐸 ↾s 𝐹)
2		rtelextdg2.2	. . . . 5 ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝑋})))
3		eqid 2761	. . . . 5 ⊢ (deg1‘𝐸) = (deg1‘𝐸)
4		eqid 2761	. . . . 5 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
5		rtelextdg2.9	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Field)
6		rtelextdg2.10	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
7		rtelextdg2.11	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
8		fveq2 6862	. . . . . . . . 9 ⊢ (𝑝 = 𝐺 → ((𝐸 evalSub1 𝐹)‘𝑝) = ((𝐸 evalSub1 𝐹)‘𝐺))
9	8	fveq1d 6864	. . . . . . . 8 ⊢ (𝑝 = 𝐺 → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋))
10	9	eqeq1d 2763	. . . . . . 7 ⊢ (𝑝 = 𝐺 → ((((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 ↔ (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 ))
11		rtelextdg2lem.6	. . . . . . . . 9 ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))
12		eqid 2761	. . . . . . . . . 10 ⊢ (Base‘𝑃) = (Base‘𝑃)
13		rtelextdg2lem.2	. . . . . . . . . 10 ⊢ ⊕ = (+g‘𝑃)
14		fldsdrgfld 20835	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
15	5, 6, 14	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
16	15	fldcrngd 20779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing)
17	1, 16	eqeltrid 2865	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ CRing)
18	17	crngringd 20283	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
19		rtelextdg2.4	. . . . . . . . . . . . 13 ⊢ 𝑃 = (Poly1‘𝐾)
20	19	ply1ring 22297	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
21	18, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ Ring)
22	21	ringgrpd 20279	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
23		eqid 2761	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
24	23, 12	mgpbas 20182	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
25		rtelextdg2lem.4	. . . . . . . . . . 11 ⊢ ∧ = (.g‘(mulGrp‘𝑃))
26	23	ringmgp 20276	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
27	21, 26	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
28		2nn0 12492	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ0)
30		rtelextdg2lem.1	. . . . . . . . . . . . 13 ⊢ 𝑌 = (var1‘𝐾)
31	30, 19, 12	vr1cl 22267	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑌 ∈ (Base‘𝑃))
32	18, 31	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑃))
33	24, 25, 27, 29, 32	mulgnn0cld 19128	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∧ 𝑌) ∈ (Base‘𝑃))
34		rtelextdg2lem.3	. . . . . . . . . . . 12 ⊢ ⊗ = (.r‘𝑃)
35		rtelextdg2lem.5	. . . . . . . . . . . . 13 ⊢ 𝑈 = (algSc‘𝑃)
36	5	fldcrngd 20779	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37		sdrgsubrg 20828	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
38	6, 37	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
39		rtelextdg2.12	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝐹)
40	19, 1, 35, 12, 36, 38, 39	ressasclcl 33728	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘𝐴) ∈ (Base‘𝑃))
41	12, 34, 21, 40, 32	ringcld 20297	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃))
42		rtelextdg2.13	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐹)
43	19, 1, 35, 12, 36, 38, 42	ressasclcl 33728	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘𝐵) ∈ (Base‘𝑃))
44	12, 13, 22, 41, 43	grpcld 18980	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃))
45	12, 13, 22, 33, 44	grpcld 18980	. . . . . . . . 9 ⊢ (𝜑 → ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) ∈ (Base‘𝑃))
46	11, 45	eqeltrid 2865	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))
47	11	fveq2i 6865	. . . . . . . . . . . 12 ⊢ (coe1‘𝐺) = (coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
48	47	fveq1i 6863	. . . . . . . . . . 11 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2)
49		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐾) = (+g‘𝐾)
50	19, 12, 13, 49	coe1addfv 22316	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)))
51	18, 33, 44, 29, 50	syl31anc 1391	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)))
52		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐾) = (0g‘𝐾)
53		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝐾) = (1r‘𝐾)
54	19, 30, 25, 18, 29, 52, 53	coe1mon 33744	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (coe1‘(2 ∧ 𝑌)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾))))
55		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2)
56	55	iftrued 4485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
57		fvexd 6877	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ V)
58	54, 56, 29, 57	fvmptd 6978	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘2) = (1r‘𝐾))
59	19, 12, 13, 49	coe1addfv 22316	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)))
60	18, 41, 43, 29, 59	syl31anc 1391	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)))
61		rtelextdg2.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑉 = (Base‘𝐸)
62	61	sdrgss 20830	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝑉)
63	1, 61	ressbas2 17265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ⊆ 𝑉 → 𝐹 = (Base‘𝐾))
64	6, 62, 63	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
65	39, 64	eleqtrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐾))
66		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐾) = (Base‘𝐾)
67		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐾) = (.r‘𝐾)
68	19, 12, 66, 35, 34, 67	coe1sclmulfv 22334	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)))
69	18, 65, 32, 29, 68	syl121anc 1393	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)))
70	19, 30, 18, 52, 53	coe1vr1 33748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (coe1‘𝑌) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾))))
71		1ne2 12422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 2
72	71	nesymi 3013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 2 = 1
73		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → (𝑖 = 1 ↔ 2 = 1))
74	72, 73	mtbiri 329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 1)
75	74	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 1)
76	75	iffalsed 4488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
77		fvexd 6877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐾) ∈ V)
78	70, 76, 29, 77	fvmptd 6978	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘𝑌)‘2) = (0g‘𝐾))
79	78	oveq2d 7407	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
80	66, 67, 52, 18, 65	ringrzd 20333	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
81	69, 79, 80	3eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (0g‘𝐾))
82	42, 64	eleqtrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (Base‘𝐾))
83	19, 35, 66, 52	coe1scl 22338	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
84	18, 82, 83	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
85		0ne2 12421	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≠ 2
86	85	neii 2958	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 0 = 2
87		eqeq1 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑖 = 2 ↔ 0 = 2))
88	86, 87	mtbiri 329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ¬ 𝑖 = 2)
89	88, 55	nsyl3 138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
90	89	iffalsed 4488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
91	84, 90, 29, 77	fvmptd 6978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘2) = (0g‘𝐾))
92	81, 91	oveq12d 7409	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)) = ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)))
93	18	ringgrpd 20279	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Grp)
94	66, 52	grpidcl 18998	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Grp → (0g‘𝐾) ∈ (Base‘𝐾))
95	93, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐾) ∈ (Base‘𝐾))
96	66, 49, 52, 93, 95	grpridd 19003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
97	60, 92, 96	3eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (0g‘𝐾))
98	58, 97	oveq12d 7409	. . . . . . . . . . . 12 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)) = ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)))
99	66, 53	ringidcl 20302	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (1r‘𝐾) ∈ (Base‘𝐾))
100	18, 99	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾))
101	66, 49, 52, 93, 100	grpridd 19003	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐾))
102	36	crngringd 20283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
103		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝐸) = (1r‘𝐸)
104	103	subrg1cl 20617	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
105	38, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
106	6, 62	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝑉)
107	1, 61, 103	ress1r 33374	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Ring ∧ (1r‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → (1r‘𝐸) = (1r‘𝐾))
108	102, 105, 106, 107	syl3anc 1389	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
109	101, 108	eqtr4d 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐸))
110	51, 98, 109	3eqtrd 2800	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (1r‘𝐸))
111	48, 110	eqtrid 2808	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘𝐺)‘2) = (1r‘𝐸))
112	5	flddrngd 20778	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
113		drngnzr 20785	. . . . . . . . . . 11 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
114		rtelextdg2.3	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐸)
115	103, 114	nzrnz 20552	. . . . . . . . . . 11 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ 0 )
116	112, 113, 115	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐸) ≠ 0 )
117	111, 116	eqnetrd 3023	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘2) ≠ 0 )
118		fveq2 6862	. . . . . . . . . . 11 ⊢ (𝐺 = (0g‘𝑃) → (coe1‘𝐺) = (coe1‘(0g‘𝑃)))
119	118	fveq1d 6864	. . . . . . . . . 10 ⊢ (𝐺 = (0g‘𝑃) → ((coe1‘𝐺)‘2) = ((coe1‘(0g‘𝑃))‘2))
120		eqid 2761	. . . . . . . . . . . 12 ⊢ (0g‘𝑃) = (0g‘𝑃)
121	19, 120, 52, 18, 29	coe1zfv 33747	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = (0g‘𝐾))
122	102	ringgrpd 20279	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ Grp)
123	122	grpmndd 18979	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ Mnd)
124		subrgsubg 20614	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
125	38, 124	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
126	114	subg0cl 19167	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 0 ∈ 𝐹)
127	125, 126	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ 𝐹)
128	1, 61, 114	ress0g 18787	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Mnd ∧ 0 ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → 0 = (0g‘𝐾))
129	123, 127, 106, 128	syl3anc 1389	. . . . . . . . . . 11 ⊢ (𝜑 → 0 = (0g‘𝐾))
130	121, 129	eqtr4d 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = 0 )
131	119, 130	sylan9eqr 2818	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 = (0g‘𝑃)) → ((coe1‘𝐺)‘2) = 0 )
132	117, 131	mteqand 3047	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃))
133	11	fveq2i 6865	. . . . . . . . . . 11 ⊢ ((deg1‘𝐾)‘𝐺) = ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
134		eqid 2761	. . . . . . . . . . . . 13 ⊢ (deg1‘𝐾) = (deg1‘𝐾)
135		2re 12286	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
136	135	rexri 11234	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ*
137	136	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ*)
138	134, 19, 12	deg1xrcl 26130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
139	41, 138	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
140		1xr 11235	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ*
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ*)
142	134, 19, 66, 12, 34, 35	deg1mul3le 26165	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
143	18, 65, 32, 142	syl3anc 1389	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
144	1, 15	eqeltrid 2865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ Field)
145	144	flddrngd 20778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ DivRing)
146		drngnzr 20785	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ NzRing)
148	134, 19, 30, 147	deg1vr 33749	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘𝑌) = 1)
149	143, 148	breqtrd 5123	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ 1)
150		1lt2 12384	. . . . . . . . . . . . . . . . 17 ⊢ 1 < 2
151	150	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 < 2)
152	139, 141, 137, 149, 151	xrlelttrd 13156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) < 2)
153	134, 19, 12	deg1xrcl 26130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝐵) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
154	43, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
155		0xr 11223	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ*
156	155	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℝ*)
157	134, 19, 66, 35	deg1sclle 26160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
158	18, 82, 157	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
159		2pos 12316	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
160	159	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
161	154, 156, 137, 158, 160	xrlelttrd 13156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) < 2)
162	19, 134, 18, 12, 13, 41, 43, 137, 152, 161	deg1addlt 33757	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < 2)
163	134, 19, 30, 23, 25	deg1pw 26169	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ NzRing ∧ 2 ∈ ℕ0) → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
164	147, 29, 163	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
165	162, 164	breqtrrd 5125	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < ((deg1‘𝐾)‘(2 ∧ 𝑌)))
166	19, 134, 18, 12, 13, 33, 44, 165	deg1add 26151	. . . . . . . . . . . 12 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = ((deg1‘𝐾)‘(2 ∧ 𝑌)))
167	166, 164	eqtrd 2796	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = 2)
168	133, 167	eqtrid 2808	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐾)‘𝐺) = 2)
169	168	fveq2d 6866	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = ((coe1‘𝐺)‘2))
170	169, 111, 108	3eqtrd 2800	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾))
171		eqid 2761	. . . . . . . . 9 ⊢ (Monic1p‘𝐾) = (Monic1p‘𝐾)
172	19, 12, 120, 134, 171, 53	ismon1p 26191	. . . . . . . 8 ⊢ (𝐺 ∈ (Monic1p‘𝐾) ↔ (𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ (0g‘𝑃) ∧ ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾)))
173	46, 132, 170, 172	syl3anbrc 1356	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝐾))
174		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝐸 evalSub1 𝐹) = (𝐸 evalSub1 𝐹)
175		eqid 2761	. . . . . . . . . . . 12 ⊢ (eval1‘𝐸) = (eval1‘𝐸)
176	174, 61, 19, 1, 12, 175, 36, 38	ressply1evl 22421	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 evalSub1 𝐹) = ((eval1‘𝐸) ↾ (Base‘𝑃)))
177	176	fveq1d 6864	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺))
178	46	fvresd 6882	. . . . . . . . . 10 ⊢ (𝜑 → (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺) = ((eval1‘𝐸)‘𝐺))
179	177, 178	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = ((eval1‘𝐸)‘𝐺))
180	179	fveq1d 6864	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = (((eval1‘𝐸)‘𝐺)‘𝑋))
181		eqid 2761	. . . . . . . . 9 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
182		eqid 2761	. . . . . . . . 9 ⊢ (Base‘(Poly1‘𝐸)) = (Base‘(Poly1‘𝐸))
183		rtelextdg2.6	. . . . . . . . 9 ⊢ · = (.r‘𝐸)
184		rtelextdg2.7	. . . . . . . . 9 ⊢ + = (+g‘𝐸)
185		rtelextdg2.8	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐸))
186		eqid 2761	. . . . . . . . 9 ⊢ (coe1‘𝐺) = (coe1‘𝐺)
187		eqid 2761	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘𝐺)‘2)
188		eqid 2761	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘𝐺)‘1)
189		eqid 2761	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘𝐺)‘0)
190		eqid 2761	. . . . . . . . . . . 12 ⊢ (PwSer1‘𝐾) = (PwSer1‘𝐾)
191		eqid 2761	. . . . . . . . . . . 12 ⊢ (Base‘(PwSer1‘𝐾)) = (Base‘(PwSer1‘𝐾))
192	181, 1, 19, 12, 38, 190, 191, 182	ressply1bas2 22277	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑃) = ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
193	46, 192	eleqtrd 2863	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
194	193	elin2d 4155	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Base‘(Poly1‘𝐸)))
195	1, 3, 19, 12, 46, 38	ressdeg1 33723	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = ((deg1‘𝐾)‘𝐺))
196	195, 168	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = 2)
197	181, 175, 61, 182, 183, 184, 185, 186, 3, 187, 188, 189, 36, 194, 196, 7	evl1deg2 33734	. . . . . . . 8 ⊢ (𝜑 → (((eval1‘𝐸)‘𝐺)‘𝑋) = ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))))
198	111	oveq1d 7406	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = ((1r‘𝐸) · (2 ↑ 𝑋)))
199		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (mulGrp‘𝐸) = (mulGrp‘𝐸)
200	199, 61	mgpbas 20182	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Base‘(mulGrp‘𝐸))
201	199	ringmgp 20276	. . . . . . . . . . . . . 14 ⊢ (𝐸 ∈ Ring → (mulGrp‘𝐸) ∈ Mnd)
202	102, 201	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝐸) ∈ Mnd)
203	200, 185, 202, 29, 7	mulgnn0cld 19128	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝑉)
204	61, 183, 103, 102, 203	ringlidmd 20309	. . . . . . . . . . 11 ⊢ (𝜑 → ((1r‘𝐸) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
205	198, 204	eqtrd 2796	. . . . . . . . . 10 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
206	47	fveq1i 6863	. . . . . . . . . . . . 13 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1)
207		1nn0 12491	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ0
208	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ0)
209	19, 12, 13, 49	coe1addfv 22316	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)))
210	18, 33, 44, 208, 209	syl31anc 1391	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)))
211	71	neii 2958	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 1 = 2
212		eqeq1 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → (𝑖 = 2 ↔ 1 = 2))
213	212	notbid 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 1 → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
214	213	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
215	211, 214	mpbiri 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 2)
216	215	iffalsed 4488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
217	54, 216, 208, 77	fvmptd 6978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘1) = (0g‘𝐾))
218	19, 12, 13, 49	coe1addfv 22316	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)))
219	18, 41, 43, 208, 218	syl31anc 1391	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)))
220	19, 12, 66, 35, 34, 67	coe1sclmulfv 22334	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)))
221	18, 65, 32, 208, 220	syl121anc 1393	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)))
222		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 = 1)
223	222	iftrued 4485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
224	70, 223, 208, 57	fvmptd 6978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((coe1‘𝑌)‘1) = (1r‘𝐾))
225	224	oveq2d 7407	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)) = (𝐴(.r‘𝐾)(1r‘𝐾)))
226	66, 67, 53, 18, 65	ringridmd 20310	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)(1r‘𝐾)) = 𝐴)
227	221, 225, 226	3eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = 𝐴)
228		0ne1 12283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 1
229	228	nesymi 3013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
230		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0))
231	229, 230	mtbiri 329	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
232	231	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
233	232	iffalsed 4488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
234	84, 233, 208, 77	fvmptd 6978	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘1) = (0g‘𝐾))
235	227, 234	oveq12d 7409	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)) = (𝐴(+g‘𝐾)(0g‘𝐾)))
236	66, 49, 52, 93, 65	grpridd 19003	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(+g‘𝐾)(0g‘𝐾)) = 𝐴)
237	219, 235, 236	3eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = 𝐴)
238	217, 237	oveq12d 7409	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)) = ((0g‘𝐾)(+g‘𝐾)𝐴))
239	66, 49, 52, 93, 65	grplidd 19002	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐴) = 𝐴)
240	210, 238, 239	3eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = 𝐴)
241	206, 240	eqtrid 2808	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘𝐺)‘1) = 𝐴)
242	241	oveq1d 7406	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘1) · 𝑋) = (𝐴 · 𝑋))
243	47	fveq1i 6863	. . . . . . . . . . . 12 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0)
244		0nn0 12490	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℕ0
245	244	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℕ0)
246	19, 12, 13, 49	coe1addfv 22316	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)))
247	18, 33, 44, 245, 246	syl31anc 1391	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)))
248	88	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 2)
249	248	iffalsed 4488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
250	54, 249, 245, 77	fvmptd 6978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘0) = (0g‘𝐾))
251	19, 12, 13, 49	coe1addfv 22316	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)))
252	18, 41, 43, 245, 251	syl31anc 1391	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)))
253	19, 12, 66, 35, 34, 67	coe1sclmulfv 22334	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)))
254	18, 65, 32, 245, 253	syl121anc 1393	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)))
255	228	neii 2958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 0 = 1
256		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 = 1 ↔ 0 = 1))
257	255, 256	mtbiri 329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → ¬ 𝑖 = 1)
258	257	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 1)
259	258	iffalsed 4488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
260	70, 259, 245, 77	fvmptd 6978	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘𝑌)‘0) = (0g‘𝐾))
261	260	oveq2d 7407	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
262	254, 261, 80	3eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (0g‘𝐾))
263	19, 35, 66	ply1sclid 22339	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
264	18, 82, 263	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
265	264	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘0) = 𝐵)
266	262, 265	oveq12d 7409	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
267	66, 49, 52, 93, 82	grplidd 19002	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐵) = 𝐵)
268	252, 266, 267	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = 𝐵)
269	250, 268	oveq12d 7409	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
270	247, 269, 267	3eqtrd 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = 𝐵)
271	243, 270	eqtrid 2808	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘𝐺)‘0) = 𝐵)
272	242, 271	oveq12d 7409	. . . . . . . . . 10 ⊢ (𝜑 → ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0)) = ((𝐴 · 𝑋) + 𝐵))
273	205, 272	oveq12d 7409	. . . . . . . . 9 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)))
274		rtelextdg2.14	. . . . . . . . 9 ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )
275	273, 274	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = 0 )
276	180, 197, 275	3eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 )
277	10, 173, 276	rspcedvdw 3583	. . . . . 6 ⊢ (𝜑 → ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )
278	174, 1, 61, 114, 36, 38	elirng 33944	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )))
279	7, 277, 278	mpbir2and 723	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
280	1, 2, 3, 4, 5, 6, 279	algextdeg 33983	. . . 4 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)))
281	1	fveq2i 6865	. . . . . . 7 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
282	19, 281	eqtri 2784	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
283		eqid 2761	. . . . . 6 ⊢ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 } = {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 }
284		eqid 2761	. . . . . 6 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
285		eqid 2761	. . . . . 6 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
286	174, 282, 61, 5, 6, 7, 114, 283, 284, 285, 4	minplycl 33964	. . . . 5 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝑋) ∈ (Base‘𝑃))
287	1, 3, 19, 12, 286, 38	ressdeg1 33723	. . . 4 ⊢ (𝜑 → ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
288	280, 287	eqtrd 2796	. . 3 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
289	1	fveq2i 6865	. . . 4 ⊢ (deg1‘𝐾) = (deg1‘(𝐸 ↾s 𝐹))
290	174, 282, 61, 5, 6, 7, 114, 4, 289, 120, 12, 276, 46, 132	minplymindeg 33966	. . 3 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)) ≤ ((deg1‘𝐾)‘𝐺))
291	288, 290	eqbrtrd 5119	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ ((deg1‘𝐾)‘𝐺))
292	291, 168	breqtrd 5123	1 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ≠ wne 2956  ∃wrex 3085  {crab 3413  Vcvv 3453   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ifcif 4477  {csn 4579   class class class wbr 5097   ↦ cmpt 5178  dom cdm 5643   ↾ cres 5645  ‘cfv 6516  (class class class)co 7391  0cc0 11067  1c1 11068  ℝ^*cxr 11209   < clt 11210   ≤ cle 11211  2c2 12266  ℕ₀cn0 12475  Basecbs 17236   ↾_s cress 17257  +_gcplusg 17277  ._rcmulr 17278  0_gc0g 17459  Mndcmnd 18759  Grpcgrp 18966  ._gcmg 19100  SubGrpcsubg 19153  mulGrpcmgp 20177  1_rcur 20218  Ringcrg 20270  CRingccrg 20271  NzRingcnzr 20549  SubRingcsubrg 20606  DivRingcdr 20766  Fieldcfield 20767  SubDRingcsdrg 20823  RSpancrsp 21265  algSccascl 21892  PwSer₁cps1 22225  var₁cv1 22226  Poly₁cpl1 22227  coe₁cco1 22228   evalSub₁ ces1 22364  eval₁ce1 22365  deg₁cdg1 26102  Monic_1pcmn1 26174  idlGen_1pcig1p 26178   fldGen cfldgen 33458  [:]cextdg 33898   IntgRing cirng 33941   minPoly cminply 33957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-reg 9534  ax-inf2 9590  ax-ac2 10414  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144  ax-pre-sup 11145  ax-addf 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-tp 4584  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-of 7655  df-ofr 7656  df-rpss 7701  df-om 7842  df-1st 7965  df-2nd 7966  df-supp 8135  df-tpos 8200  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-1o 8431  df-2o 8432  df-oadd 8435  df-er 8672  df-ec 8674  df-qs 8678  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9302  df-sup 9382  df-inf 9383  df-oi 9452  df-r1 9716  df-rank 9717  df-dju 9853  df-card 9891  df-acn 9894  df-ac 10066  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-nn 12205  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12476  df-xnn0 12549  df-z 12563  df-dec 12683  df-uz 12834  df-ico 13349  df-fz 13507  df-fzo 13654  df-seq 14009  df-hash 14338  df-struct 17174  df-sets 17191  df-slot 17209  df-ndx 17221  df-base 17237  df-ress 17258  df-plusg 17290  df-mulr 17291  df-starv 17292  df-sca 17293  df-vsca 17294  df-ip 17295  df-tset 17296  df-ple 17297  df-ocomp 17298  df-ds 17299  df-unif 17300  df-hom 17301  df-cco 17302  df-0g 17461  df-gsum 17462  df-prds 17467  df-pws 17469  df-imas 17529  df-qus 17530  df-mre 17605  df-mrc 17606  df-mri 17607  df-acs 17608  df-proset 18317  df-drs 18318  df-poset 18336  df-ipo 18551  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18969  df-minusg 18970  df-sbg 18971  df-mulg 19101  df-subg 19156  df-nsg 19157  df-eqg 19158  df-ghm 19245  df-gim 19290  df-cntz 19348  df-oppg 19377  df-lsm 19667  df-cmn 19813  df-abl 19814  df-mgp 20178  df-rng 20190  df-ur 20219  df-srg 20224  df-ring 20272  df-cring 20273  df-oppr 20373  df-dvdsr 20393  df-unit 20394  df-irred 20395  df-invr 20424  df-dvr 20437  df-rhm 20508  df-nzr 20550  df-subrng 20583  df-subrg 20607  df-rlreg 20731  df-domn 20732  df-idom 20733  df-drng 20768  df-field 20769  df-sdrg 20824  df-lmod 20917  df-lss 20987  df-lsp 21027  df-lmhm 21077  df-lmim 21078  df-lmic 21079  df-lbs 21130  df-lvec 21158  df-sra 21228  df-rgmod 21229  df-lidl 21266  df-rsp 21267  df-2idl 21308  df-lpidl 21380  df-lpir 21381  df-pid 21395  df-cnfld 21413  df-dsmm 21772  df-frlm 21787  df-uvc 21823  df-lindf 21846  df-linds 21847  df-assa 21893  df-asp 21894  df-ascl 21895  df-psr 21949  df-mvr 21950  df-mpl 21951  df-opsr 21953  df-evls 22115  df-evl 22116  df-psr1 22230  df-vr1 22231  df-ply1 22232  df-coe1 22233  df-evls1 22366  df-evl1 22367  df-mdeg 26103  df-deg1 26104  df-mon1 26179  df-uc1p 26180  df-q1p 26181  df-r1p 26182  df-ig1p 26183  df-fldgen 33459  df-mxidl 33609  df-dim 33858  df-fldext 33899  df-extdg 33900  df-irng 33942  df-minply 33958

This theorem is referenced by:  rtelextdg2  33985