Theorem rtelextdg2lem 33723

Description: Lemma for rtelextdg2 33724: 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 2730	. . . . 5 ⊢ (deg1‘𝐸) = (deg1‘𝐸)
4		eqid 2730	. . . . 5 ⊢ (𝐸 minPoly 𝐹) = (𝐸 minPoly 𝐹)
5		rtelextdg2.9	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ Field)
6		rtelextdg2.10	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸))
7		rtelextdg2.11	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
8		fveq2 6861	. . . . . . . . 9 ⊢ (𝑝 = 𝐺 → ((𝐸 evalSub1 𝐹)‘𝑝) = ((𝐸 evalSub1 𝐹)‘𝐺))
9	8	fveq1d 6863	. . . . . . . 8 ⊢ (𝑝 = 𝐺 → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋))
10	9	eqeq1d 2732	. . . . . . 7 ⊢ (𝑝 = 𝐺 → ((((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 ↔ (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 ))
11		rtelextdg2lem.6	. . . . . . . . 9 ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))
12		eqid 2730	. . . . . . . . . 10 ⊢ (Base‘𝑃) = (Base‘𝑃)
13		rtelextdg2lem.2	. . . . . . . . . 10 ⊢ ⊕ = (+g‘𝑃)
14		fldsdrgfld 20714	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field)
15	5, 6, 14	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field)
16	15	fldcrngd 20658	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing)
17	1, 16	eqeltrid 2833	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ CRing)
18	17	crngringd 20162	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ Ring)
19		rtelextdg2.4	. . . . . . . . . . . . 13 ⊢ 𝑃 = (Poly1‘𝐾)
20	19	ply1ring 22139	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑃 ∈ Ring)
21	18, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ Ring)
22	21	ringgrpd 20158	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ Grp)
23		eqid 2730	. . . . . . . . . . . 12 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
24	23, 12	mgpbas 20061	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
25		rtelextdg2lem.4	. . . . . . . . . . 11 ⊢ ∧ = (.g‘(mulGrp‘𝑃))
26	23	ringmgp 20155	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
27	21, 26	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
28		2nn0 12466	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ0
29	28	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ0)
30		rtelextdg2lem.1	. . . . . . . . . . . . 13 ⊢ 𝑌 = (var1‘𝐾)
31	30, 19, 12	vr1cl 22109	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Ring → 𝑌 ∈ (Base‘𝑃))
32	18, 31	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑃))
33	24, 25, 27, 29, 32	mulgnn0cld 19034	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∧ 𝑌) ∈ (Base‘𝑃))
34		rtelextdg2lem.3	. . . . . . . . . . . 12 ⊢ ⊗ = (.r‘𝑃)
35		rtelextdg2lem.5	. . . . . . . . . . . . 13 ⊢ 𝑈 = (algSc‘𝑃)
36	5	fldcrngd 20658	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ CRing)
37		sdrgsubrg 20707	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸))
38	6, 37	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸))
39		rtelextdg2.12	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝐹)
40	19, 1, 35, 12, 36, 38, 39	ressasclcl 33547	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈‘𝐴) ∈ (Base‘𝑃))
41	12, 34, 21, 40, 32	ringcld 20176	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃))
42		rtelextdg2.13	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝐹)
43	19, 1, 35, 12, 36, 38, 42	ressasclcl 33547	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈‘𝐵) ∈ (Base‘𝑃))
44	12, 13, 22, 41, 43	grpcld 18886	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃))
45	12, 13, 22, 33, 44	grpcld 18886	. . . . . . . . 9 ⊢ (𝜑 → ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) ∈ (Base‘𝑃))
46	11, 45	eqeltrid 2833	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃))
47	11	fveq2i 6864	. . . . . . . . . . . 12 ⊢ (coe1‘𝐺) = (coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
48	47	fveq1i 6862	. . . . . . . . . . 11 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2)
49		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (+g‘𝐾) = (+g‘𝐾)
50	19, 12, 13, 49	coe1addfv 22158	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)))
51	18, 33, 44, 29, 50	syl31anc 1375	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)))
52		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝐾) = (0g‘𝐾)
53		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (1r‘𝐾) = (1r‘𝐾)
54	19, 30, 25, 18, 29, 52, 53	coe1mon 33561	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (coe1‘(2 ∧ 𝑌)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾))))
55		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 2) → 𝑖 = 2)
56	55	iftrued 4499	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
57		fvexd 6876	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ V)
58	54, 56, 29, 57	fvmptd 6978	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘2) = (1r‘𝐾))
59	19, 12, 13, 49	coe1addfv 22158	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)))
60	18, 41, 43, 29, 59	syl31anc 1375	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)))
61		rtelextdg2.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑉 = (Base‘𝐸)
62	61	sdrgss 20709	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ⊆ 𝑉)
63	1, 61	ressbas2 17215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ⊆ 𝑉 → 𝐹 = (Base‘𝐾))
64	6, 62, 63	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 = (Base‘𝐾))
65	39, 64	eleqtrd 2831	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐾))
66		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐾) = (Base‘𝐾)
67		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (.r‘𝐾) = (.r‘𝐾)
68	19, 12, 66, 35, 34, 67	coe1sclmulfv 22176	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)))
69	18, 65, 32, 29, 68	syl121anc 1377	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)))
70	19, 30, 18, 52, 53	coe1vr1 33564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (coe1‘𝑌) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾))))
71		1ne2 12396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 2
72	71	nesymi 2983	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 2 = 1
73		eqeq1 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → (𝑖 = 1 ↔ 2 = 1))
74	72, 73	mtbiri 327	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 1)
75	74	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 1)
76	75	iffalsed 4502	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
77		fvexd 6876	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (0g‘𝐾) ∈ V)
78	70, 76, 29, 77	fvmptd 6978	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘𝑌)‘2) = (0g‘𝐾))
79	78	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘2)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
80	66, 67, 52, 18, 65	ringrzd 20212	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(.r‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
81	69, 79, 80	3eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2) = (0g‘𝐾))
82	42, 64	eleqtrd 2831	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (Base‘𝐾))
83	19, 35, 66, 52	coe1scl 22180	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
84	18, 82, 83	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (coe1‘(𝑈‘𝐵)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 𝐵, (0g‘𝐾))))
85		0ne2 12395	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≠ 2
86	85	neii 2928	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 0 = 2
87		eqeq1 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 0 → (𝑖 = 2 ↔ 0 = 2))
88	86, 87	mtbiri 327	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 0 → ¬ 𝑖 = 2)
89	88, 55	nsyl3 138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
90	89	iffalsed 4502	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 2) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
91	84, 90, 29, 77	fvmptd 6978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘2) = (0g‘𝐾))
92	81, 91	oveq12d 7408	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘2)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘2)) = ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)))
93	18	ringgrpd 20158	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ Grp)
94	66, 52	grpidcl 18904	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ Grp → (0g‘𝐾) ∈ (Base‘𝐾))
95	93, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0g‘𝐾) ∈ (Base‘𝐾))
96	66, 49, 52, 93, 95	grpridd 18909	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (0g‘𝐾))
97	60, 92, 96	3eqtrd 2769	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2) = (0g‘𝐾))
98	58, 97	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘2)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘2)) = ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)))
99	66, 53	ringidcl 20181	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ Ring → (1r‘𝐾) ∈ (Base‘𝐾))
100	18, 99	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾))
101	66, 49, 52, 93, 100	grpridd 18909	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐾))
102	36	crngringd 20162	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 ∈ Ring)
103		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝐸) = (1r‘𝐸)
104	103	subrg1cl 20496	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (SubRing‘𝐸) → (1r‘𝐸) ∈ 𝐹)
105	38, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1r‘𝐸) ∈ 𝐹)
106	6, 62	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ⊆ 𝑉)
107	1, 61, 103	ress1r 33192	. . . . . . . . . . . . . 14 ⊢ ((𝐸 ∈ Ring ∧ (1r‘𝐸) ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → (1r‘𝐸) = (1r‘𝐾))
108	102, 105, 106, 107	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1r‘𝐸) = (1r‘𝐾))
109	101, 108	eqtr4d 2768	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1r‘𝐾)(+g‘𝐾)(0g‘𝐾)) = (1r‘𝐸))
110	51, 98, 109	3eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘2) = (1r‘𝐸))
111	48, 110	eqtrid 2777	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘𝐺)‘2) = (1r‘𝐸))
112	5	flddrngd 20657	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ DivRing)
113		drngnzr 20664	. . . . . . . . . . 11 ⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing)
114		rtelextdg2.3	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐸)
115	103, 114	nzrnz 20431	. . . . . . . . . . 11 ⊢ (𝐸 ∈ NzRing → (1r‘𝐸) ≠ 0 )
116	112, 113, 115	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (1r‘𝐸) ≠ 0 )
117	111, 116	eqnetrd 2993	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘2) ≠ 0 )
118		fveq2 6861	. . . . . . . . . . 11 ⊢ (𝐺 = (0g‘𝑃) → (coe1‘𝐺) = (coe1‘(0g‘𝑃)))
119	118	fveq1d 6863	. . . . . . . . . 10 ⊢ (𝐺 = (0g‘𝑃) → ((coe1‘𝐺)‘2) = ((coe1‘(0g‘𝑃))‘2))
120		eqid 2730	. . . . . . . . . . . 12 ⊢ (0g‘𝑃) = (0g‘𝑃)
121	19, 120, 52, 18, 29	coe1zfv 33563	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = (0g‘𝐾))
122	102	ringgrpd 20158	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ Grp)
123	122	grpmndd 18885	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ Mnd)
124		subrgsubg 20493	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ (SubRing‘𝐸) → 𝐹 ∈ (SubGrp‘𝐸))
125	38, 124	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝐸))
126	114	subg0cl 19073	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (SubGrp‘𝐸) → 0 ∈ 𝐹)
127	125, 126	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ 𝐹)
128	1, 61, 114	ress0g 18696	. . . . . . . . . . . 12 ⊢ ((𝐸 ∈ Mnd ∧ 0 ∈ 𝐹 ∧ 𝐹 ⊆ 𝑉) → 0 = (0g‘𝐾))
129	123, 127, 106, 128	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → 0 = (0g‘𝐾))
130	121, 129	eqtr4d 2768	. . . . . . . . . 10 ⊢ (𝜑 → ((coe1‘(0g‘𝑃))‘2) = 0 )
131	119, 130	sylan9eqr 2787	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 = (0g‘𝑃)) → ((coe1‘𝐺)‘2) = 0 )
132	117, 131	mteqand 3017	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃))
133	11	fveq2i 6864	. . . . . . . . . . 11 ⊢ ((deg1‘𝐾)‘𝐺) = ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))
134		eqid 2730	. . . . . . . . . . . . 13 ⊢ (deg1‘𝐾) = (deg1‘𝐾)
135		2re 12267	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
136	135	rexri 11239	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ*
137	136	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ*)
138	134, 19, 12	deg1xrcl 25994	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
139	41, 138	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ∈ ℝ*)
140		1xr 11240	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ*
141	140	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ*)
142	134, 19, 66, 12, 34, 35	deg1mul3le 26029	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
143	18, 65, 32, 142	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ ((deg1‘𝐾)‘𝑌))
144	1, 15	eqeltrid 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐾 ∈ Field)
145	144	flddrngd 20657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ DivRing)
146		drngnzr 20664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ DivRing → 𝐾 ∈ NzRing)
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ NzRing)
148	134, 19, 30, 147	deg1vr 33565	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((deg1‘𝐾)‘𝑌) = 1)
149	143, 148	breqtrd 5136	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) ≤ 1)
150		1lt2 12359	. . . . . . . . . . . . . . . . 17 ⊢ 1 < 2
151	150	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 < 2)
152	139, 141, 137, 149, 151	xrlelttrd 13127	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝑈‘𝐴) ⊗ 𝑌)) < 2)
153	134, 19, 12	deg1xrcl 25994	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈‘𝐵) ∈ (Base‘𝑃) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
154	43, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ∈ ℝ*)
155		0xr 11228	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ*
156	155	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ∈ ℝ*)
157	134, 19, 66, 35	deg1sclle 26024	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
158	18, 82, 157	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) ≤ 0)
159		2pos 12296	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
160	159	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 2)
161	154, 156, 137, 158, 160	xrlelttrd 13127	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((deg1‘𝐾)‘(𝑈‘𝐵)) < 2)
162	19, 134, 18, 12, 13, 41, 43, 137, 152, 161	deg1addlt 33572	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < 2)
163	134, 19, 30, 23, 25	deg1pw 26033	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ NzRing ∧ 2 ∈ ℕ0) → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
164	147, 29, 163	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((deg1‘𝐾)‘(2 ∧ 𝑌)) = 2)
165	162, 164	breqtrrd 5138	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((deg1‘𝐾)‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) < ((deg1‘𝐾)‘(2 ∧ 𝑌)))
166	19, 134, 18, 12, 13, 33, 44, 165	deg1add 26015	. . . . . . . . . . . 12 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = ((deg1‘𝐾)‘(2 ∧ 𝑌)))
167	166, 164	eqtrd 2765	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg1‘𝐾)‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))) = 2)
168	133, 167	eqtrid 2777	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐾)‘𝐺) = 2)
169	168	fveq2d 6865	. . . . . . . . 9 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = ((coe1‘𝐺)‘2))
170	169, 111, 108	3eqtrd 2769	. . . . . . . 8 ⊢ (𝜑 → ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾))
171		eqid 2730	. . . . . . . . 9 ⊢ (Monic1p‘𝐾) = (Monic1p‘𝐾)
172	19, 12, 120, 134, 171, 53	ismon1p 26055	. . . . . . . 8 ⊢ (𝐺 ∈ (Monic1p‘𝐾) ↔ (𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ (0g‘𝑃) ∧ ((coe1‘𝐺)‘((deg1‘𝐾)‘𝐺)) = (1r‘𝐾)))
173	46, 132, 170, 172	syl3anbrc 1344	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘𝐾))
174		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝐸 evalSub1 𝐹) = (𝐸 evalSub1 𝐹)
175		eqid 2730	. . . . . . . . . . . 12 ⊢ (eval1‘𝐸) = (eval1‘𝐸)
176	174, 61, 19, 1, 12, 175, 36, 38	ressply1evl 22264	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 evalSub1 𝐹) = ((eval1‘𝐸) ↾ (Base‘𝑃)))
177	176	fveq1d 6863	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺))
178	46	fvresd 6881	. . . . . . . . . 10 ⊢ (𝜑 → (((eval1‘𝐸) ↾ (Base‘𝑃))‘𝐺) = ((eval1‘𝐸)‘𝐺))
179	177, 178	eqtrd 2765	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 evalSub1 𝐹)‘𝐺) = ((eval1‘𝐸)‘𝐺))
180	179	fveq1d 6863	. . . . . . . 8 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = (((eval1‘𝐸)‘𝐺)‘𝑋))
181		eqid 2730	. . . . . . . . 9 ⊢ (Poly1‘𝐸) = (Poly1‘𝐸)
182		eqid 2730	. . . . . . . . 9 ⊢ (Base‘(Poly1‘𝐸)) = (Base‘(Poly1‘𝐸))
183		rtelextdg2.6	. . . . . . . . 9 ⊢ · = (.r‘𝐸)
184		rtelextdg2.7	. . . . . . . . 9 ⊢ + = (+g‘𝐸)
185		rtelextdg2.8	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐸))
186		eqid 2730	. . . . . . . . 9 ⊢ (coe1‘𝐺) = (coe1‘𝐺)
187		eqid 2730	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘2) = ((coe1‘𝐺)‘2)
188		eqid 2730	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘𝐺)‘1)
189		eqid 2730	. . . . . . . . 9 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘𝐺)‘0)
190		eqid 2730	. . . . . . . . . . . 12 ⊢ (PwSer1‘𝐾) = (PwSer1‘𝐾)
191		eqid 2730	. . . . . . . . . . . 12 ⊢ (Base‘(PwSer1‘𝐾)) = (Base‘(PwSer1‘𝐾))
192	181, 1, 19, 12, 38, 190, 191, 182	ressply1bas2 22119	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑃) = ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
193	46, 192	eleqtrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ ((Base‘(PwSer1‘𝐾)) ∩ (Base‘(Poly1‘𝐸))))
194	193	elin2d 4171	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (Base‘(Poly1‘𝐸)))
195	1, 3, 19, 12, 46, 38	ressdeg1 33542	. . . . . . . . . 10 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = ((deg1‘𝐾)‘𝐺))
196	195, 168	eqtrd 2765	. . . . . . . . 9 ⊢ (𝜑 → ((deg1‘𝐸)‘𝐺) = 2)
197	181, 175, 61, 182, 183, 184, 185, 186, 3, 187, 188, 189, 36, 194, 196, 7	evl1deg2 33553	. . . . . . . 8 ⊢ (𝜑 → (((eval1‘𝐸)‘𝐺)‘𝑋) = ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))))
198	111	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = ((1r‘𝐸) · (2 ↑ 𝑋)))
199		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (mulGrp‘𝐸) = (mulGrp‘𝐸)
200	199, 61	mgpbas 20061	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Base‘(mulGrp‘𝐸))
201	199	ringmgp 20155	. . . . . . . . . . . . . 14 ⊢ (𝐸 ∈ Ring → (mulGrp‘𝐸) ∈ Mnd)
202	102, 201	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mulGrp‘𝐸) ∈ Mnd)
203	200, 185, 202, 29, 7	mulgnn0cld 19034	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 ↑ 𝑋) ∈ 𝑉)
204	61, 183, 103, 102, 203	ringlidmd 20188	. . . . . . . . . . 11 ⊢ (𝜑 → ((1r‘𝐸) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
205	198, 204	eqtrd 2765	. . . . . . . . . 10 ⊢ (𝜑 → (((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) = (2 ↑ 𝑋))
206	47	fveq1i 6862	. . . . . . . . . . . . 13 ⊢ ((coe1‘𝐺)‘1) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1)
207		1nn0 12465	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ0
208	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℕ0)
209	19, 12, 13, 49	coe1addfv 22158	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)))
210	18, 33, 44, 208, 209	syl31anc 1375	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)))
211	71	neii 2928	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 1 = 2
212		eqeq1 2734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → (𝑖 = 2 ↔ 1 = 2))
213	212	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 1 → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
214	213	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → (¬ 𝑖 = 2 ↔ ¬ 1 = 2))
215	211, 214	mpbiri 258	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 2)
216	215	iffalsed 4502	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
217	54, 216, 208, 77	fvmptd 6978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘1) = (0g‘𝐾))
218	19, 12, 13, 49	coe1addfv 22158	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)))
219	18, 41, 43, 208, 218	syl31anc 1375	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)))
220	19, 12, 66, 35, 34, 67	coe1sclmulfv 22176	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)))
221	18, 65, 32, 208, 220	syl121anc 1377	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)))
222		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 = 1) → 𝑖 = 1)
223	222	iftrued 4499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (1r‘𝐾))
224	70, 223, 208, 57	fvmptd 6978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((coe1‘𝑌)‘1) = (1r‘𝐾))
225	224	oveq2d 7406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘1)) = (𝐴(.r‘𝐾)(1r‘𝐾)))
226	66, 67, 53, 18, 65	ringridmd 20189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴(.r‘𝐾)(1r‘𝐾)) = 𝐴)
227	221, 225, 226	3eqtrd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1) = 𝐴)
228		0ne1 12264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 1
229	228	nesymi 2983	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
230		eqeq1 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → (𝑖 = 0 ↔ 1 = 0))
231	229, 230	mtbiri 327	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
232	231	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
233	232	iffalsed 4502	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 = 1) → if(𝑖 = 0, 𝐵, (0g‘𝐾)) = (0g‘𝐾))
234	84, 233, 208, 77	fvmptd 6978	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘1) = (0g‘𝐾))
235	227, 234	oveq12d 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘1)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘1)) = (𝐴(+g‘𝐾)(0g‘𝐾)))
236	66, 49, 52, 93, 65	grpridd 18909	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴(+g‘𝐾)(0g‘𝐾)) = 𝐴)
237	219, 235, 236	3eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1) = 𝐴)
238	217, 237	oveq12d 7408	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘1)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘1)) = ((0g‘𝐾)(+g‘𝐾)𝐴))
239	66, 49, 52, 93, 65	grplidd 18908	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐴) = 𝐴)
240	210, 238, 239	3eqtrd 2769	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘1) = 𝐴)
241	206, 240	eqtrid 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘𝐺)‘1) = 𝐴)
242	241	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝜑 → (((coe1‘𝐺)‘1) · 𝑋) = (𝐴 · 𝑋))
243	47	fveq1i 6862	. . . . . . . . . . . 12 ⊢ ((coe1‘𝐺)‘0) = ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0)
244		0nn0 12464	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℕ0
245	244	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℕ0)
246	19, 12, 13, 49	coe1addfv 22158	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Ring ∧ (2 ∧ 𝑌) ∈ (Base‘𝑃) ∧ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)))
247	18, 33, 44, 245, 246	syl31anc 1375	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)))
248	88	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 2)
249	248	iffalsed 4502	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 2, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
250	54, 249, 245, 77	fvmptd 6978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(2 ∧ 𝑌))‘0) = (0g‘𝐾))
251	19, 12, 13, 49	coe1addfv 22158	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ Ring ∧ ((𝑈‘𝐴) ⊗ 𝑌) ∈ (Base‘𝑃) ∧ (𝑈‘𝐵) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)))
252	18, 41, 43, 245, 251	syl31anc 1375	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)))
253	19, 12, 66, 35, 34, 67	coe1sclmulfv 22176	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ (𝐴 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)))
254	18, 65, 32, 245, 253	syl121anc 1377	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)))
255	228	neii 2928	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 0 = 1
256		eqeq1 2734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 = 1 ↔ 0 = 1))
257	255, 256	mtbiri 327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → ¬ 𝑖 = 1)
258	257	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 = 0) → ¬ 𝑖 = 1)
259	258	iffalsed 4502	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 = 0) → if(𝑖 = 1, (1r‘𝐾), (0g‘𝐾)) = (0g‘𝐾))
260	70, 259, 245, 77	fvmptd 6978	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((coe1‘𝑌)‘0) = (0g‘𝐾))
261	260	oveq2d 7406	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴(.r‘𝐾)((coe1‘𝑌)‘0)) = (𝐴(.r‘𝐾)(0g‘𝐾)))
262	254, 261, 80	3eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0) = (0g‘𝐾))
263	19, 35, 66	ply1sclid 22181	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Ring ∧ 𝐵 ∈ (Base‘𝐾)) → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
264	18, 82, 263	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 = ((coe1‘(𝑈‘𝐵))‘0))
265	264	eqcomd 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((coe1‘(𝑈‘𝐵))‘0) = 𝐵)
266	262, 265	oveq12d 7408	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((coe1‘((𝑈‘𝐴) ⊗ 𝑌))‘0)(+g‘𝐾)((coe1‘(𝑈‘𝐵))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
267	66, 49, 52, 93, 82	grplidd 18908	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((0g‘𝐾)(+g‘𝐾)𝐵) = 𝐵)
268	252, 266, 267	3eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0) = 𝐵)
269	250, 268	oveq12d 7408	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((coe1‘(2 ∧ 𝑌))‘0)(+g‘𝐾)((coe1‘(((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵)))‘0)) = ((0g‘𝐾)(+g‘𝐾)𝐵))
270	247, 269, 267	3eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → ((coe1‘((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))))‘0) = 𝐵)
271	243, 270	eqtrid 2777	. . . . . . . . . . 11 ⊢ (𝜑 → ((coe1‘𝐺)‘0) = 𝐵)
272	242, 271	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝜑 → ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0)) = ((𝐴 · 𝑋) + 𝐵))
273	205, 272	oveq12d 7408	. . . . . . . . 9 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)))
274		rtelextdg2.14	. . . . . . . . 9 ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 )
275	273, 274	eqtrd 2765	. . . . . . . 8 ⊢ (𝜑 → ((((coe1‘𝐺)‘2) · (2 ↑ 𝑋)) + ((((coe1‘𝐺)‘1) · 𝑋) + ((coe1‘𝐺)‘0))) = 0 )
276	180, 197, 275	3eqtrd 2769	. . . . . . 7 ⊢ (𝜑 → (((𝐸 evalSub1 𝐹)‘𝐺)‘𝑋) = 0 )
277	10, 173, 276	rspcedvdw 3594	. . . . . 6 ⊢ (𝜑 → ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )
278	174, 1, 61, 114, 36, 38	elirng 33688	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑝 ∈ (Monic1p‘𝐾)(((𝐸 evalSub1 𝐹)‘𝑝)‘𝑋) = 0 )))
279	7, 277, 278	mpbir2and 713	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹))
280	1, 2, 3, 4, 5, 6, 279	algextdeg 33722	. . . 4 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)))
281	1	fveq2i 6864	. . . . . . 7 ⊢ (Poly1‘𝐾) = (Poly1‘(𝐸 ↾s 𝐹))
282	19, 281	eqtri 2753	. . . . . 6 ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹))
283		eqid 2730	. . . . . 6 ⊢ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 } = {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝑋) = 0 }
284		eqid 2730	. . . . . 6 ⊢ (RSpan‘𝑃) = (RSpan‘𝑃)
285		eqid 2730	. . . . . 6 ⊢ (idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹))
286	174, 282, 61, 5, 6, 7, 114, 283, 284, 285, 4	minplycl 33703	. . . . 5 ⊢ (𝜑 → ((𝐸 minPoly 𝐹)‘𝑋) ∈ (Base‘𝑃))
287	1, 3, 19, 12, 286, 38	ressdeg1 33542	. . . 4 ⊢ (𝜑 → ((deg1‘𝐸)‘((𝐸 minPoly 𝐹)‘𝑋)) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
288	280, 287	eqtrd 2765	. . 3 ⊢ (𝜑 → (𝐿[:]𝐾) = ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)))
289	1	fveq2i 6864	. . . 4 ⊢ (deg1‘𝐾) = (deg1‘(𝐸 ↾s 𝐹))
290	174, 282, 61, 5, 6, 7, 114, 4, 289, 120, 12, 276, 46, 132	minplymindeg 33705	. . 3 ⊢ (𝜑 → ((deg1‘𝐾)‘((𝐸 minPoly 𝐹)‘𝑋)) ≤ ((deg1‘𝐾)‘𝐺))
291	288, 290	eqbrtrd 5132	. 2 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ ((deg1‘𝐾)‘𝐺))
292	291, 168	breqtrd 5136	1 ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∃wrex 3054  {crab 3408  Vcvv 3450   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917  ifcif 4491  {csn 4592   class class class wbr 5110   ↦ cmpt 5191  dom cdm 5641   ↾ cres 5643  ‘cfv 6514  (class class class)co 7390  0cc0 11075  1c1 11076  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216  2c2 12248  ℕ₀cn0 12449  Basecbs 17186   ↾_s cress 17207  +_gcplusg 17227  ._rcmulr 17228  0_gc0g 17409  Mndcmnd 18668  Grpcgrp 18872  ._gcmg 19006  SubGrpcsubg 19059  mulGrpcmgp 20056  1_rcur 20097  Ringcrg 20149  CRingccrg 20150  NzRingcnzr 20428  SubRingcsubrg 20485  DivRingcdr 20645  Fieldcfield 20646  SubDRingcsdrg 20702  RSpancrsp 21124  algSccascl 21768  PwSer₁cps1 22066  var₁cv1 22067  Poly₁cpl1 22068  coe₁cco1 22069   evalSub₁ ces1 22207  eval₁ce1 22208  deg₁cdg1 25966  Monic_1pcmn1 26038  idlGen_1pcig1p 26042   fldGen cfldgen 33267  [:]cextdg 33643   IntgRing cirng 33685   minPoly cminply 33696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-reg 9552  ax-inf2 9601  ax-ac2 10423  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-ofr 7657  df-rpss 7702  df-om 7846  df-1st 7971  df-2nd 7972  df-supp 8143  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-oadd 8441  df-er 8674  df-ec 8676  df-qs 8680  df-map 8804  df-pm 8805  df-ixp 8874  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fsupp 9320  df-sup 9400  df-inf 9401  df-oi 9470  df-r1 9724  df-rank 9725  df-dju 9861  df-card 9899  df-acn 9902  df-ac 10076  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12450  df-xnn0 12523  df-z 12537  df-dec 12657  df-uz 12801  df-ico 13319  df-fz 13476  df-fzo 13623  df-seq 13974  df-hash 14303  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ocomp 17248  df-ds 17249  df-unif 17250  df-hom 17251  df-cco 17252  df-0g 17411  df-gsum 17412  df-prds 17417  df-pws 17419  df-imas 17478  df-qus 17479  df-mre 17554  df-mrc 17555  df-mri 17556  df-acs 17557  df-proset 18262  df-drs 18263  df-poset 18281  df-ipo 18494  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-mhm 18717  df-submnd 18718  df-grp 18875  df-minusg 18876  df-sbg 18877  df-mulg 19007  df-subg 19062  df-nsg 19063  df-eqg 19064  df-ghm 19152  df-gim 19198  df-cntz 19256  df-oppg 19285  df-lsm 19573  df-cmn 19719  df-abl 19720  df-mgp 20057  df-rng 20069  df-ur 20098  df-srg 20103  df-ring 20151  df-cring 20152  df-oppr 20253  df-dvdsr 20273  df-unit 20274  df-irred 20275  df-invr 20304  df-dvr 20317  df-rhm 20388  df-nzr 20429  df-subrng 20462  df-subrg 20486  df-rlreg 20610  df-domn 20611  df-idom 20612  df-drng 20647  df-field 20648  df-sdrg 20703  df-lmod 20775  df-lss 20845  df-lsp 20885  df-lmhm 20936  df-lmim 20937  df-lmic 20938  df-lbs 20989  df-lvec 21017  df-sra 21087  df-rgmod 21088  df-lidl 21125  df-rsp 21126  df-2idl 21167  df-lpidl 21239  df-lpir 21240  df-pid 21254  df-cnfld 21272  df-dsmm 21648  df-frlm 21663  df-uvc 21699  df-lindf 21722  df-linds 21723  df-assa 21769  df-asp 21770  df-ascl 21771  df-psr 21825  df-mvr 21826  df-mpl 21827  df-opsr 21829  df-evls 21988  df-evl 21989  df-psr1 22071  df-vr1 22072  df-ply1 22073  df-coe1 22074  df-evls1 22209  df-evl1 22210  df-mdeg 25967  df-deg1 25968  df-mon1 26043  df-uc1p 26044  df-q1p 26045  df-r1p 26046  df-ig1p 26047  df-fldgen 33268  df-mxidl 33438  df-dim 33602  df-fldext 33644  df-extdg 33645  df-irng 33686  df-minply 33697

This theorem is referenced by:  rtelextdg2  33724