Theorem rtelextdg2lem 34156

Description: Lemma for rtelextdg2 34157: 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 2765	. . . . 5 ⊢ (deg1‘𝐸) = (deg1‘𝐸)
4		eqid 2765	. . . . 5 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
5		rtelextdg2.9	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Field)
6		rtelextdg2.10	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
7		rtelextdg2.11	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
8		fveq2 6885	. . . . . . . . 9 ⊢ (𝑝 = 𝐺 → ((𝐸 evalSub1 𝐹)‘𝑝) = ((𝐸 evalSub1 𝐹)‘𝐺))
9	8	fveq1d 6887	. . . . . . . 8 ⊢ (𝑝 = 𝐺 → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋))
10	9	eqeq1d 2767	. . . . . . 7 ⊢ (𝑝 = 𝐺 → ((((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 ↔ (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 ))
11		rtelextdg2lem.6	. . . . . . . . 9 ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))
12		eqid 2765	. . . . . . . . . 10 ⊢ (Base‘𝑃) = (Base‘𝑃)
13		rtelextdg2lem.2	. . . . . . . . . 10 ⊢ ⊕ = (+g‘𝑃)
14		fldsdrgfld 20931	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
15	5, 6, 14	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
16	15	fldcrngd 20872	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing)
17	1, 16	eqeltrid 2869	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ CRing)
18	17	crngringd 20352	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
19		rtelextdg2.4	. . . . . . . . . . . . 13 ⊢ 𝑃 = (Poly1‘𝐾)
20	19	ply1ring 22437	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
21	18, 20	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ Ring)
22	21	ringgrpd 20348	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
23		eqid 2765	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
24	23, 12	mgpbas 20245	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
25		rtelextdg2lem.4	. . . . . . . . . . 11 ⊢ ∧ = (.g‘(mulGrp‘𝑃))
26	23	ringmgp 20345	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
27	21, 26	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
28		2nn0 12532	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ0)
30		rtelextdg2lem.1	. . . . . . . . . . . . 13 ⊢ 𝑌 = (var1‘𝐾)
31	30, 19, 12	vr1cl 22407	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑌 ∈ (Base‘𝑃))
32	18, 31	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑃))
33	24, 25, 27, 29, 32	mulgnn0cld 19185	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∧ 𝑌) ∈ (Base‘𝑃))
34		rtelextdg2lem.3	. . . . . . . . . . . 12 ⊢ ⊗ = (.r‘𝑃)
35		rtelextdg2lem.5	. . . . . . . . . . . . 13 ⊢ 𝑈 = (algSc‘𝑃)
36	5	fldcrngd 20872	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37		sdrgsubrg 20924	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
38	6, 37	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
39		rtelextdg2.12	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝐹)
40	19, 1, 35, 12, 36, 38, 39	ressasclcl 33901	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘𝐴) ∈ (Base‘𝑃))
41	12, 34, 21, 40, 32	ringcld 20363	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃))
42		rtelextdg2.13	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐹)
43	19, 1, 35, 12, 36, 38, 42	ressasclcl 33901	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘𝐵) ∈ (Base‘𝑃))
44	12, 13, 22, 41, 43	grpcld 19038	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃))
45	12, 13, 22, 33, 44	grpcld 19038	. . . . . . . . 9 ⊢ (𝜑 → ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) ∈ (Base‘𝑃))
46	11, 45	eqeltrid 2869	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))
47	11	fveq2i 6888	. . . . . . . . . . . 12 ⊢ (coe1‘𝐺) = (coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
48	47	fveq1i 6886	. . . . . . . . . . 11 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2)
49		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐾) = (+g‘𝐾)
50	19, 12, 13, 49	coe1addfv 22456	. . . . . . . . . . . . 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 2765	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐾) = (0g‘𝐾)
53		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝐾) = (1r‘𝐾)
54	19, 30, 25, 18, 29, 52, 53	coe1mon 33917	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (coe1‘(2 ∧ 𝑌)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾))))
55		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2)
56	55	iftrued 4497	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
57		fvexd 6900	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ V)
58	54, 56, 29, 57	fvmptd 7001	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘2) = (1r‘𝐾))
59	19, 12, 13, 49	coe1addfv 22456	. . . . . . . . . . . . . . 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 20926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝑉)
63	1, 61	ressbas2 17316	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ⊆ 𝑉 → 𝐹 = (Base‘𝐾))
64	6, 62, 63	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
65	39, 64	eleqtrd 2867	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐾))
66		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐾) = (Base‘𝐾)
67		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐾) = (.r‘𝐾)
68	19, 12, 66, 35, 34, 67	coe1sclmulfv 22474	. . . . . . . . . . . . . . . . 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 33921	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (coe1‘𝑌) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾))))
71		1ne2 12462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 2
72	71	nesymi 3017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 2 = 1
73		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → (𝑖 = 1 ↔ 2 = 1))
74	72, 73	mtbiri 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 1)
75	74	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 1)
76	75	iffalsed 4500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
77		fvexd 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐾) ∈ V)
78	70, 76, 29, 77	fvmptd 7001	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘𝑌)‘2) = (0g‘𝐾))
79	78	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
80	66, 67, 52, 18, 65	ringrzd 20405	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
81	69, 79, 80	3eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (0g‘𝐾))
82	42, 64	eleqtrd 2867	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (Base‘𝐾))
83	19, 35, 66, 52	coe1scl 22478	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
84	18, 82, 83	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
85		0ne2 12461	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≠ 2
86	85	neii 2962	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 0 = 2
87		eqeq1 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑖 = 2 ↔ 0 = 2))
88	86, 87	mtbiri 330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ¬ 𝑖 = 2)
89	88, 55	nsyl3 139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
90	89	iffalsed 4500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
91	84, 90, 29, 77	fvmptd 7001	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘2) = (0g‘𝐾))
92	81, 91	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)) = ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)))
93	18	ringgrpd 20348	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Grp)
94	66, 52	grpidcl 19056	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Grp → (0g‘𝐾) ∈ (Base‘𝐾))
95	93, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐾) ∈ (Base‘𝐾))
96	66, 49, 52, 93, 95	grpridd 19061	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
97	60, 92, 96	3eqtrd 2804	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (0g‘𝐾))
98	58, 97	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)) = ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)))
99	66, 53	ringidcl 20373	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (1r‘𝐾) ∈ (Base‘𝐾))
100	18, 99	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾))
101	66, 49, 52, 93, 100	grpridd 19061	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐾))
102	36	crngringd 20352	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
103		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝐸) = (1r‘𝐸)
104	103	subrg1cl 20709	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
105	38, 104	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
106	6, 62	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝑉)
107	1, 61, 103	ress1r 33592	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Ring ∧ (1r‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → (1r‘𝐸) = (1r‘𝐾))
108	102, 105, 106, 107	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
109	101, 108	eqtr4d 2803	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐸))
110	51, 98, 109	3eqtrd 2804	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (1r‘𝐸))
111	48, 110	eqtrid 2812	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘𝐺)‘2) = (1r‘𝐸))
112	5	flddrngd 20871	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
113		drngnzr 20878	. . . . . . . . . . 11 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
114		rtelextdg2.3	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐸)
115	103, 114	nzrnz 20642	. . . . . . . . . . 11 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ 0 )
116	112, 113, 115	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐸) ≠ 0 )
117	111, 116	eqnetrd 3027	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘2) ≠ 0 )
118		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝐺 = (0g‘𝑃) → (coe1‘𝐺) = (coe1‘(0g‘𝑃)))
119	118	fveq1d 6887	. . . . . . . . . 10 ⊢ (𝐺 = (0g‘𝑃) → ((coe1‘𝐺)‘2) = ((coe1‘(0g‘𝑃))‘2))
120		eqid 2765	. . . . . . . . . . . 12 ⊢ (0g‘𝑃) = (0g‘𝑃)
121	19, 120, 52, 18, 29	coe1zfv 33920	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = (0g‘𝐾))
122	102	ringgrpd 20348	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ Grp)
123	122	grpmndd 19037	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ Mnd)
124		subrgsubg 20706	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
125	38, 124	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
126	114	subg0cl 19224	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 0 ∈ 𝐹)
127	125, 126	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ 𝐹)
128	1, 61, 114	ress0g 18842	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Mnd ∧ 0 ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → 0 = (0g‘𝐾))
129	123, 127, 106, 128	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → 0 = (0g‘𝐾))
130	121, 129	eqtr4d 2803	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = 0 )
131	119, 130	sylan9eqr 2822	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 = (0g‘𝑃)) → ((coe1‘𝐺)‘2) = 0 )
132	117, 131	mteqand 3051	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃))
133	11	fveq2i 6888	. . . . . . . . . . 11 ⊢ ((deg1‘𝐾)‘𝐺) = ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
134		eqid 2765	. . . . . . . . . . . . 13 ⊢ (deg1‘𝐾) = (deg1‘𝐾)
135		2re 12326	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
136	135	rexri 11278	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ*
137	136	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ*)
138	134, 19, 12	deg1xrcl 26270	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
139	41, 138	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
140		1xr 11279	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ*
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ*)
142	134, 19, 66, 12, 34, 35	deg1mul3le 26305	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
143	18, 65, 32, 142	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
144	1, 15	eqeltrid 2869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ Field)
145	144	flddrngd 20871	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ DivRing)
146		drngnzr 20878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
147	145, 146	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ NzRing)
148	134, 19, 30, 147	deg1vr 33922	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘𝑌) = 1)
149	143, 148	breqtrd 5139	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ 1)
150		1lt2 12424	. . . . . . . . . . . . . . . . 17 ⊢ 1 < 2
151	150	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 < 2)
152	139, 141, 137, 149, 151	xrlelttrd 13197	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) < 2)
153	134, 19, 12	deg1xrcl 26270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝐵) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
154	43, 153	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
155		0xr 11267	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ*
156	155	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℝ*)
157	134, 19, 66, 35	deg1sclle 26300	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
158	18, 82, 157	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
159		2pos 12356	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
160	159	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
161	154, 156, 137, 158, 160	xrlelttrd 13197	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) < 2)
162	19, 134, 18, 12, 13, 41, 43, 137, 152, 161	deg1addlt 33930	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < 2)
163	134, 19, 30, 23, 25	deg1pw 26309	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ NzRing ∧ 2 ∈ ℕ0) → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
164	147, 29, 163	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
165	162, 164	breqtrrd 5141	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < ((deg1‘𝐾)‘(2 ∧ 𝑌)))
166	19, 134, 18, 12, 13, 33, 44, 165	deg1add 26291	. . . . . . . . . . . 12 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = ((deg1‘𝐾)‘(2 ∧ 𝑌)))
167	166, 164	eqtrd 2800	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = 2)
168	133, 167	eqtrid 2812	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐾)‘𝐺) = 2)
169	168	fveq2d 6889	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = ((coe1‘𝐺)‘2))
170	169, 111, 108	3eqtrd 2804	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾))
171		eqid 2765	. . . . . . . . 9 ⊢ (Monic1p‘𝐾) = (Monic1p‘𝐾)
172	19, 12, 120, 134, 171, 53	ismon1p 26331	. . . . . . . 8 ⊢ (𝐺 ∈ (Monic1p‘𝐾) ↔ (𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ (0g‘𝑃) ∧ ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾)))
173	46, 132, 170, 172	syl3anbrc 1362	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝐾))
174		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝐸 evalSub1 𝐹) = (𝐸 evalSub1 𝐹)
175		eqid 2765	. . . . . . . . . . . 12 ⊢ (eval1‘𝐸) = (eval1‘𝐸)
176	174, 61, 19, 1, 12, 175, 36, 38	ressply1evl 22560	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 evalSub1 𝐹) = ((eval1‘𝐸) ↾ (Base‘𝑃)))
177	176	fveq1d 6887	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺))
178	46	fvresd 6905	. . . . . . . . . 10 ⊢ (𝜑 → (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺) = ((eval1‘𝐸)‘𝐺))
179	177, 178	eqtrd 2800	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = ((eval1‘𝐸)‘𝐺))
180	179	fveq1d 6887	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = (((eval1‘𝐸)‘𝐺)‘𝑋))
181		eqid 2765	. . . . . . . . 9 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
182		eqid 2765	. . . . . . . . 9 ⊢ (Base‘(Poly1‘𝐸)) = (Base‘(Poly1‘𝐸))
183		rtelextdg2.6	. . . . . . . . 9 ⊢ · = (.r‘𝐸)
184		rtelextdg2.7	. . . . . . . . 9 ⊢ + = (+g‘𝐸)
185		rtelextdg2.8	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐸))
186		eqid 2765	. . . . . . . . 9 ⊢ (coe1‘𝐺) = (coe1‘𝐺)
187		eqid 2765	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘𝐺)‘2)
188		eqid 2765	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘𝐺)‘1)
189		eqid 2765	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘𝐺)‘0)
190		eqid 2765	. . . . . . . . . . . 12 ⊢ (PwSer1‘𝐾) = (PwSer1‘𝐾)
191		eqid 2765	. . . . . . . . . . . 12 ⊢ (Base‘(PwSer1‘𝐾)) = (Base‘(PwSer1‘𝐾))
192	181, 1, 19, 12, 38, 190, 191, 182	ressply1bas2 22417	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑃) = ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
193	46, 192	eleqtrd 2867	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
194	193	elin2d 4158	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Base‘(Poly1‘𝐸)))
195	1, 3, 19, 12, 46, 38	ressdeg1 33896	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = ((deg1‘𝐾)‘𝐺))
196	195, 168	eqtrd 2800	. . . . . . . . 9 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = 2)
197	181, 175, 61, 182, 183, 184, 185, 186, 3, 187, 188, 189, 36, 194, 196, 7	evl1deg2 33907	. . . . . . . 8 ⊢ (𝜑 → (((eval1‘𝐸)‘𝐺)‘𝑋) = ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))))
198	111	oveq1d 7431	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = ((1r‘𝐸) · (2 ↑ 𝑋)))
199		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (mulGrp‘𝐸) = (mulGrp‘𝐸)
200	199, 61	mgpbas 20245	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Base‘(mulGrp‘𝐸))
201	199	ringmgp 20345	. . . . . . . . . . . . . 14 ⊢ (𝐸 ∈ Ring → (mulGrp‘𝐸) ∈ Mnd)
202	102, 201	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝐸) ∈ Mnd)
203	200, 185, 202, 29, 7	mulgnn0cld 19185	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝑉)
204	61, 183, 103, 102, 203	ringlidmd 20380	. . . . . . . . . . 11 ⊢ (𝜑 → ((1r‘𝐸) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
205	198, 204	eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
206	47	fveq1i 6886	. . . . . . . . . . . . 13 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1)
207		1nn0 12531	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ0
208	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ0)
209	19, 12, 13, 49	coe1addfv 22456	. . . . . . . . . . . . . . 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 2962	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 1 = 2
212		eqeq1 2769	. . . . . . . . . . . . . . . . . . . 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 4500	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
217	54, 216, 208, 77	fvmptd 7001	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘1) = (0g‘𝐾))
218	19, 12, 13, 49	coe1addfv 22456	. . . . . . . . . . . . . . . . 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 22474	. . . . . . . . . . . . . . . . . . 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 4497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
224	70, 223, 208, 57	fvmptd 7001	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((coe1‘𝑌)‘1) = (1r‘𝐾))
225	224	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)) = (𝐴(.r‘𝐾)(1r‘𝐾)))
226	66, 67, 53, 18, 65	ringridmd 20381	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)(1r‘𝐾)) = 𝐴)
227	221, 225, 226	3eqtrd 2804	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = 𝐴)
228		0ne1 12323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 1
229	228	nesymi 3017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
230		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0))
231	229, 230	mtbiri 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
232	231	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
233	232	iffalsed 4500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
234	84, 233, 208, 77	fvmptd 7001	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘1) = (0g‘𝐾))
235	227, 234	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)) = (𝐴(+g‘𝐾)(0g‘𝐾)))
236	66, 49, 52, 93, 65	grpridd 19061	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(+g‘𝐾)(0g‘𝐾)) = 𝐴)
237	219, 235, 236	3eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = 𝐴)
238	217, 237	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)) = ((0g‘𝐾)(+g‘𝐾)𝐴))
239	66, 49, 52, 93, 65	grplidd 19060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐴) = 𝐴)
240	210, 238, 239	3eqtrd 2804	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = 𝐴)
241	206, 240	eqtrid 2812	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘𝐺)‘1) = 𝐴)
242	241	oveq1d 7431	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘1) · 𝑋) = (𝐴 · 𝑋))
243	47	fveq1i 6886	. . . . . . . . . . . 12 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0)
244		0nn0 12530	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℕ0
245	244	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℕ0)
246	19, 12, 13, 49	coe1addfv 22456	. . . . . . . . . . . . . 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 4500	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
250	54, 249, 245, 77	fvmptd 7001	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘0) = (0g‘𝐾))
251	19, 12, 13, 49	coe1addfv 22456	. . . . . . . . . . . . . . . 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 22474	. . . . . . . . . . . . . . . . . 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 2962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 0 = 1
256		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 = 1 ↔ 0 = 1))
257	255, 256	mtbiri 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → ¬ 𝑖 = 1)
258	257	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 1)
259	258	iffalsed 4500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
260	70, 259, 245, 77	fvmptd 7001	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘𝑌)‘0) = (0g‘𝐾))
261	260	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
262	254, 261, 80	3eqtrd 2804	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (0g‘𝐾))
263	19, 35, 66	ply1sclid 22479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
264	18, 82, 263	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
265	264	eqcomd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘0) = 𝐵)
266	262, 265	oveq12d 7434	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
267	66, 49, 52, 93, 82	grplidd 19060	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐵) = 𝐵)
268	252, 266, 267	3eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = 𝐵)
269	250, 268	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
270	247, 269, 267	3eqtrd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = 𝐵)
271	243, 270	eqtrid 2812	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘𝐺)‘0) = 𝐵)
272	242, 271	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝜑 → ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0)) = ((𝐴 · 𝑋) + 𝐵))
273	205, 272	oveq12d 7434	. . . . . . . . 9 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)))
274		rtelextdg2.14	. . . . . . . . 9 ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )
275	273, 274	eqtrd 2800	. . . . . . . 8 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = 0 )
276	180, 197, 275	3eqtrd 2804	. . . . . . 7 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 )
277	10, 173, 276	rspcedvdw 3586	. . . . . 6 ⊢ (𝜑 → ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )
278	174, 1, 61, 114, 36, 38	elirng 34116	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )))
279	7, 277, 278	mpbir2and 726	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
280	1, 2, 3, 4, 5, 6, 279	algextdeg 34155	. . . 4 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)))
281	1	fveq2i 6888	. . . . . . 7 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
282	19, 281	eqtri 2788	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
283		eqid 2765	. . . . . 6 ⊢ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 } = {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 }
284		eqid 2765	. . . . . 6 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
285		eqid 2765	. . . . . 6 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
286	174, 282, 61, 5, 6, 7, 114, 283, 284, 285, 4	minplycl 34136	. . . . 5 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝑋) ∈ (Base‘𝑃))
287	1, 3, 19, 12, 286, 38	ressdeg1 33896	. . . 4 ⊢ (𝜑 → ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
288	280, 287	eqtrd 2800	. . 3 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
289	1	fveq2i 6888	. . . 4 ⊢ (deg1‘𝐾) = (deg1‘(𝐸 ↾s 𝐹))
290	174, 282, 61, 5, 6, 7, 114, 4, 289, 120, 12, 276, 46, 132	minplymindeg 34138	. . 3 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)) ≤ ((deg1‘𝐾)‘𝐺))
291	288, 290	eqbrtrd 5135	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ ((deg1‘𝐾)‘𝐺))
292	291, 168	breqtrd 5139	1 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091  {crab 3418  Vcvv 3457   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ifcif 4489  {csn 4591   class class class wbr 5111   ↦ cmpt 5194  dom cdm 5663   ↾ cres 5665  ‘cfv 6540  (class class class)co 7416  0cc0 11111  1c1 11112  ℝ^*cxr 11253   < clt 11254   ≤ cle 11255  2c2 12306  ℕ₀cn0 12515  Basecbs 17287   ↾_s cress 17308  +_gcplusg 17328  ._rcmulr 17329  0_gc0g 17510  Mndcmnd 18814  Grpcgrp 19024  ._gcmg 19157  SubGrpcsubg 19210  mulGrpcmgp 20240  1_rcur 20287  Ringcrg 20339  CRingccrg 20340  NzRingcnzr 20639  SubRingcsubrg 20698  DivRingcdr 20857  Fieldcfield 20858  SubDRingcsdrg 20919  RSpancrsp 21361  algSccascl 22032  PwSer₁cps1 22365  var₁cv1 22366  Poly₁cpl1 22367  coe₁cco1 22368   evalSub₁ ces1 22503  eval₁ce1 22504  deg₁cdg1 26242  Monic_1pcmn1 26314  idlGen_1pcig1p 26318   fldGen cfldgen 33671  [:]cextdg 34070   IntgRing cirng 34113   minPoly cminply 34129

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-reg 9557  ax-inf2 9613  ax-ac2 10458  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188  ax-pre-sup 11189  ax-addf 11190

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7680  df-ofr 7681  df-rpss 7726  df-om 7865  df-1st 7988  df-2nd 7989  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 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9325  df-sup 9405  df-inf 9406  df-oi 9475  df-r1 9739  df-rank 9740  df-scott 9861  df-dju 9899  df-card 9937  df-acn 9940  df-ac 10112  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-nn 12245  df-2 12314  df-3 12315  df-4 12316  df-5 12317  df-6 12318  df-7 12319  df-8 12320  df-9 12321  df-n0 12516  df-xnn0 12589  df-z 12603  df-dec 12724  df-uz 12875  df-ico 13390  df-fz 13548  df-fzo 13696  df-seq 14052  df-hash 14381  df-struct 17225  df-sets 17242  df-slot 17260  df-ndx 17272  df-base 17288  df-ress 17309  df-plusg 17341  df-mulr 17342  df-starv 17343  df-sca 17344  df-vsca 17345  df-ip 17346  df-tset 17347  df-ple 17348  df-ocomp 17349  df-ds 17350  df-unif 17351  df-hom 17352  df-cco 17353  df-0g 17512  df-gsum 17513  df-prds 17518  df-pws 17520  df-imas 17580  df-qus 17581  df-mre 17656  df-mrc 17657  df-mri 17658  df-acs 17659  df-proset 18368  df-drs 18369  df-poset 18387  df-ipo 18602  df-mgm 18716  df-sgrp 18799  df-mnd 18815  df-mhm 18865  df-submnd 18866  df-grp 19027  df-minusg 19028  df-sbg 19029  df-mulg 19158  df-subg 19213  df-nsg 19214  df-eqg 19215  df-ghm 19308  df-gim 19353  df-cntz 19411  df-oppg 19440  df-lsm 19730  df-cmn 19876  df-abl 19877  df-mgp 20241  df-rng 20255  df-ur 20288  df-srg 20293  df-ring 20341  df-cring 20342  df-oppr 20445  df-dvdsr 20465  df-unit 20466  df-irred 20467  df-invr 20496  df-dvr 20509  df-rhm 20580  df-nzr 20640  df-subrng 20675  df-subrg 20699  df-rlreg 20823  df-domn 20824  df-idom 20825  df-drng 20859  df-field 20860  df-sdrg 20920  df-lmod 21013  df-lss 21083  df-lsp 21123  df-lmhm 21173  df-lmim 21174  df-lmic 21175  df-lbs 21226  df-lvec 21254  df-sra 21324  df-rgmod 21325  df-lidl 21362  df-rsp 21363  df-2idl 21419  df-lpidl 21520  df-lpir 21521  df-pid 21535  df-cnfld 21553  df-dsmm 21912  df-frlm 21927  df-uvc 21963  df-lindf 21986  df-linds 21987  df-assa 22033  df-asp 22034  df-ascl 22035  df-psr 22089  df-mvr 22090  df-mpl 22091  df-opsr 22093  df-evls 22255  df-evl 22256  df-psr1 22370  df-vr1 22371  df-ply1 22372  df-coe1 22373  df-evls1 22505  df-evl1 22506  df-mdeg 26243  df-deg1 26244  df-mon1 26319  df-uc1p 26320  df-q1p 26321  df-r1p 26322  df-ig1p 26323  df-fldgen 33672  df-mxidl 33783  df-dim 34030  df-fldext 34071  df-extdg 34072  df-irng 34114  df-minply 34130

This theorem is used by:  rtelextdg2  34157