Theorem rtelextdg2lem 34236

Description: Lemma for rtelextdg2 34237: 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 2760	. . . . 5 ⊢ (deg1‘𝐸) = (deg1‘𝐸)
4		eqid 2760	. . . . 5 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
5		rtelextdg2.9	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Field)
6		rtelextdg2.10	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
7		rtelextdg2.11	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
8		fveq2 6878	. . . . . . . . 9 ⊢ (𝑝 = 𝐺 → ((𝐸 evalSub1 𝐹)‘𝑝) = ((𝐸 evalSub1 𝐹)‘𝐺))
9	8	fveq1d 6880	. . . . . . . 8 ⊢ (𝑝 = 𝐺 → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋))
10	9	eqeq1d 2762	. . . . . . 7 ⊢ (𝑝 = 𝐺 → ((((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 ↔ (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 ))
11		rtelextdg2lem.6	. . . . . . . . 9 ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))
12		eqid 2760	. . . . . . . . . 10 ⊢ (Base‘𝑃) = (Base‘𝑃)
13		rtelextdg2lem.2	. . . . . . . . . 10 ⊢ ⊕ = (+g‘𝑃)
14		fldsdrgfld 20964	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
15	5, 6, 14	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
16	15	fldcrngd 20905	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing)
17	1, 16	eqeltrid 2864	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ CRing)
18	17	crngringd 20385	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
19		rtelextdg2.4	. . . . . . . . . . . . 13 ⊢ 𝑃 = (Poly1‘𝐾)
20	19	ply1ring 22472	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
21	18, 20	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ Ring)
22	21	ringgrpd 20381	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
23		eqid 2760	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
24	23, 12	mgpbas 20278	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
25		rtelextdg2lem.4	. . . . . . . . . . 11 ⊢ ∧ = (.g‘(mulGrp‘𝑃))
26	23	ringmgp 20378	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
27	21, 26	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
28		2nn0 12545	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ0)
30		rtelextdg2lem.1	. . . . . . . . . . . . 13 ⊢ 𝑌 = (var1‘𝐾)
31	30, 19, 12	vr1cl 22442	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑌 ∈ (Base‘𝑃))
32	18, 31	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑃))
33	24, 25, 27, 29, 32	mulgnn0cld 19218	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∧ 𝑌) ∈ (Base‘𝑃))
34		rtelextdg2lem.3	. . . . . . . . . . . 12 ⊢ ⊗ = (.r‘𝑃)
35		rtelextdg2lem.5	. . . . . . . . . . . . 13 ⊢ 𝑈 = (algSc‘𝑃)
36	5	fldcrngd 20905	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37		sdrgsubrg 20957	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
38	6, 37	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
39		rtelextdg2.12	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝐹)
40	19, 1, 35, 12, 36, 38, 39	ressasclcl 33981	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘𝐴) ∈ (Base‘𝑃))
41	12, 34, 21, 40, 32	ringcld 20396	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃))
42		rtelextdg2.13	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐹)
43	19, 1, 35, 12, 36, 38, 42	ressasclcl 33981	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘𝐵) ∈ (Base‘𝑃))
44	12, 13, 22, 41, 43	grpcld 19071	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃))
45	12, 13, 22, 33, 44	grpcld 19071	. . . . . . . . 9 ⊢ (𝜑 → ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) ∈ (Base‘𝑃))
46	11, 45	eqeltrid 2864	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))
47	11	fveq2i 6881	. . . . . . . . . . . 12 ⊢ (coe1‘𝐺) = (coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
48	47	fveq1i 6879	. . . . . . . . . . 11 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2)
49		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐾) = (+g‘𝐾)
50	19, 12, 13, 49	coe1addfv 22491	. . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐾) = (0g‘𝐾)
53		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝐾) = (1r‘𝐾)
54	19, 30, 25, 18, 29, 52, 53	coe1mon 33997	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (coe1‘(2 ∧ 𝑌)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾))))
55		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2)
56	55	iftrued 4490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
57		fvexd 6893	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ V)
58	54, 56, 29, 57	fvmptd 6994	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘2) = (1r‘𝐾))
59	19, 12, 13, 49	coe1addfv 22491	. . . . . . . . . . . . . . 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 20959	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝑉)
63	1, 61	ressbas2 17330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ⊆ 𝑉 → 𝐹 = (Base‘𝐾))
64	6, 62, 63	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
65	39, 64	eleqtrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐾))
66		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐾) = (Base‘𝐾)
67		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐾) = (.r‘𝐾)
68	19, 12, 66, 35, 34, 67	coe1sclmulfv 22509	. . . . . . . . . . . . . . . . 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 34001	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (coe1‘𝑌) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾))))
71		1ne2 12475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 2
72	71	nesymi 3012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 2 = 1
73		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → (𝑖 = 1 ↔ 2 = 1))
74	72, 73	mtbiri 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 1)
75	74	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 1)
76	75	iffalsed 4493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
77		fvexd 6893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐾) ∈ V)
78	70, 76, 29, 77	fvmptd 6994	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘𝑌)‘2) = (0g‘𝐾))
79	78	oveq2d 7429	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
80	66, 67, 52, 18, 65	ringrzd 20438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
81	69, 79, 80	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (0g‘𝐾))
82	42, 64	eleqtrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (Base‘𝐾))
83	19, 35, 66, 52	coe1scl 22513	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
84	18, 82, 83	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
85		0ne2 12474	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≠ 2
86	85	neii 2957	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 0 = 2
87		eqeq1 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑖 = 2 ↔ 0 = 2))
88	86, 87	mtbiri 330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ¬ 𝑖 = 2)
89	88, 55	nsyl3 139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
90	89	iffalsed 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
91	84, 90, 29, 77	fvmptd 6994	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘2) = (0g‘𝐾))
92	81, 91	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)) = ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)))
93	18	ringgrpd 20381	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Grp)
94	66, 52	grpidcl 19089	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Grp → (0g‘𝐾) ∈ (Base‘𝐾))
95	93, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐾) ∈ (Base‘𝐾))
96	66, 49, 52, 93, 95	grpridd 19094	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
97	60, 92, 96	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (0g‘𝐾))
98	58, 97	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)) = ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)))
99	66, 53	ringidcl 20406	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (1r‘𝐾) ∈ (Base‘𝐾))
100	18, 99	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾))
101	66, 49, 52, 93, 100	grpridd 19094	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐾))
102	36	crngringd 20385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
103		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝐸) = (1r‘𝐸)
104	103	subrg1cl 20742	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
105	38, 104	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
106	6, 62	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝑉)
107	1, 61, 103	ress1r 33672	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Ring ∧ (1r‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → (1r‘𝐸) = (1r‘𝐾))
108	102, 105, 106, 107	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
109	101, 108	eqtr4d 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐸))
110	51, 98, 109	3eqtrd 2799	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (1r‘𝐸))
111	48, 110	eqtrid 2807	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘𝐺)‘2) = (1r‘𝐸))
112	5	flddrngd 20904	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
113		drngnzr 20911	. . . . . . . . . . 11 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
114		rtelextdg2.3	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐸)
115	103, 114	nzrnz 20675	. . . . . . . . . . 11 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ 0 )
116	112, 113, 115	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐸) ≠ 0 )
117	111, 116	eqnetrd 3022	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘2) ≠ 0 )
118		fveq2 6878	. . . . . . . . . . 11 ⊢ (𝐺 = (0g‘𝑃) → (coe1‘𝐺) = (coe1‘(0g‘𝑃)))
119	118	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝐺 = (0g‘𝑃) → ((coe1‘𝐺)‘2) = ((coe1‘(0g‘𝑃))‘2))
120		eqid 2760	. . . . . . . . . . . 12 ⊢ (0g‘𝑃) = (0g‘𝑃)
121	19, 120, 52, 18, 29	coe1zfv 34000	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = (0g‘𝐾))
122	102	ringgrpd 20381	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ Grp)
123	122	grpmndd 19070	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ Mnd)
124		subrgsubg 20739	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
125	38, 124	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
126	114	subg0cl 19257	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 0 ∈ 𝐹)
127	125, 126	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ 𝐹)
128	1, 61, 114	ress0g 18867	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Mnd ∧ 0 ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → 0 = (0g‘𝐾))
129	123, 127, 106, 128	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → 0 = (0g‘𝐾))
130	121, 129	eqtr4d 2798	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = 0 )
131	119, 130	sylan9eqr 2817	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 = (0g‘𝑃)) → ((coe1‘𝐺)‘2) = 0 )
132	117, 131	mteqand 3046	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃))
133	11	fveq2i 6881	. . . . . . . . . . 11 ⊢ ((deg1‘𝐾)‘𝐺) = ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
134		eqid 2760	. . . . . . . . . . . . 13 ⊢ (deg1‘𝐾) = (deg1‘𝐾)
135		2re 12339	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
136	135	rexri 11291	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ*
137	136	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ*)
138	134, 19, 12	deg1xrcl 26307	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
139	41, 138	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
140		1xr 11292	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ*
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ*)
142	134, 19, 66, 12, 34, 35	deg1mul3le 26342	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
143	18, 65, 32, 142	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
144	1, 15	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ Field)
145	144	flddrngd 20904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ DivRing)
146		drngnzr 20911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
147	145, 146	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ NzRing)
148	134, 19, 30, 147	deg1vr 34002	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘𝑌) = 1)
149	143, 148	breqtrd 5131	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ 1)
150		1lt2 12437	. . . . . . . . . . . . . . . . 17 ⊢ 1 < 2
151	150	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 < 2)
152	139, 141, 137, 149, 151	xrlelttrd 13211	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) < 2)
153	134, 19, 12	deg1xrcl 26307	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝐵) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
154	43, 153	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
155		0xr 11280	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ*
156	155	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℝ*)
157	134, 19, 66, 35	deg1sclle 26337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
158	18, 82, 157	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
159		2pos 12369	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
160	159	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
161	154, 156, 137, 158, 160	xrlelttrd 13211	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) < 2)
162	19, 134, 18, 12, 13, 41, 43, 137, 152, 161	deg1addlt 34010	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < 2)
163	134, 19, 30, 23, 25	deg1pw 26346	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ NzRing ∧ 2 ∈ ℕ0) → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
164	147, 29, 163	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
165	162, 164	breqtrrd 5133	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < ((deg1‘𝐾)‘(2 ∧ 𝑌)))
166	19, 134, 18, 12, 13, 33, 44, 165	deg1add 26328	. . . . . . . . . . . 12 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = ((deg1‘𝐾)‘(2 ∧ 𝑌)))
167	166, 164	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = 2)
168	133, 167	eqtrid 2807	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐾)‘𝐺) = 2)
169	168	fveq2d 6882	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = ((coe1‘𝐺)‘2))
170	169, 111, 108	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾))
171		eqid 2760	. . . . . . . . 9 ⊢ (Monic1p‘𝐾) = (Monic1p‘𝐾)
172	19, 12, 120, 134, 171, 53	ismon1p 26368	. . . . . . . 8 ⊢ (𝐺 ∈ (Monic1p‘𝐾) ↔ (𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ (0g‘𝑃) ∧ ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾)))
173	46, 132, 170, 172	syl3anbrc 1362	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝐾))
174		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝐸 evalSub1 𝐹) = (𝐸 evalSub1 𝐹)
175		eqid 2760	. . . . . . . . . . . 12 ⊢ (eval1‘𝐸) = (eval1‘𝐸)
176	174, 61, 19, 1, 12, 175, 36, 38	ressply1evl 22595	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 evalSub1 𝐹) = ((eval1‘𝐸) ↾ (Base‘𝑃)))
177	176	fveq1d 6880	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺))
178	46	fvresd 6898	. . . . . . . . . 10 ⊢ (𝜑 → (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺) = ((eval1‘𝐸)‘𝐺))
179	177, 178	eqtrd 2795	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = ((eval1‘𝐸)‘𝐺))
180	179	fveq1d 6880	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = (((eval1‘𝐸)‘𝐺)‘𝑋))
181		eqid 2760	. . . . . . . . 9 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
182		eqid 2760	. . . . . . . . 9 ⊢ (Base‘(Poly1‘𝐸)) = (Base‘(Poly1‘𝐸))
183		rtelextdg2.6	. . . . . . . . 9 ⊢ · = (.r‘𝐸)
184		rtelextdg2.7	. . . . . . . . 9 ⊢ + = (+g‘𝐸)
185		rtelextdg2.8	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐸))
186		eqid 2760	. . . . . . . . 9 ⊢ (coe1‘𝐺) = (coe1‘𝐺)
187		eqid 2760	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘𝐺)‘2)
188		eqid 2760	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘𝐺)‘1)
189		eqid 2760	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘𝐺)‘0)
190		eqid 2760	. . . . . . . . . . . 12 ⊢ (PwSer1‘𝐾) = (PwSer1‘𝐾)
191		eqid 2760	. . . . . . . . . . . 12 ⊢ (Base‘(PwSer1‘𝐾)) = (Base‘(PwSer1‘𝐾))
192	181, 1, 19, 12, 38, 190, 191, 182	ressply1bas2 22452	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑃) = ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
193	46, 192	eleqtrd 2862	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
194	193	elin2d 4151	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Base‘(Poly1‘𝐸)))
195	1, 3, 19, 12, 46, 38	ressdeg1 33976	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = ((deg1‘𝐾)‘𝐺))
196	195, 168	eqtrd 2795	. . . . . . . . 9 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = 2)
197	181, 175, 61, 182, 183, 184, 185, 186, 3, 187, 188, 189, 36, 194, 196, 7	evl1deg2 33987	. . . . . . . 8 ⊢ (𝜑 → (((eval1‘𝐸)‘𝐺)‘𝑋) = ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))))
198	111	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = ((1r‘𝐸) · (2 ↑ 𝑋)))
199		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (mulGrp‘𝐸) = (mulGrp‘𝐸)
200	199, 61	mgpbas 20278	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Base‘(mulGrp‘𝐸))
201	199	ringmgp 20378	. . . . . . . . . . . . . 14 ⊢ (𝐸 ∈ Ring → (mulGrp‘𝐸) ∈ Mnd)
202	102, 201	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝐸) ∈ Mnd)
203	200, 185, 202, 29, 7	mulgnn0cld 19218	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝑉)
204	61, 183, 103, 102, 203	ringlidmd 20413	. . . . . . . . . . 11 ⊢ (𝜑 → ((1r‘𝐸) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
205	198, 204	eqtrd 2795	. . . . . . . . . 10 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
206	47	fveq1i 6879	. . . . . . . . . . . . 13 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1)
207		1nn0 12544	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ0
208	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ0)
209	19, 12, 13, 49	coe1addfv 22491	. . . . . . . . . . . . . . 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 2957	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 1 = 2
212		eqeq1 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → (𝑖 = 2 ↔ 1 = 2))
213	212	notbid 321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 1 → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
214	213	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
215	211, 214	mpbiri 261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 2)
216	215	iffalsed 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
217	54, 216, 208, 77	fvmptd 6994	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘1) = (0g‘𝐾))
218	19, 12, 13, 49	coe1addfv 22491	. . . . . . . . . . . . . . . . 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 22509	. . . . . . . . . . . . . . . . . . 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 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 = 1)
223	222	iftrued 4490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
224	70, 223, 208, 57	fvmptd 6994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((coe1‘𝑌)‘1) = (1r‘𝐾))
225	224	oveq2d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)) = (𝐴(.r‘𝐾)(1r‘𝐾)))
226	66, 67, 53, 18, 65	ringridmd 20414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)(1r‘𝐾)) = 𝐴)
227	221, 225, 226	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = 𝐴)
228		0ne1 12336	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 1
229	228	nesymi 3012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
230		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0))
231	229, 230	mtbiri 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
232	231	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
233	232	iffalsed 4493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
234	84, 233, 208, 77	fvmptd 6994	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘1) = (0g‘𝐾))
235	227, 234	oveq12d 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)) = (𝐴(+g‘𝐾)(0g‘𝐾)))
236	66, 49, 52, 93, 65	grpridd 19094	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(+g‘𝐾)(0g‘𝐾)) = 𝐴)
237	219, 235, 236	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = 𝐴)
238	217, 237	oveq12d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)) = ((0g‘𝐾)(+g‘𝐾)𝐴))
239	66, 49, 52, 93, 65	grplidd 19093	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐴) = 𝐴)
240	210, 238, 239	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = 𝐴)
241	206, 240	eqtrid 2807	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘𝐺)‘1) = 𝐴)
242	241	oveq1d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘1) · 𝑋) = (𝐴 · 𝑋))
243	47	fveq1i 6879	. . . . . . . . . . . 12 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0)
244		0nn0 12543	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℕ0
245	244	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℕ0)
246	19, 12, 13, 49	coe1addfv 22491	. . . . . . . . . . . . . 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 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 2)
249	248	iffalsed 4493	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
250	54, 249, 245, 77	fvmptd 6994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘0) = (0g‘𝐾))
251	19, 12, 13, 49	coe1addfv 22491	. . . . . . . . . . . . . . . 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 22509	. . . . . . . . . . . . . . . . . 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 2957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 0 = 1
256		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 = 1 ↔ 0 = 1))
257	255, 256	mtbiri 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → ¬ 𝑖 = 1)
258	257	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 1)
259	258	iffalsed 4493	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
260	70, 259, 245, 77	fvmptd 6994	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘𝑌)‘0) = (0g‘𝐾))
261	260	oveq2d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
262	254, 261, 80	3eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (0g‘𝐾))
263	19, 35, 66	ply1sclid 22514	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
264	18, 82, 263	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
265	264	eqcomd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘0) = 𝐵)
266	262, 265	oveq12d 7431	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
267	66, 49, 52, 93, 82	grplidd 19093	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐵) = 𝐵)
268	252, 266, 267	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = 𝐵)
269	250, 268	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
270	247, 269, 267	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = 𝐵)
271	243, 270	eqtrid 2807	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘𝐺)‘0) = 𝐵)
272	242, 271	oveq12d 7431	. . . . . . . . . 10 ⊢ (𝜑 → ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0)) = ((𝐴 · 𝑋) + 𝐵))
273	205, 272	oveq12d 7431	. . . . . . . . 9 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)))
274		rtelextdg2.14	. . . . . . . . 9 ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )
275	273, 274	eqtrd 2795	. . . . . . . 8 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = 0 )
276	180, 197, 275	3eqtrd 2799	. . . . . . 7 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 )
277	10, 173, 276	rspcedvdw 3579	. . . . . 6 ⊢ (𝜑 → ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )
278	174, 1, 61, 114, 36, 38	elirng 34196	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )))
279	7, 277, 278	mpbir2and 726	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
280	1, 2, 3, 4, 5, 6, 279	algextdeg 34235	. . . 4 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)))
281	1	fveq2i 6881	. . . . . . 7 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
282	19, 281	eqtri 2783	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
283		eqid 2760	. . . . . 6 ⊢ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 } = {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 }
284		eqid 2760	. . . . . 6 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
285		eqid 2760	. . . . . 6 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
286	174, 282, 61, 5, 6, 7, 114, 283, 284, 285, 4	minplycl 34216	. . . . 5 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝑋) ∈ (Base‘𝑃))
287	1, 3, 19, 12, 286, 38	ressdeg1 33976	. . . 4 ⊢ (𝜑 → ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
288	280, 287	eqtrd 2795	. . 3 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
289	1	fveq2i 6881	. . . 4 ⊢ (deg1‘𝐾) = (deg1‘(𝐸 ↾s 𝐹))
290	174, 282, 61, 5, 6, 7, 114, 4, 289, 120, 12, 276, 46, 132	minplymindeg 34218	. . 3 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)) ≤ ((deg1‘𝐾)‘𝐺))
291	288, 290	eqbrtrd 5127	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ ((deg1‘𝐾)‘𝐺))
292	291, 168	breqtrd 5131	1 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∃wrex 3086  {crab 3412  Vcvv 3450   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ifcif 4482  {csn 4584   class class class wbr 5103   ↦ cmpt 5186  dom cdm 5655   ↾ cres 5657  ‘cfv 6533  (class class class)co 7413  0cc0 11124  1c1 11125  ℝ^*cxr 11266   < clt 11267   ≤ cle 11268  2c2 12319  ℕ₀cn0 12528  Basecbs 17301   ↾_s cress 17322  +_gcplusg 17342  ._rcmulr 17343  0_gc0g 17524  Mndcmnd 18836  Grpcgrp 19057  ._gcmg 19190  SubGrpcsubg 19243  mulGrpcmgp 20273  1_rcur 20320  Ringcrg 20372  CRingccrg 20373  NzRingcnzr 20672  SubRingcsubrg 20731  DivRingcdr 20890  Fieldcfield 20891  SubDRingcsdrg 20952  RSpancrsp 21394  algSccascl 22067  PwSer₁cps1 22400  var₁cv1 22401  Poly₁cpl1 22402  coe₁cco1 22403   evalSub₁ ces1 22538  eval₁ce1 22539  deg₁cdg1 26279  Monic_1pcmn1 26351  idlGen_1pcig1p 26355   fldGen cfldgen 33751  [:]cextdg 34150   IntgRing cirng 34193   minPoly cminply 34209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-reg 9564  ax-inf2 9620  ax-ac2 10465  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202  ax-addf 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7678  df-ofr 7679  df-rpss 7724  df-om 7863  df-1st 7986  df-2nd 7987  df-supp 8159  df-tpos 8224  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-er 8696  df-ec 8698  df-qs 8702  df-map 8828  df-pm 8829  df-ixp 8905  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-fsupp 9332  df-sup 9412  df-inf 9413  df-oi 9482  df-r1 9746  df-rank 9747  df-scott 9868  df-dju 9906  df-card 9944  df-acn 9947  df-ac 10119  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-xnn0 12602  df-z 12616  df-dec 12737  df-uz 12888  df-ico 13404  df-fz 13562  df-fzo 13710  df-seq 14066  df-hash 14395  df-struct 17239  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-ress 17323  df-plusg 17355  df-mulr 17356  df-starv 17357  df-sca 17358  df-vsca 17359  df-ip 17360  df-tset 17361  df-ple 17362  df-ocomp 17363  df-ds 17364  df-unif 17365  df-hom 17366  df-cco 17367  df-0g 17526  df-gsum 17527  df-prds 17532  df-pws 17534  df-imas 17594  df-qus 17595  df-mre 17670  df-mrc 17671  df-mri 17672  df-acs 17673  df-proset 18382  df-drs 18383  df-poset 18401  df-ipo 18616  df-mgm 18730  df-sgrp 18821  df-mnd 18837  df-mhm 18891  df-submnd 18892  df-grp 19060  df-minusg 19061  df-sbg 19062  df-mulg 19191  df-subg 19246  df-nsg 19247  df-eqg 19248  df-ghm 19341  df-gim 19386  df-cntz 19444  df-oppg 19473  df-lsm 19763  df-cmn 19909  df-abl 19910  df-mgp 20274  df-rng 20288  df-ur 20321  df-srg 20326  df-ring 20374  df-cring 20375  df-oppr 20478  df-dvdsr 20498  df-unit 20499  df-irred 20500  df-invr 20529  df-dvr 20542  df-rhm 20613  df-nzr 20673  df-subrng 20708  df-subrg 20732  df-rlreg 20856  df-domn 20857  df-idom 20858  df-drng 20892  df-field 20893  df-sdrg 20953  df-lmod 21046  df-lss 21116  df-lsp 21156  df-lmhm 21206  df-lmim 21207  df-lmic 21208  df-lbs 21259  df-lvec 21287  df-sra 21357  df-rgmod 21358  df-lidl 21395  df-rsp 21396  df-2idl 21452  df-lpidl 21553  df-lpir 21554  df-pid 21568  df-cnfld 21586  df-dsmm 21945  df-frlm 21960  df-uvc 21996  df-lindf 22019  df-linds 22020  df-assa 22068  df-asp 22069  df-ascl 22070  df-psr 22124  df-mvr 22125  df-mpl 22126  df-opsr 22128  df-evls 22290  df-evl 22291  df-psr1 22405  df-vr1 22406  df-ply1 22407  df-coe1 22408  df-evls1 22540  df-evl1 22541  df-mdeg 26280  df-deg1 26281  df-mon1 26356  df-uc1p 26357  df-q1p 26358  df-r1p 26359  df-ig1p 26360  df-fldgen 33752  df-mxidl 33863  df-dim 34110  df-fldext 34151  df-extdg 34152  df-irng 34194  df-minply 34210

This theorem is used by:  rtelextdg2  34237