Theorem 2sqr3minply 34298

Description: The polynomial ((𝑋↑3) − 2) is the minimal polynomial for (2↑_𝑐(1 / 3)) over ℚ, and its degree is 3. (Contributed by Thierry Arnoux, 14-Jun-2025.)

Hypotheses

Ref	Expression
2sqr3minply.q	⊢ 𝑄 = (ℂfld ↾s ℚ)
2sqr3minply.1	⊢ − = (-g‘𝑃)
2sqr3minply.2	⊢ ↑ = (.g‘(mulGrp‘𝑃))
2sqr3minply.p	⊢ 𝑃 = (Poly1‘𝑄)
2sqr3minply.k	⊢ 𝐾 = (algSc‘𝑃)
2sqr3minply.x	⊢ 𝑋 = (var1‘𝑄)
2sqr3minply.d	⊢ 𝐷 = (deg1‘𝑄)
2sqr3minply.f	⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2))
2sqr3minply.a	⊢ 𝐴 = (2↑𝑐(1 / 3))
2sqr3minply.m	⊢ 𝑀 = (ℂfld minPoly ℚ)

Assertion

Ref	Expression
2sqr3minply	⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)

Proof of Theorem 2sqr3minply

Dummy variables 𝑖 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2762	. . . 4 ⊢ (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
2		2sqr3minply.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑄)
3		2sqr3minply.q	. . . . . 6 ⊢ 𝑄 = (ℂfld ↾s ℚ)
4	3	fveq2i 6885	. . . . 5 ⊢ (Poly1‘𝑄) = (Poly1‘(ℂfld ↾s ℚ))
5	2, 4	eqtri 2785	. . . 4 ⊢ 𝑃 = (Poly1‘(ℂfld ↾s ℚ))
6		cnfldbas 21595	. . . 4 ⊢ ℂ = (Base‘ℂfld)
7		cndrng 21620	. . . . . 6 ⊢ ℂfld ∈ DivRing
8		cncrng 21612	. . . . . 6 ⊢ ℂfld ∈ CRing
9		isfld 20909	. . . . . 6 ⊢ (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
10	7, 8, 9	mpbir2an 724	. . . . 5 ⊢ ℂfld ∈ Field
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂfld ∈ Field)
12		qsubdrg 21638	. . . . . . 7 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
13	12	simpli 489	. . . . . 6 ⊢ ℚ ∈ (SubRing‘ℂfld)
14	12	simpri 491	. . . . . 6 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
15		issdrg 20960	. . . . . 6 ⊢ (ℚ ∈ (SubDRing‘ℂfld) ↔ (ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing))
16	7, 13, 14, 15	mpbir3an 1360	. . . . 5 ⊢ ℚ ∈ (SubDRing‘ℂfld)
17	16	a1i 11	. . . 4 ⊢ (⊤ → ℚ ∈ (SubDRing‘ℂfld))
18		2sqr3minply.a	. . . . . 6 ⊢ 𝐴 = (2↑𝑐(1 / 3))
19		2cn 12344	. . . . . . 7 ⊢ 2 ∈ ℂ
20		3cn 12350	. . . . . . . 8 ⊢ 3 ∈ ℂ
21		3ne0 12378	. . . . . . . 8 ⊢ 3 ≠ 0
22	20, 21	reccli 11973	. . . . . . 7 ⊢ (1 / 3) ∈ ℂ
23		cxpcl 26919	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
24	19, 22, 23	mp2an 705	. . . . . 6 ⊢ (2↑𝑐(1 / 3)) ∈ ℂ
25	18, 24	eqeltri 2858	. . . . 5 ⊢ 𝐴 ∈ ℂ
26	25	a1i 11	. . . 4 ⊢ (⊤ → 𝐴 ∈ ℂ)
27		cnfld0 21615	. . . 4 ⊢ 0 = (0g‘ℂfld)
28		2sqr3minply.m	. . . 4 ⊢ 𝑀 = (ℂfld minPoly ℚ)
29		eqid 2762	. . . 4 ⊢ (0g‘𝑃) = (0g‘𝑃)
30		2sqr3minply.f	. . . . . . . 8 ⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2))
31	30	fveq2i 6885	. . . . . . 7 ⊢ ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))
32	31	fveq1i 6883	. . . . . 6 ⊢ (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴)
33	32	a1i 11	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴))
34		eqid 2762	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
35		2sqr3minply.1	. . . . . 6 ⊢ − = (-g‘𝑃)
36		cnfldsub 21619	. . . . . 6 ⊢ − = (-g‘ℂfld)
37	8	a1i 11	. . . . . 6 ⊢ (⊤ → ℂfld ∈ CRing)
38	13	a1i 11	. . . . . 6 ⊢ (⊤ → ℚ ∈ (SubRing‘ℂfld))
39		eqid 2762	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
40	39, 34	mgpbas 20284	. . . . . . 7 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41		2sqr3minply.2	. . . . . . 7 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
42	3	qdrng 27864	. . . . . . . . . . 11 ⊢ 𝑄 ∈ DivRing
43	42	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝑄 ∈ DivRing)
44	43	drngringd 20904	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ Ring)
45	2	ply1ring 22478	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring)
46	44, 45	syl 18	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ Ring)
47	39	ringmgp 20384	. . . . . . . 8 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
48	46, 47	syl 18	. . . . . . 7 ⊢ (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49		3nn0 12550	. . . . . . . 8 ⊢ 3 ∈ ℕ0
50	49	a1i 11	. . . . . . 7 ⊢ (⊤ → 3 ∈ ℕ0)
51		2sqr3minply.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑄)
52	51, 2, 34	vr1cl 22448	. . . . . . . 8 ⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
53	44, 52	syl 18	. . . . . . 7 ⊢ (⊤ → 𝑋 ∈ (Base‘𝑃))
54	40, 41, 48, 50, 53	mulgnn0cld 19224	. . . . . 6 ⊢ (⊤ → (3 ↑ 𝑋) ∈ (Base‘𝑃))
55		2sqr3minply.k	. . . . . . . 8 ⊢ 𝐾 = (algSc‘𝑃)
56	44	mptru 1577	. . . . . . . . 9 ⊢ 𝑄 ∈ Ring
57	2	ply1sca 22483	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
58	56, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑄 = (Scalar‘𝑃)
59	2	ply1lmod 22482	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod)
60	44, 59	syl 18	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ LMod)
61	3	qrngbas 27863	. . . . . . . 8 ⊢ ℚ = (Base‘𝑄)
62	55, 58, 46, 60, 61, 34	asclf 22102	. . . . . . 7 ⊢ (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63		2z 12654	. . . . . . . 8 ⊢ 2 ∈ ℤ
64		zq 13007	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
65	63, 64	mp1i 14	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℚ)
66	62, 65	ffvelcdmd 7082	. . . . . 6 ⊢ (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
67	1, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26	evls1subd 33990	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴) = ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)))
68		eqid 2762	. . . . . . . . . 10 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
69	1, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26	evls1expd 22598	. . . . . . . . 9 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
70	1, 51, 3, 6, 37, 38	evls1var 22569	. . . . . . . . . . . 12 ⊢ (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
71	70	fveq1d 6884	. . . . . . . . . . 11 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72		fvresi 7175	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
73	25, 72	mp1i 14	. . . . . . . . . . 11 ⊢ (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
74	71, 73	eqtrd 2797	. . . . . . . . . 10 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
75	74	oveq2d 7433	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76		cnfldexp 21624	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
77	26, 50, 76	syl2anc 596	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
78	69, 75, 77	3eqtrd 2801	. . . . . . . 8 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (𝐴↑3))
79	18	oveq1i 7427	. . . . . . . . 9 ⊢ (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80		3nn 12348	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
81		cxproot 26935	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
82	19, 80, 81	mp2an 705	. . . . . . . . 9 ⊢ ((2↑𝑐(1 / 3))↑3) = 2
83	79, 82	eqtri 2785	. . . . . . . 8 ⊢ (𝐴↑3) = 2
84	78, 83	eqtrdi 2813	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = 2)
85	1, 2, 3, 6, 55, 37, 38, 65, 26	evls1scafv 22597	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
86	84, 85	oveq12d 7435	. . . . . 6 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
87	19	subidi 11557	. . . . . 6 ⊢ (2 − 2) = 0
88	86, 87	eqtrdi 2813	. . . . 5 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0)
89	33, 67, 88	3eqtrd 2801	. . . 4 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0)
90	3	qrng0 27865	. . . . 5 ⊢ 0 = (0g‘𝑄)
91		eqid 2762	. . . . 5 ⊢ (eval1‘𝑄) = (eval1‘𝑄)
92		2sqr3minply.d	. . . . 5 ⊢ 𝐷 = (deg1‘𝑄)
93		fldsdrgfld 20970	. . . . . . . 8 ⊢ ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂfld ↾s ℚ) ∈ Field)
94	10, 16, 93	mp2an 705	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) ∈ Field
95	3, 94	eqeltri 2858	. . . . . 6 ⊢ 𝑄 ∈ Field
96	95	a1i 11	. . . . 5 ⊢ (⊤ → 𝑄 ∈ Field)
97	46	ringgrpd 20387	. . . . . . 7 ⊢ (⊤ → 𝑃 ∈ Grp)
98	34, 35	grpsubcl 19149	. . . . . . 7 ⊢ ((𝑃 ∈ Grp ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
99	97, 54, 66, 98	syl3anc 1398	. . . . . 6 ⊢ (⊤ → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
100	30, 99	eqeltrid 2866	. . . . 5 ⊢ (⊤ → 𝐹 ∈ (Base‘𝑃))
101	96	fldcrngd 20911	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ CRing)
102	91, 2, 34, 101, 61, 100	evl1fvf 33981	. . . . . . . 8 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹):ℚ⟶ℚ)
103	102	ffnd 6707	. . . . . . 7 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹) Fn ℚ)
104		fniniseg2 7058	. . . . . . 7 ⊢ (((eval1‘𝑄)‘𝐹) Fn ℚ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
105	103, 104	syl 18	. . . . . 6 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
106		cnfldmul 21599	. . . . . . . . . . . . . . 15 ⊢ · = (.r‘ℂfld)
107	3, 106	ressmulr 17398	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → · = (.r‘𝑄))
108	13, 107	ax-mp 5	. . . . . . . . . . . . 13 ⊢ · = (.r‘𝑄)
109		cnfldadd 21597	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘ℂfld)
110	3, 109	ressplusg 17382	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → + = (+g‘𝑄))
111	13, 110	ax-mp 5	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑄)
112		eqid 2762	. . . . . . . . . . . . 13 ⊢ (.g‘(mulGrp‘𝑄)) = (.g‘(mulGrp‘𝑄))
113		eqid 2762	. . . . . . . . . . . . 13 ⊢ (coe1‘𝐹) = (coe1‘𝐹)
114	30	fveq2i 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2)))
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2))))
116	30	fveq2i 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2)))
117	116	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))))
118		3pos 12377	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 3
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 < 3)
120		2ne0 12375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 2 ≠ 0)
122	92, 2, 61, 55, 90	deg1scl 26345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
123	44, 65, 121, 122	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(𝐾‘2)) = 0)
124		drngnzr 20917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
125	42, 124	mp1i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 𝑄 ∈ NzRing)
126	92, 2, 51, 39, 41	deg1pw 26353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 ↑ 𝑋)) = 3)
127	125, 50, 126	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(3 ↑ 𝑋)) = 3)
128	119, 123, 127	3brtr4d 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 ↑ 𝑋)))
129	2, 92, 44, 34, 35, 54, 66, 128	deg1sub 26340	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) = (𝐷‘(3 ↑ 𝑋)))
130	117, 129, 127	3eqtrd 2801	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝐷‘𝐹) = 3)
131	115, 130	fveq12d 6889	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3))
132		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (-g‘𝑄) = (-g‘𝑄)
133	2, 34, 35, 132	coe1subfv 22498	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 3 ∈ ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
134	44, 54, 66, 50, 133	syl31anc 1400	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
135		subrgsubg 20745	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℚ ∈ (SubRing‘ℂfld) → ℚ ∈ (SubGrp‘ℂfld))
136	13, 135	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ℚ ∈ (SubGrp‘ℂfld))
137		eqid 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(3 ↑ 𝑋)) = (coe1‘(3 ↑ 𝑋))
138	137, 34, 2, 61	coe1fvalcl 22443	. . . . . . . . . . . . . . . . . . 19 ⊢ (((3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
139	54, 50, 138	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
140		eqid 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141	140, 34, 2, 61	coe1fvalcl 22443	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
142	66, 50, 141	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
143	36, 3, 132	subgsub 19268	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ ∧ ((coe1‘(𝐾‘2))‘3) ∈ ℚ) → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
144	136, 139, 142, 143	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
145		iftrue 4491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
146	3	qrng1 27866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 = (1r‘𝑄)
147	2, 51, 41, 44, 50, 90, 146	coe1mon 34005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(3 ↑ 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148		1cnd 11230	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 1 ∈ ℂ)
149	145, 147, 50, 148	fvmptd4 7015	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) = 1)
150	21	neii 2959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 3 = 0
151		eqeq1 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152	150, 151	mtbiri 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 3 → ¬ 𝑖 = 0)
153	152	iffalsed 4496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
154	2, 55, 61, 90	coe1scl 22519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
155	44, 65, 154	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156		0nn0 12547	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℕ0
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 ∈ ℕ0)
158	153, 155, 50, 157	fvmptd4 7015	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159	149, 158	oveq12d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160		1m0e1 12388	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
161	159, 160	eqtrdi 2813	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = 1)
162	144, 161	eqtr3d 2799	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)) = 1)
163	131, 134, 162	3eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1)
164	130	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘3))
165	163, 164	eqtr3d 2799	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 = ((coe1‘𝐹)‘3))
166	165	mptru 1577	. . . . . . . . . . . . 13 ⊢ 1 = ((coe1‘𝐹)‘3)
167	115	fveq1d 6884	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘2) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2))
168		2nn0 12549	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
169	168	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 2 ∈ ℕ0)
170	2, 34, 35, 132	coe1subfv 22498	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 2 ∈ ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)))
171	44, 54, 66, 169, 170	syl31anc 1400	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)))
172		2re 12343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
173		2lt3 12442	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < 3
174	172, 173	ltneii 11351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 3
175		neeq1 3019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176	174, 175	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 3)
177	176	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178	177	neneqd 2962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179	178	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180	147, 179, 169, 157	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘2) = 0)
181		neeq1 3019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182	120, 181	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 0)
183	182	neneqd 2962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 0)
184	183	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185	184	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186	155, 185, 169, 157	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187	180, 186	oveq12d 7435	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)) = (0(-g‘𝑄)0))
188	171, 187	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (0(-g‘𝑄)0))
189	158, 142	eqeltrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 0 ∈ ℚ)
190	36, 3, 132	subgsub 19268	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ) → (0 − 0) = (0(-g‘𝑄)0))
191	136, 189, 189, 190	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 0) = (0(-g‘𝑄)0))
192		0m0e0 12387	. . . . . . . . . . . . . . . 16 ⊢ (0 − 0) = 0
193	191, 192	eqtr3di 2812	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)0) = 0)
194	167, 188, 193	3eqtrrd 2802	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘2))
195	194	mptru 1577	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘2)
196	115	fveq1d 6884	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘1) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1))
197		1nn0 12548	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
198	197	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 1 ∈ ℕ0)
199	2, 34, 35, 132	coe1subfv 22498	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 1 ∈ ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)))
200	44, 54, 66, 198, 199	syl31anc 1400	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)))
201		1re 11236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
202		1lt3 12444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 3
203	201, 202	ltneii 11351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 3
204		neeq1 3019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205	203, 204	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 3)
206	205	neneqd 2962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 3)
207	206	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208	207	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209	147, 208, 198, 157	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘1) = 0)
210		ax-1ne0 11197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
211		neeq1 3019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212	210, 211	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 0)
213	212	neneqd 2962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
214	213	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215	214	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216	155, 215, 198, 157	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217	209, 216	oveq12d 7435	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)) = (0(-g‘𝑄)0))
218	200, 217	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (0(-g‘𝑄)0))
219	196, 218, 193	3eqtrrd 2802	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘1))
220	219	mptru 1577	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘1)
221	115	fveq1d 6884	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘0) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0))
222	2, 34, 35, 132	coe1subfv 22498	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄 ∈ Ring ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) ∧ 0 ∈ ℕ0) → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)))
223	44, 54, 66, 157, 222	syl31anc 1400	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)))
224	21	necomi 3011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 3
225		neeq1 3019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226	224, 225	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → 𝑖 ≠ 3)
227	226	neneqd 2962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 0 → ¬ 𝑖 = 3)
228	227	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229	228	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230	147, 229, 157, 157	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘0) = 0)
231		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232	231	iftrued 4493	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233	155, 232, 157, 169	fvmptd 6998	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234	230, 233	oveq12d 7435	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)) = (0(-g‘𝑄)2))
235	223, 234	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (0(-g‘𝑄)2))
236		df-neg 11472	. . . . . . . . . . . . . . . 16 ⊢ -2 = (0 − 2)
237	36, 3, 132	subgsub 19268	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ) → (0 − 2) = (0(-g‘𝑄)2))
238	136, 189, 65, 237	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 2) = (0(-g‘𝑄)2))
239	236, 238	eqtr2id 2810	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)2) = -2)
240	221, 235, 239	3eqtrrd 2802	. . . . . . . . . . . . . 14 ⊢ (⊤ → -2 = ((coe1‘𝐹)‘0))
241	240	mptru 1577	. . . . . . . . . . . . 13 ⊢ -2 = ((coe1‘𝐹)‘0)
242	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ Field)
243	242	fldcrngd 20911	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ CRing)
244	100	mptru 1577	. . . . . . . . . . . . . 14 ⊢ 𝐹 ∈ (Base‘𝑃)
245	244	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝐹 ∈ (Base‘𝑃))
246	130	mptru 1577	. . . . . . . . . . . . . 14 ⊢ (𝐷‘𝐹) = 3
247	246	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → (𝐷‘𝐹) = 3)
248		id 23	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℚ)
249	2, 91, 61, 34, 108, 111, 112, 113, 92, 166, 195, 220, 241, 243, 245, 247, 248	evl1deg3 33996	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250		qsscn 13013	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ ℂ
251		eqid 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253	252, 6	mgpbas 20284	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ = (Base‘(mulGrp‘ℂfld))
254	251, 253	ressbas2 17336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255	250, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
256	3, 252	mgpress 20289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld)) → ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄))
257	7, 13, 256	mp2an 705	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄)
258	257	fveq2i 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘((mulGrp‘ℂfld) ↾s ℚ)) = (Base‘(mulGrp‘𝑄))
259	255, 258	eqtri 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
260		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
261	260	ringmgp 20384	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
262	56, 261	mp1i 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (mulGrp‘𝑄) ∈ Mnd)
263	49	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ0)
264	259, 112, 262, 263, 248	mulgnn0cld 19224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265	250, 264	sselid 3932	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266	265	mullidd 11255	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267	257	eqcomi 2771	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268	250, 253	sseqtri 3982	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269	268	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
270	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ)
271	267, 269, 248, 270	ressmulgnnd 19207	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272		qcn 13016	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273		cnfldexp 21624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274	272, 263, 273	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275	266, 271, 274	3eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276	168	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277	259, 112, 262, 276, 248	mulgnn0cld 19224	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278	250, 277	sselid 3932	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279	278	mul02d 11436	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280	275, 279	oveq12d 7435	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281	272, 263	expcld 14214	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282	281	addridd 11438	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283	280, 282	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284	272	mul02d 11436	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285	284	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
286	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℂ)
287	286	negcld 11584	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → -2 ∈ ℂ)
288	287	addlidd 11439	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → (0 + -2) = -2)
289	285, 288	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290	283, 289	oveq12d 7435	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291	281, 286	negsubd 11603	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292	249, 290, 291	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293		2prm 16788	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℙ
294		3z 12655	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
295		3re 12349	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℝ
296	172, 295, 173	ltleii 11361	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 3
297	63	eluz1i 12899	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ (ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298	294, 296, 297	mpbir2an 724	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ (ℤ≥‘2)
299		rtprmirr 27005	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℙ ∧ 3 ∈ (ℤ≥‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300	293, 298, 299	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301		eldifn 4082	. . . . . . . . . . . . . 14 ⊢ ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302	300, 301	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303		nelne2 3055	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304	302, 303	mpan2 704	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305		qre 13006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306	305	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307		2pos 12373	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
308	281, 286	subeq0ad 11605	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309	308	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310	307, 309	breqtrrid 5147	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
311	80	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312		n2dvds3 16467	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 2 ∥ 3
313	312	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314	306, 311, 313	expgt0b 33295	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315	310, 314	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < 𝑥)
316	306, 315	elrpd 13087	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ+)
317	295	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℝ)
318	22	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (1 / 3) ∈ ℂ)
319	316, 317, 318	cxpmuld 26982	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑𝑐(3 · (1 / 3))) = ((𝑥↑𝑐3)↑𝑐(1 / 3)))
320	20	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℂ)
321	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 3 ≠ 0)
322	320, 321	recidd 12014	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323	322	oveq2d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = (𝑥↑𝑐1))
324	272	cxp1d 26951	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐1) = 𝑥)
325	323, 324	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
326	325	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
327		cxpexp 26913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥↑𝑐3) = (𝑥↑3))
328	272, 263, 327	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐3) = (𝑥↑3))
329	328	oveq1d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330	329	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331	319, 326, 330	3eqtr3rd 2806	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332	309	oveq1d 7432	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)))
333	331, 332	eqtr3d 2799	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 = (2↑𝑐(1 / 3)))
334	304, 333	mteqand 3048	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335	292, 334	eqnetrd 3024	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) ≠ 0)
336	335	neneqd 2962	. . . . . . . . 9 ⊢ (𝑥 ∈ ℚ → ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
337	336	rgen 3080	. . . . . . . 8 ⊢ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0
338	337	a1i 11	. . . . . . 7 ⊢ (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
339		rabeq0 4341	. . . . . . 7 ⊢ ({𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
340	338, 339	sylibr 237	. . . . . 6 ⊢ (⊤ → {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341	105, 340	eqtrd 2797	. . . . 5 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = ∅)
342	90, 91, 92, 2, 34, 96, 100, 341, 130	ply1dg3rt0irred 34002	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Irred‘𝑃))
343		eqid 2762	. . . . . . 7 ⊢ (Irred‘𝑃) = (Irred‘𝑃)
344	343, 29	irredn0 20570	. . . . . 6 ⊢ ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g‘𝑃))
345	46, 342, 344	syl2anc 596	. . . . 5 ⊢ (⊤ → 𝐹 ≠ (0g‘𝑃))
346	3	fveq2i 6885	. . . . . . 7 ⊢ (deg1‘𝑄) = (deg1‘(ℂfld ↾s ℚ))
347	92, 346	eqtri 2785	. . . . . 6 ⊢ 𝐷 = (deg1‘(ℂfld ↾s ℚ))
348		eqid 2762	. . . . . 6 ⊢ (Monic1p‘(ℂfld ↾s ℚ)) = (Monic1p‘(ℂfld ↾s ℚ))
349		eqid 2762	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
350	349	qrng1 27866	. . . . . 6 ⊢ 1 = (1r‘(ℂfld ↾s ℚ))
351	5, 34, 29, 347, 348, 350	ismon1p 26375	. . . . 5 ⊢ (𝐹 ∈ (Monic1p‘(ℂfld ↾s ℚ)) ↔ (𝐹 ∈ (Base‘𝑃) ∧ 𝐹 ≠ (0g‘𝑃) ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1))
352	100, 345, 163, 351	syl3anbrc 1362	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Monic1p‘(ℂfld ↾s ℚ)))
353	1, 5, 6, 11, 17, 26, 27, 28, 29, 89, 342, 352	irredminply 34234	. . 3 ⊢ (⊤ → 𝐹 = (𝑀‘𝐴))
354	353, 130	jca 521	. 2 ⊢ (⊤ → (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3))
355	354	mptru 1577	1 ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  {crab 3414   ∖ cdif 3899   ⊆ wss 3902  ∅c0 4282  ifcif 4485  {csn 4587   class class class wbr 5107   ↦ cmpt 5190   I cid 5553  ^◡ccnv 5658   ↾ cres 5661   “ cima 5662   Fn wfn 6532  ‘cfv 6537  (class class class)co 7417  ℂcc 11126  ℝcr 11127  0cc0 11128  1c1 11129   + caddc 11131   · cmul 11133   < clt 11271   ≤ cle 11272   − cmin 11469  -cneg 11470   / cdiv 11899  ℕcn 12261  2c2 12323  3c3 12324  ℕ₀cn0 12532  ℤcz 12619  ℤ_≥cuz 12891  ℚcq 13001  ↑cexp 14129   ∥ cdvds 16348  ℙcprime 16767  Basecbs 17307   ↾_s cress 17328  +_gcplusg 17348  ._rcmulr 17349  Scalarcsca 17351  0_gc0g 17530  Mndcmnd 18842  Grpcgrp 19063  -_gcsg 19065  ._gcmg 19196  SubGrpcsubg 19249  mulGrpcmgp 20279  Ringcrg 20378  CRingccrg 20379  Irredcir 20503  NzRingcnzr 20678  SubRingcsubrg 20737  DivRingcdr 20896  Fieldcfield 20897  SubDRingcsdrg 20958  LModclmod 21050  ℂ_fldccnfld 21591  algSccascl 22073  var₁cv1 22407  Poly₁cpl1 22408  coe₁cco1 22409   evalSub₁ ces1 22544  eval₁ce1 22545  deg₁cdg1 26286  Monic_1pcmn1 26358  ↑_𝑐ccxp 26800   minPoly cminply 34217

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 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-inf2 9624  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-pre-sup 11206  ax-addf 11207  ax-mulf 11208

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-of 7682  df-ofr 7683  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8163  df-tpos 8228  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-pm 8833  df-ixp 8909  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-fsupp 9336  df-fi 9385  df-sup 9416  df-inf 9417  df-oi 9486  df-card 9948  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900  df-nn 12262  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336  df-8 12337  df-9 12338  df-n0 12533  df-z 12620  df-dec 12741  df-uz 12892  df-q 13002  df-rp 13047  df-xneg 13167  df-xadd 13168  df-xmul 13169  df-ioo 13406  df-ioc 13407  df-ico 13408  df-icc 13409  df-fz 13566  df-fzo 13714  df-fl 13857  df-mod 13935  df-seq 14070  df-exp 14130  df-fac 14342  df-bc 14371  df-hash 14399  df-shft 15144  df-cj 15190  df-re 15191  df-im 15192  df-sqrt 15326  df-abs 15327  df-limsup 15562  df-clim 15579  df-rlim 15580  df-sum 15778  df-ef 16159  df-sin 16161  df-cos 16162  df-pi 16164  df-dvds 16349  df-gcd 16591  df-prm 16768  df-numer 16832  df-denom 16833  df-struct 17245  df-sets 17262  df-slot 17280  df-ndx 17292  df-base 17308  df-ress 17329  df-plusg 17361  df-mulr 17362  df-starv 17363  df-sca 17364  df-vsca 17365  df-ip 17366  df-tset 17367  df-ple 17368  df-ds 17370  df-unif 17371  df-hom 17372  df-cco 17373  df-rest 17513  df-topn 17514  df-0g 17532  df-gsum 17533  df-topgen 17534  df-pt 17535  df-prds 17538  df-pws 17540  df-xrs 17594  df-qtop 17599  df-imas 17600  df-xps 17602  df-mre 17676  df-mrc 17677  df-acs 17679  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-mhm 18897  df-submnd 18898  df-grp 19066  df-minusg 19067  df-sbg 19068  df-mulg 19197  df-subg 19252  df-ghm 19347  df-cntz 19450  df-cmn 19915  df-abl 19916  df-mgp 20280  df-rng 20294  df-ur 20327  df-srg 20332  df-ring 20380  df-cring 20381  df-oppr 20484  df-dvdsr 20504  df-unit 20505  df-irred 20506  df-invr 20535  df-dvr 20548  df-rhm 20619  df-nzr 20679  df-subrng 20714  df-subrg 20738  df-rlreg 20862  df-domn 20863  df-idom 20864  df-drng 20898  df-field 20899  df-sdrg 20959  df-lmod 21052  df-lss 21122  df-lsp 21162  df-sra 21363  df-rgmod 21364  df-lidl 21401  df-rsp 21402  df-psmet 21583  df-xmet 21584  df-met 21585  df-bl 21586  df-mopn 21587  df-fbas 21588  df-fg 21589  df-cnfld 21592  df-assa 22074  df-asp 22075  df-ascl 22076  df-psr 22130  df-mvr 22131  df-mpl 22132  df-opsr 22134  df-evls 22296  df-evl 22297  df-psr1 22411  df-vr1 22412  df-ply1 22413  df-coe1 22414  df-evls1 22546  df-evl1 22547  df-top 23125  df-topon 23142  df-topsp 23164  df-bases 23177  df-cld 23250  df-ntr 23251  df-cls 23252  df-nei 23329  df-lp 23367  df-perf 23368  df-cn 23458  df-cnp 23459  df-haus 23546  df-tx 23794  df-hmeo 23987  df-fil 24078  df-fm 24170  df-flim 24171  df-flf 24172  df-xms 24552  df-ms 24553  df-tms 24554  df-cncf 25112  df-limc 26100  df-dv 26101  df-mdeg 26287  df-deg1 26288  df-mon1 26363  df-uc1p 26364  df-q1p 26365  df-r1p 26366  df-ig1p 26367  df-log 26801  df-cxp 26802  df-irng 34202  df-minply 34218

This theorem is used by:  2sqr3nconstr  34299