Theorem rtelextdg2lem 34116

Description: Lemma for rtelextdg2 34117: 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 2763	. . . . 5 ⊢ (deg1‘𝐸) = (deg1‘𝐸)
4		eqid 2763	. . . . 5 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
5		rtelextdg2.9	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Field)
6		rtelextdg2.10	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
7		rtelextdg2.11	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
8		fveq2 6881	. . . . . . . . 9 ⊢ (𝑝 = 𝐺 → ((𝐸 evalSub1 𝐹)‘𝑝) = ((𝐸 evalSub1 𝐹)‘𝐺))
9	8	fveq1d 6883	. . . . . . . 8 ⊢ (𝑝 = 𝐺 → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋))
10	9	eqeq1d 2765	. . . . . . 7 ⊢ (𝑝 = 𝐺 → ((((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 ↔ (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 ))
11		rtelextdg2lem.6	. . . . . . . . 9 ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))
12		eqid 2763	. . . . . . . . . 10 ⊢ (Base‘𝑃) = (Base‘𝑃)
13		rtelextdg2lem.2	. . . . . . . . . 10 ⊢ ⊕ = (+g‘𝑃)
14		fldsdrgfld 20901	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
15	5, 6, 14	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
16	15	fldcrngd 20842	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing)
17	1, 16	eqeltrid 2867	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ CRing)
18	17	crngringd 20323	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
19		rtelextdg2.4	. . . . . . . . . . . . 13 ⊢ 𝑃 = (Poly1‘𝐾)
20	19	ply1ring 22407	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
21	18, 20	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ Ring)
22	21	ringgrpd 20319	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
23		eqid 2763	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
24	23, 12	mgpbas 20216	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
25		rtelextdg2lem.4	. . . . . . . . . . 11 ⊢ ∧ = (.g‘(mulGrp‘𝑃))
26	23	ringmgp 20316	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
27	21, 26	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
28		2nn0 12516	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ0)
30		rtelextdg2lem.1	. . . . . . . . . . . . 13 ⊢ 𝑌 = (var1‘𝐾)
31	30, 19, 12	vr1cl 22377	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑌 ∈ (Base‘𝑃))
32	18, 31	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑃))
33	24, 25, 27, 29, 32	mulgnn0cld 19156	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∧ 𝑌) ∈ (Base‘𝑃))
34		rtelextdg2lem.3	. . . . . . . . . . . 12 ⊢ ⊗ = (.r‘𝑃)
35		rtelextdg2lem.5	. . . . . . . . . . . . 13 ⊢ 𝑈 = (algSc‘𝑃)
36	5	fldcrngd 20842	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37		sdrgsubrg 20894	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
38	6, 37	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
39		rtelextdg2.12	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝐹)
40	19, 1, 35, 12, 36, 38, 39	ressasclcl 33861	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘𝐴) ∈ (Base‘𝑃))
41	12, 34, 21, 40, 32	ringcld 20334	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃))
42		rtelextdg2.13	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐹)
43	19, 1, 35, 12, 36, 38, 42	ressasclcl 33861	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘𝐵) ∈ (Base‘𝑃))
44	12, 13, 22, 41, 43	grpcld 19009	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃))
45	12, 13, 22, 33, 44	grpcld 19009	. . . . . . . . 9 ⊢ (𝜑 → ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) ∈ (Base‘𝑃))
46	11, 45	eqeltrid 2867	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))
47	11	fveq2i 6884	. . . . . . . . . . . 12 ⊢ (coe1‘𝐺) = (coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
48	47	fveq1i 6882	. . . . . . . . . . 11 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2)
49		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐾) = (+g‘𝐾)
50	19, 12, 13, 49	coe1addfv 22426	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)))
51	18, 33, 44, 29, 50	syl31anc 1400	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)))
52		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐾) = (0g‘𝐾)
53		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝐾) = (1r‘𝐾)
54	19, 30, 25, 18, 29, 52, 53	coe1mon 33877	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (coe1‘(2 ∧ 𝑌)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾))))
55		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2)
56	55	iftrued 4495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
57		fvexd 6896	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ V)
58	54, 56, 29, 57	fvmptd 6997	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘2) = (1r‘𝐾))
59	19, 12, 13, 49	coe1addfv 22426	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)))
60	18, 41, 43, 29, 59	syl31anc 1400	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)))
61		rtelextdg2.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑉 = (Base‘𝐸)
62	61	sdrgss 20896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝑉)
63	1, 61	ressbas2 17293	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ⊆ 𝑉 → 𝐹 = (Base‘𝐾))
64	6, 62, 63	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
65	39, 64	eleqtrd 2865	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐾))
66		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐾) = (Base‘𝐾)
67		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐾) = (.r‘𝐾)
68	19, 12, 66, 35, 34, 67	coe1sclmulfv 22444	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)))
69	18, 65, 32, 29, 68	syl121anc 1402	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)))
70	19, 30, 18, 52, 53	coe1vr1 33881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (coe1‘𝑌) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾))))
71		1ne2 12446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 2
72	71	nesymi 3015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 2 = 1
73		eqeq1 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → (𝑖 = 1 ↔ 2 = 1))
74	72, 73	mtbiri 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 1)
75	74	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 1)
76	75	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
77		fvexd 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐾) ∈ V)
78	70, 76, 29, 77	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘𝑌)‘2) = (0g‘𝐾))
79	78	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
80	66, 67, 52, 18, 65	ringrzd 20375	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
81	69, 79, 80	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (0g‘𝐾))
82	42, 64	eleqtrd 2865	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (Base‘𝐾))
83	19, 35, 66, 52	coe1scl 22448	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
84	18, 82, 83	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
85		0ne2 12445	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≠ 2
86	85	neii 2960	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 0 = 2
87		eqeq1 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑖 = 2 ↔ 0 = 2))
88	86, 87	mtbiri 330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ¬ 𝑖 = 2)
89	88, 55	nsyl3 139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
90	89	iffalsed 4498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
91	84, 90, 29, 77	fvmptd 6997	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘2) = (0g‘𝐾))
92	81, 91	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)) = ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)))
93	18	ringgrpd 20319	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Grp)
94	66, 52	grpidcl 19027	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Grp → (0g‘𝐾) ∈ (Base‘𝐾))
95	93, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐾) ∈ (Base‘𝐾))
96	66, 49, 52, 93, 95	grpridd 19032	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
97	60, 92, 96	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (0g‘𝐾))
98	58, 97	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)) = ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)))
99	66, 53	ringidcl 20344	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (1r‘𝐾) ∈ (Base‘𝐾))
100	18, 99	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾))
101	66, 49, 52, 93, 100	grpridd 19032	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐾))
102	36	crngringd 20323	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
103		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝐸) = (1r‘𝐸)
104	103	subrg1cl 20679	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
105	38, 104	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
106	6, 62	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝑉)
107	1, 61, 103	ress1r 33552	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Ring ∧ (1r‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → (1r‘𝐸) = (1r‘𝐾))
108	102, 105, 106, 107	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
109	101, 108	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐸))
110	51, 98, 109	3eqtrd 2802	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (1r‘𝐸))
111	48, 110	eqtrid 2810	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘𝐺)‘2) = (1r‘𝐸))
112	5	flddrngd 20841	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
113		drngnzr 20848	. . . . . . . . . . 11 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
114		rtelextdg2.3	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐸)
115	103, 114	nzrnz 20612	. . . . . . . . . . 11 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ 0 )
116	112, 113, 115	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐸) ≠ 0 )
117	111, 116	eqnetrd 3025	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘2) ≠ 0 )
118		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝐺 = (0g‘𝑃) → (coe1‘𝐺) = (coe1‘(0g‘𝑃)))
119	118	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝐺 = (0g‘𝑃) → ((coe1‘𝐺)‘2) = ((coe1‘(0g‘𝑃))‘2))
120		eqid 2763	. . . . . . . . . . . 12 ⊢ (0g‘𝑃) = (0g‘𝑃)
121	19, 120, 52, 18, 29	coe1zfv 33880	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = (0g‘𝐾))
122	102	ringgrpd 20319	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ Grp)
123	122	grpmndd 19008	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ Mnd)
124		subrgsubg 20676	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
125	38, 124	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
126	114	subg0cl 19195	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 0 ∈ 𝐹)
127	125, 126	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ 𝐹)
128	1, 61, 114	ress0g 18815	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Mnd ∧ 0 ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → 0 = (0g‘𝐾))
129	123, 127, 106, 128	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → 0 = (0g‘𝐾))
130	121, 129	eqtr4d 2801	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = 0 )
131	119, 130	sylan9eqr 2820	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 = (0g‘𝑃)) → ((coe1‘𝐺)‘2) = 0 )
132	117, 131	mteqand 3049	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃))
133	11	fveq2i 6884	. . . . . . . . . . 11 ⊢ ((deg1‘𝐾)‘𝐺) = ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
134		eqid 2763	. . . . . . . . . . . . 13 ⊢ (deg1‘𝐾) = (deg1‘𝐾)
135		2re 12310	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
136	135	rexri 11262	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ*
137	136	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ*)
138	134, 19, 12	deg1xrcl 26239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
139	41, 138	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
140		1xr 11263	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ*
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ*)
142	134, 19, 66, 12, 34, 35	deg1mul3le 26274	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
143	18, 65, 32, 142	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
144	1, 15	eqeltrid 2867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ Field)
145	144	flddrngd 20841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ DivRing)
146		drngnzr 20848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
147	145, 146	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ NzRing)
148	134, 19, 30, 147	deg1vr 33882	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘𝑌) = 1)
149	143, 148	breqtrd 5137	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ 1)
150		1lt2 12408	. . . . . . . . . . . . . . . . 17 ⊢ 1 < 2
151	150	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 < 2)
152	139, 141, 137, 149, 151	xrlelttrd 13180	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) < 2)
153	134, 19, 12	deg1xrcl 26239	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝐵) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
154	43, 153	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
155		0xr 11251	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ*
156	155	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℝ*)
157	134, 19, 66, 35	deg1sclle 26269	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
158	18, 82, 157	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
159		2pos 12340	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
160	159	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
161	154, 156, 137, 158, 160	xrlelttrd 13180	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) < 2)
162	19, 134, 18, 12, 13, 41, 43, 137, 152, 161	deg1addlt 33890	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < 2)
163	134, 19, 30, 23, 25	deg1pw 26278	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ NzRing ∧ 2 ∈ ℕ0) → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
164	147, 29, 163	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
165	162, 164	breqtrrd 5139	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < ((deg1‘𝐾)‘(2 ∧ 𝑌)))
166	19, 134, 18, 12, 13, 33, 44, 165	deg1add 26260	. . . . . . . . . . . 12 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = ((deg1‘𝐾)‘(2 ∧ 𝑌)))
167	166, 164	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = 2)
168	133, 167	eqtrid 2810	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐾)‘𝐺) = 2)
169	168	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = ((coe1‘𝐺)‘2))
170	169, 111, 108	3eqtrd 2802	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾))
171		eqid 2763	. . . . . . . . 9 ⊢ (Monic1p‘𝐾) = (Monic1p‘𝐾)
172	19, 12, 120, 134, 171, 53	ismon1p 26300	. . . . . . . 8 ⊢ (𝐺 ∈ (Monic1p‘𝐾) ↔ (𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ (0g‘𝑃) ∧ ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾)))
173	46, 132, 170, 172	syl3anbrc 1362	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝐾))
174		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝐸 evalSub1 𝐹) = (𝐸 evalSub1 𝐹)
175		eqid 2763	. . . . . . . . . . . 12 ⊢ (eval1‘𝐸) = (eval1‘𝐸)
176	174, 61, 19, 1, 12, 175, 36, 38	ressply1evl 22530	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 evalSub1 𝐹) = ((eval1‘𝐸) ↾ (Base‘𝑃)))
177	176	fveq1d 6883	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺))
178	46	fvresd 6901	. . . . . . . . . 10 ⊢ (𝜑 → (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺) = ((eval1‘𝐸)‘𝐺))
179	177, 178	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = ((eval1‘𝐸)‘𝐺))
180	179	fveq1d 6883	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = (((eval1‘𝐸)‘𝐺)‘𝑋))
181		eqid 2763	. . . . . . . . 9 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
182		eqid 2763	. . . . . . . . 9 ⊢ (Base‘(Poly1‘𝐸)) = (Base‘(Poly1‘𝐸))
183		rtelextdg2.6	. . . . . . . . 9 ⊢ · = (.r‘𝐸)
184		rtelextdg2.7	. . . . . . . . 9 ⊢ + = (+g‘𝐸)
185		rtelextdg2.8	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐸))
186		eqid 2763	. . . . . . . . 9 ⊢ (coe1‘𝐺) = (coe1‘𝐺)
187		eqid 2763	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘𝐺)‘2)
188		eqid 2763	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘𝐺)‘1)
189		eqid 2763	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘𝐺)‘0)
190		eqid 2763	. . . . . . . . . . . 12 ⊢ (PwSer1‘𝐾) = (PwSer1‘𝐾)
191		eqid 2763	. . . . . . . . . . . 12 ⊢ (Base‘(PwSer1‘𝐾)) = (Base‘(PwSer1‘𝐾))
192	181, 1, 19, 12, 38, 190, 191, 182	ressply1bas2 22387	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑃) = ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
193	46, 192	eleqtrd 2865	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
194	193	elin2d 4158	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Base‘(Poly1‘𝐸)))
195	1, 3, 19, 12, 46, 38	ressdeg1 33856	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = ((deg1‘𝐾)‘𝐺))
196	195, 168	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = 2)
197	181, 175, 61, 182, 183, 184, 185, 186, 3, 187, 188, 189, 36, 194, 196, 7	evl1deg2 33867	. . . . . . . 8 ⊢ (𝜑 → (((eval1‘𝐸)‘𝐺)‘𝑋) = ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))))
198	111	oveq1d 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = ((1r‘𝐸) · (2 ↑ 𝑋)))
199		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (mulGrp‘𝐸) = (mulGrp‘𝐸)
200	199, 61	mgpbas 20216	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Base‘(mulGrp‘𝐸))
201	199	ringmgp 20316	. . . . . . . . . . . . . 14 ⊢ (𝐸 ∈ Ring → (mulGrp‘𝐸) ∈ Mnd)
202	102, 201	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝐸) ∈ Mnd)
203	200, 185, 202, 29, 7	mulgnn0cld 19156	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝑉)
204	61, 183, 103, 102, 203	ringlidmd 20351	. . . . . . . . . . 11 ⊢ (𝜑 → ((1r‘𝐸) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
205	198, 204	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
206	47	fveq1i 6882	. . . . . . . . . . . . 13 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1)
207		1nn0 12515	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ0
208	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ0)
209	19, 12, 13, 49	coe1addfv 22426	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)))
210	18, 33, 44, 208, 209	syl31anc 1400	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)))
211	71	neii 2960	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 1 = 2
212		eqeq1 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → (𝑖 = 2 ↔ 1 = 2))
213	212	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 1 → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
214	213	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
215	211, 214	mpbiri 261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 2)
216	215	iffalsed 4498	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
217	54, 216, 208, 77	fvmptd 6997	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘1) = (0g‘𝐾))
218	19, 12, 13, 49	coe1addfv 22426	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)))
219	18, 41, 43, 208, 218	syl31anc 1400	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)))
220	19, 12, 66, 35, 34, 67	coe1sclmulfv 22444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)))
221	18, 65, 32, 208, 220	syl121anc 1402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)))
222		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 = 1)
223	222	iftrued 4495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
224	70, 223, 208, 57	fvmptd 6997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((coe1‘𝑌)‘1) = (1r‘𝐾))
225	224	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)) = (𝐴(.r‘𝐾)(1r‘𝐾)))
226	66, 67, 53, 18, 65	ringridmd 20352	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)(1r‘𝐾)) = 𝐴)
227	221, 225, 226	3eqtrd 2802	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = 𝐴)
228		0ne1 12307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 1
229	228	nesymi 3015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
230		eqeq1 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0))
231	229, 230	mtbiri 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
232	231	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
233	232	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
234	84, 233, 208, 77	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘1) = (0g‘𝐾))
235	227, 234	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)) = (𝐴(+g‘𝐾)(0g‘𝐾)))
236	66, 49, 52, 93, 65	grpridd 19032	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(+g‘𝐾)(0g‘𝐾)) = 𝐴)
237	219, 235, 236	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = 𝐴)
238	217, 237	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)) = ((0g‘𝐾)(+g‘𝐾)𝐴))
239	66, 49, 52, 93, 65	grplidd 19031	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐴) = 𝐴)
240	210, 238, 239	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = 𝐴)
241	206, 240	eqtrid 2810	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘𝐺)‘1) = 𝐴)
242	241	oveq1d 7425	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘1) · 𝑋) = (𝐴 · 𝑋))
243	47	fveq1i 6882	. . . . . . . . . . . 12 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0)
244		0nn0 12514	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℕ0
245	244	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℕ0)
246	19, 12, 13, 49	coe1addfv 22426	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)))
247	18, 33, 44, 245, 246	syl31anc 1400	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)))
248	88	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 2)
249	248	iffalsed 4498	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
250	54, 249, 245, 77	fvmptd 6997	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘0) = (0g‘𝐾))
251	19, 12, 13, 49	coe1addfv 22426	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)))
252	18, 41, 43, 245, 251	syl31anc 1400	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)))
253	19, 12, 66, 35, 34, 67	coe1sclmulfv 22444	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)))
254	18, 65, 32, 245, 253	syl121anc 1402	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)))
255	228	neii 2960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 0 = 1
256		eqeq1 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 = 1 ↔ 0 = 1))
257	255, 256	mtbiri 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → ¬ 𝑖 = 1)
258	257	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 1)
259	258	iffalsed 4498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
260	70, 259, 245, 77	fvmptd 6997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘𝑌)‘0) = (0g‘𝐾))
261	260	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
262	254, 261, 80	3eqtrd 2802	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (0g‘𝐾))
263	19, 35, 66	ply1sclid 22449	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
264	18, 82, 263	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
265	264	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘0) = 𝐵)
266	262, 265	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
267	66, 49, 52, 93, 82	grplidd 19031	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐵) = 𝐵)
268	252, 266, 267	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = 𝐵)
269	250, 268	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
270	247, 269, 267	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = 𝐵)
271	243, 270	eqtrid 2810	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘𝐺)‘0) = 𝐵)
272	242, 271	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝜑 → ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0)) = ((𝐴 · 𝑋) + 𝐵))
273	205, 272	oveq12d 7428	. . . . . . . . 9 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)))
274		rtelextdg2.14	. . . . . . . . 9 ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )
275	273, 274	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = 0 )
276	180, 197, 275	3eqtrd 2802	. . . . . . 7 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 )
277	10, 173, 276	rspcedvdw 3584	. . . . . 6 ⊢ (𝜑 → ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )
278	174, 1, 61, 114, 36, 38	elirng 34076	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )))
279	7, 277, 278	mpbir2and 725	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
280	1, 2, 3, 4, 5, 6, 279	algextdeg 34115	. . . 4 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)))
281	1	fveq2i 6884	. . . . . . 7 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
282	19, 281	eqtri 2786	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
283		eqid 2763	. . . . . 6 ⊢ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 } = {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 }
284		eqid 2763	. . . . . 6 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
285		eqid 2763	. . . . . 6 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
286	174, 282, 61, 5, 6, 7, 114, 283, 284, 285, 4	minplycl 34096	. . . . 5 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝑋) ∈ (Base‘𝑃))
287	1, 3, 19, 12, 286, 38	ressdeg1 33856	. . . 4 ⊢ (𝜑 → ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
288	280, 287	eqtrd 2798	. . 3 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
289	1	fveq2i 6884	. . . 4 ⊢ (deg1‘𝐾) = (deg1‘(𝐸 ↾s 𝐹))
290	174, 282, 61, 5, 6, 7, 114, 4, 289, 120, 12, 276, 46, 132	minplymindeg 34098	. . 3 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)) ≤ ((deg1‘𝐾)‘𝐺))
291	288, 290	eqbrtrd 5133	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ ((deg1‘𝐾)‘𝐺))
292	291, 168	breqtrd 5137	1 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∃wrex 3089  {crab 3416  Vcvv 3455   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ifcif 4487  {csn 4589   class class class wbr 5109   ↦ cmpt 5192  dom cdm 5661   ↾ cres 5663  ‘cfv 6536  (class class class)co 7410  0cc0 11095  1c1 11096  ℝ^*cxr 11237   < clt 11238   ≤ cle 11239  2c2 12290  ℕ₀cn0 12499  Basecbs 17264   ↾_s cress 17285  +_gcplusg 17305  ._rcmulr 17306  0_gc0g 17487  Mndcmnd 18787  Grpcgrp 18995  ._gcmg 19128  SubGrpcsubg 19181  mulGrpcmgp 20211  1_rcur 20258  Ringcrg 20310  CRingccrg 20311  NzRingcnzr 20609  SubRingcsubrg 20668  DivRingcdr 20827  Fieldcfield 20828  SubDRingcsdrg 20889  RSpancrsp 21331  algSccascl 22002  PwSer₁cps1 22335  var₁cv1 22336  Poly₁cpl1 22337  coe₁cco1 22338   evalSub₁ ces1 22473  eval₁ce1 22474  deg₁cdg1 26211  Monic_1pcmn1 26283  idlGen_1pcig1p 26287   fldGen cfldgen 33631  [:]cextdg 34030   IntgRing cirng 34073   minPoly cminply 34089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-reg 9550  ax-inf2 9606  ax-ac2 10442  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173  ax-addf 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-ofr 7675  df-rpss 7720  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-tpos 8218  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-oadd 8453  df-er 8690  df-ec 8692  df-qs 8696  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-sup 9398  df-inf 9399  df-oi 9468  df-r1 9732  df-rank 9733  df-dju 9883  df-card 9921  df-acn 9924  df-ac 10096  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305  df-n0 12500  df-xnn0 12573  df-z 12587  df-dec 12707  df-uz 12858  df-ico 13373  df-fz 13531  df-fzo 13679  df-seq 14034  df-hash 14363  df-struct 17202  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-starv 17320  df-sca 17321  df-vsca 17322  df-ip 17323  df-tset 17324  df-ple 17325  df-ocomp 17326  df-ds 17327  df-unif 17328  df-hom 17329  df-cco 17330  df-0g 17489  df-gsum 17490  df-prds 17495  df-pws 17497  df-imas 17557  df-qus 17558  df-mre 17633  df-mrc 17634  df-mri 17635  df-acs 17636  df-proset 18345  df-drs 18346  df-poset 18364  df-ipo 18579  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-mhm 18836  df-submnd 18837  df-grp 18998  df-minusg 18999  df-sbg 19000  df-mulg 19129  df-subg 19184  df-nsg 19185  df-eqg 19186  df-ghm 19279  df-gim 19324  df-cntz 19382  df-oppg 19411  df-lsm 19701  df-cmn 19847  df-abl 19848  df-mgp 20212  df-rng 20226  df-ur 20259  df-srg 20264  df-ring 20312  df-cring 20313  df-oppr 20415  df-dvdsr 20435  df-unit 20436  df-irred 20437  df-invr 20466  df-dvr 20479  df-rhm 20550  df-nzr 20610  df-subrng 20645  df-subrg 20669  df-rlreg 20793  df-domn 20794  df-idom 20795  df-drng 20829  df-field 20830  df-sdrg 20890  df-lmod 20983  df-lss 21053  df-lsp 21093  df-lmhm 21143  df-lmim 21144  df-lmic 21145  df-lbs 21196  df-lvec 21224  df-sra 21294  df-rgmod 21295  df-lidl 21332  df-rsp 21333  df-2idl 21389  df-lpidl 21490  df-lpir 21491  df-pid 21505  df-cnfld 21523  df-dsmm 21882  df-frlm 21897  df-uvc 21933  df-lindf 21956  df-linds 21957  df-assa 22003  df-asp 22004  df-ascl 22005  df-psr 22059  df-mvr 22060  df-mpl 22061  df-opsr 22063  df-evls 22225  df-evl 22226  df-psr1 22340  df-vr1 22341  df-ply1 22342  df-coe1 22343  df-evls1 22475  df-evl1 22476  df-mdeg 26212  df-deg1 26213  df-mon1 26288  df-uc1p 26289  df-q1p 26290  df-r1p 26291  df-ig1p 26292  df-fldgen 33632  df-mxidl 33743  df-dim 33990  df-fldext 34031  df-extdg 34032  df-irng 34074  df-minply 34090

This theorem is referenced by:  rtelextdg2  34117