Theorem 2sqr3minply 34179

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 2763	. . . 4 ⊢ (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
2		2sqr3minply.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑄)
3		2sqr3minply.q	. . . . . 6 ⊢ 𝑄 = (ℂfld ↾s ℚ)
4	3	fveq2i 6884	. . . . 5 ⊢ (Poly1‘𝑄) = (Poly1‘(ℂfld ↾s ℚ))
5	2, 4	eqtri 2786	. . . 4 ⊢ 𝑃 = (Poly1‘(ℂfld ↾s ℚ))
6		cnfldbas 21535	. . . 4 ⊢ ℂ = (Base‘ℂfld)
7		cndrng 21560	. . . . . 6 ⊢ ℂfld ∈ DivRing
8		cncrng 21552	. . . . . 6 ⊢ ℂfld ∈ CRing
9		isfld 20849	. . . . . 6 ⊢ (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
10	7, 8, 9	mpbir2an 723	. . . . 5 ⊢ ℂfld ∈ Field
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂfld ∈ Field)
12		qsubdrg 21578	. . . . . . 7 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
13	12	simpli 488	. . . . . 6 ⊢ ℚ ∈ (SubRing‘ℂfld)
14	12	simpri 490	. . . . . 6 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
15		issdrg 20900	. . . . . 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 12320	. . . . . . 7 ⊢ 2 ∈ ℂ
20		3cn 12326	. . . . . . . 8 ⊢ 3 ∈ ℂ
21		3ne0 12354	. . . . . . . 8 ⊢ 3 ≠ 0
22	20, 21	reccli 11949	. . . . . . 7 ⊢ (1 / 3) ∈ ℂ
23		cxpcl 26848	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
24	19, 22, 23	mp2an 704	. . . . . 6 ⊢ (2↑𝑐(1 / 3)) ∈ ℂ
25	18, 24	eqeltri 2859	. . . . 5 ⊢ 𝐴 ∈ ℂ
26	25	a1i 11	. . . 4 ⊢ (⊤ → 𝐴 ∈ ℂ)
27		cnfld0 21555	. . . 4 ⊢ 0 = (0g‘ℂfld)
28		2sqr3minply.m	. . . 4 ⊢ 𝑀 = (ℂfld minPoly ℚ)
29		eqid 2763	. . . 4 ⊢ (0g‘𝑃) = (0g‘𝑃)
30		2sqr3minply.f	. . . . . . . 8 ⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2))
31	30	fveq2i 6884	. . . . . . 7 ⊢ ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))
32	31	fveq1i 6882	. . . . . 6 ⊢ (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴)
33	32	a1i 11	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴))
34		eqid 2763	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
35		2sqr3minply.1	. . . . . 6 ⊢ − = (-g‘𝑃)
36		cnfldsub 21559	. . . . . 6 ⊢ − = (-g‘ℂfld)
37	8	a1i 11	. . . . . 6 ⊢ (⊤ → ℂfld ∈ CRing)
38	13	a1i 11	. . . . . 6 ⊢ (⊤ → ℚ ∈ (SubRing‘ℂfld))
39		eqid 2763	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
40	39, 34	mgpbas 20225	. . . . . . 7 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41		2sqr3minply.2	. . . . . . 7 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
42	3	qdrng 27793	. . . . . . . . . . 11 ⊢ 𝑄 ∈ DivRing
43	42	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝑄 ∈ DivRing)
44	43	drngringd 20844	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ Ring)
45	2	ply1ring 22416	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring)
46	44, 45	syl 18	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ Ring)
47	39	ringmgp 20325	. . . . . . . 8 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
48	46, 47	syl 18	. . . . . . 7 ⊢ (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49		3nn0 12526	. . . . . . . 8 ⊢ 3 ∈ ℕ0
50	49	a1i 11	. . . . . . 7 ⊢ (⊤ → 3 ∈ ℕ0)
51		2sqr3minply.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑄)
52	51, 2, 34	vr1cl 22386	. . . . . . . 8 ⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
53	44, 52	syl 18	. . . . . . 7 ⊢ (⊤ → 𝑋 ∈ (Base‘𝑃))
54	40, 41, 48, 50, 53	mulgnn0cld 19165	. . . . . 6 ⊢ (⊤ → (3 ↑ 𝑋) ∈ (Base‘𝑃))
55		2sqr3minply.k	. . . . . . . 8 ⊢ 𝐾 = (algSc‘𝑃)
56	44	mptru 1577	. . . . . . . . 9 ⊢ 𝑄 ∈ Ring
57	2	ply1sca 22421	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
58	56, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑄 = (Scalar‘𝑃)
59	2	ply1lmod 22420	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod)
60	44, 59	syl 18	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ LMod)
61	3	qrngbas 27792	. . . . . . . 8 ⊢ ℚ = (Base‘𝑄)
62	55, 58, 46, 60, 61, 34	asclf 22040	. . . . . . 7 ⊢ (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63		2z 12630	. . . . . . . 8 ⊢ 2 ∈ ℤ
64		zq 12982	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
65	63, 64	mp1i 14	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℚ)
66	62, 65	ffvelcdmd 7080	. . . . . 6 ⊢ (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
67	1, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26	evls1subd 33871	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴) = ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)))
68		eqid 2763	. . . . . . . . . 10 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
69	1, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26	evls1expd 22536	. . . . . . . . 9 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
70	1, 51, 3, 6, 37, 38	evls1var 22507	. . . . . . . . . . . 12 ⊢ (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
71	70	fveq1d 6883	. . . . . . . . . . 11 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72		fvresi 7171	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
73	25, 72	mp1i 14	. . . . . . . . . . 11 ⊢ (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
74	71, 73	eqtrd 2798	. . . . . . . . . 10 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
75	74	oveq2d 7426	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76		cnfldexp 21564	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
77	26, 50, 76	syl2anc 595	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
78	69, 75, 77	3eqtrd 2802	. . . . . . . 8 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (𝐴↑3))
79	18	oveq1i 7420	. . . . . . . . 9 ⊢ (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80		3nn 12324	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
81		cxproot 26864	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
82	19, 80, 81	mp2an 704	. . . . . . . . 9 ⊢ ((2↑𝑐(1 / 3))↑3) = 2
83	79, 82	eqtri 2786	. . . . . . . 8 ⊢ (𝐴↑3) = 2
84	78, 83	eqtrdi 2814	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = 2)
85	1, 2, 3, 6, 55, 37, 38, 65, 26	evls1scafv 22535	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
86	84, 85	oveq12d 7428	. . . . . 6 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
87	19	subidi 11533	. . . . . 6 ⊢ (2 − 2) = 0
88	86, 87	eqtrdi 2814	. . . . 5 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0)
89	33, 67, 88	3eqtrd 2802	. . . 4 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0)
90	3	qrng0 27794	. . . . 5 ⊢ 0 = (0g‘𝑄)
91		eqid 2763	. . . . 5 ⊢ (eval1‘𝑄) = (eval1‘𝑄)
92		2sqr3minply.d	. . . . 5 ⊢ 𝐷 = (deg1‘𝑄)
93		fldsdrgfld 20910	. . . . . . . 8 ⊢ ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂfld ↾s ℚ) ∈ Field)
94	10, 16, 93	mp2an 704	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) ∈ Field
95	3, 94	eqeltri 2859	. . . . . 6 ⊢ 𝑄 ∈ Field
96	95	a1i 11	. . . . 5 ⊢ (⊤ → 𝑄 ∈ Field)
97	46	ringgrpd 20328	. . . . . . 7 ⊢ (⊤ → 𝑃 ∈ Grp)
98	34, 35	grpsubcl 19090	. . . . . . 7 ⊢ ((𝑃 ∈ Grp ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
99	97, 54, 66, 98	syl3anc 1398	. . . . . 6 ⊢ (⊤ → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
100	30, 99	eqeltrid 2867	. . . . 5 ⊢ (⊤ → 𝐹 ∈ (Base‘𝑃))
101	96	fldcrngd 20851	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ CRing)
102	91, 2, 34, 101, 61, 100	evl1fvf 33862	. . . . . . . 8 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹):ℚ⟶ℚ)
103	102	ffnd 6706	. . . . . . 7 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹) Fn ℚ)
104		fniniseg2 7057	. . . . . . 7 ⊢ (((eval1‘𝑄)‘𝐹) Fn ℚ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
105	103, 104	syl 18	. . . . . 6 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
106		cnfldmul 21539	. . . . . . . . . . . . . . 15 ⊢ · = (.r‘ℂfld)
107	3, 106	ressmulr 17364	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → · = (.r‘𝑄))
108	13, 107	ax-mp 5	. . . . . . . . . . . . 13 ⊢ · = (.r‘𝑄)
109		cnfldadd 21537	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘ℂfld)
110	3, 109	ressplusg 17348	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → + = (+g‘𝑄))
111	13, 110	ax-mp 5	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑄)
112		eqid 2763	. . . . . . . . . . . . 13 ⊢ (.g‘(mulGrp‘𝑄)) = (.g‘(mulGrp‘𝑄))
113		eqid 2763	. . . . . . . . . . . . 13 ⊢ (coe1‘𝐹) = (coe1‘𝐹)
114	30	fveq2i 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2)))
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2))))
116	30	fveq2i 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2)))
117	116	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))))
118		3pos 12353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 3
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 < 3)
120		2ne0 12351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 2 ≠ 0)
122	92, 2, 61, 55, 90	deg1scl 26279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
123	44, 65, 121, 122	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(𝐾‘2)) = 0)
124		drngnzr 20857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
125	42, 124	mp1i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 𝑄 ∈ NzRing)
126	92, 2, 51, 39, 41	deg1pw 26287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 ↑ 𝑋)) = 3)
127	125, 50, 126	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(3 ↑ 𝑋)) = 3)
128	119, 123, 127	3brtr4d 5143	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 ↑ 𝑋)))
129	2, 92, 44, 34, 35, 54, 66, 128	deg1sub 26274	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) = (𝐷‘(3 ↑ 𝑋)))
130	117, 129, 127	3eqtrd 2802	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝐷‘𝐹) = 3)
131	115, 130	fveq12d 6888	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3))
132		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (-g‘𝑄) = (-g‘𝑄)
133	2, 34, 35, 132	coe1subfv 22436	. . . . . . . . . . . . . . . . 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 20685	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℚ ∈ (SubRing‘ℂfld) → ℚ ∈ (SubGrp‘ℂfld))
136	13, 135	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ℚ ∈ (SubGrp‘ℂfld))
137		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(3 ↑ 𝑋)) = (coe1‘(3 ↑ 𝑋))
138	137, 34, 2, 61	coe1fvalcl 22381	. . . . . . . . . . . . . . . . . . 19 ⊢ (((3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
139	54, 50, 138	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
140		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141	140, 34, 2, 61	coe1fvalcl 22381	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
142	66, 50, 141	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
143	36, 3, 132	subgsub 19209	. . . . . . . . . . . . . . . . . 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 4493	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
146	3	qrng1 27795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 = (1r‘𝑄)
147	2, 51, 41, 44, 50, 90, 146	coe1mon 33886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(3 ↑ 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148		1cnd 11206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 1 ∈ ℂ)
149	145, 147, 50, 148	fvmptd4 7014	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) = 1)
150	21	neii 2960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 3 = 0
151		eqeq1 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152	150, 151	mtbiri 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 3 → ¬ 𝑖 = 0)
153	152	iffalsed 4498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
154	2, 55, 61, 90	coe1scl 22457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
155	44, 65, 154	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156		0nn0 12523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℕ0
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 ∈ ℕ0)
158	153, 155, 50, 157	fvmptd4 7014	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159	149, 158	oveq12d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160		1m0e1 12364	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
161	159, 160	eqtrdi 2814	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = 1)
162	144, 161	eqtr3d 2800	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)) = 1)
163	131, 134, 162	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1)
164	130	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘3))
165	163, 164	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 = ((coe1‘𝐹)‘3))
166	165	mptru 1577	. . . . . . . . . . . . 13 ⊢ 1 = ((coe1‘𝐹)‘3)
167	115	fveq1d 6883	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘2) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2))
168		2nn0 12525	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
169	168	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 2 ∈ ℕ0)
170	2, 34, 35, 132	coe1subfv 22436	. . . . . . . . . . . . . . . . 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 12319	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
173		2lt3 12418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < 3
174	172, 173	ltneii 11327	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 3
175		neeq1 3020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176	174, 175	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 3)
177	176	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178	177	neneqd 2963	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179	178	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180	147, 179, 169, 157	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘2) = 0)
181		neeq1 3020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182	120, 181	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 0)
183	182	neneqd 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 0)
184	183	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185	184	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186	155, 185, 169, 157	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187	180, 186	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)) = (0(-g‘𝑄)0))
188	171, 187	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (0(-g‘𝑄)0))
189	158, 142	eqeltrrd 2864	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 0 ∈ ℚ)
190	36, 3, 132	subgsub 19209	. . . . . . . . . . . . . . . . 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 12363	. . . . . . . . . . . . . . . 16 ⊢ (0 − 0) = 0
193	191, 192	eqtr3di 2813	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)0) = 0)
194	167, 188, 193	3eqtrrd 2803	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘2))
195	194	mptru 1577	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘2)
196	115	fveq1d 6883	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘1) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1))
197		1nn0 12524	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
198	197	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 1 ∈ ℕ0)
199	2, 34, 35, 132	coe1subfv 22436	. . . . . . . . . . . . . . . . 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 11212	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
202		1lt3 12420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 3
203	201, 202	ltneii 11327	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 3
204		neeq1 3020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205	203, 204	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 3)
206	205	neneqd 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 3)
207	206	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208	207	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209	147, 208, 198, 157	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘1) = 0)
210		ax-1ne0 11173	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
211		neeq1 3020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212	210, 211	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 0)
213	212	neneqd 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
214	213	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215	214	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216	155, 215, 198, 157	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217	209, 216	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)) = (0(-g‘𝑄)0))
218	200, 217	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (0(-g‘𝑄)0))
219	196, 218, 193	3eqtrrd 2803	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘1))
220	219	mptru 1577	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘1)
221	115	fveq1d 6883	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘0) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0))
222	2, 34, 35, 132	coe1subfv 22436	. . . . . . . . . . . . . . . . 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 3012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 3
225		neeq1 3020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226	224, 225	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → 𝑖 ≠ 3)
227	226	neneqd 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 0 → ¬ 𝑖 = 3)
228	227	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229	228	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230	147, 229, 157, 157	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘0) = 0)
231		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232	231	iftrued 4495	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233	155, 232, 157, 169	fvmptd 6997	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234	230, 233	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)) = (0(-g‘𝑄)2))
235	223, 234	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (0(-g‘𝑄)2))
236		df-neg 11448	. . . . . . . . . . . . . . . 16 ⊢ -2 = (0 − 2)
237	36, 3, 132	subgsub 19209	. . . . . . . . . . . . . . . . 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 2811	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)2) = -2)
240	221, 235, 239	3eqtrrd 2803	. . . . . . . . . . . . . 14 ⊢ (⊤ → -2 = ((coe1‘𝐹)‘0))
241	240	mptru 1577	. . . . . . . . . . . . 13 ⊢ -2 = ((coe1‘𝐹)‘0)
242	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ Field)
243	242	fldcrngd 20851	. . . . . . . . . . . . 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 33877	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250		qsscn 12988	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ ℂ
251		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253	252, 6	mgpbas 20225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ = (Base‘(mulGrp‘ℂfld))
254	251, 253	ressbas2 17302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255	250, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
256	3, 252	mgpress 20230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld)) → ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄))
257	7, 13, 256	mp2an 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄)
258	257	fveq2i 6884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘((mulGrp‘ℂfld) ↾s ℚ)) = (Base‘(mulGrp‘𝑄))
259	255, 258	eqtri 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
260		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
261	260	ringmgp 20325	. . . . . . . . . . . . . . . . . . . 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 19165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265	250, 264	sselid 3935	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266	265	mullidd 11231	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267	257	eqcomi 2772	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268	250, 253	sseqtri 3985	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269	268	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
270	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ)
271	267, 269, 248, 270	ressmulgnnd 19148	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272		qcn 12991	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273		cnfldexp 21564	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274	272, 263, 273	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275	266, 271, 274	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276	168	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277	259, 112, 262, 276, 248	mulgnn0cld 19165	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278	250, 277	sselid 3935	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279	278	mul02d 11412	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280	275, 279	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281	272, 263	expcld 14187	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282	281	addridd 11414	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283	280, 282	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284	272	mul02d 11412	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285	284	oveq1d 7425	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
286	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℂ)
287	286	negcld 11560	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → -2 ∈ ℂ)
288	287	addlidd 11415	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → (0 + -2) = -2)
289	285, 288	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290	283, 289	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291	281, 286	negsubd 11579	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292	249, 290, 291	3eqtrd 2802	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293		2prm 16754	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℙ
294		3z 12631	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
295		3re 12325	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℝ
296	172, 295, 173	ltleii 11337	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 3
297	63	eluz1i 12874	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ (ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298	294, 296, 297	mpbir2an 723	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ (ℤ≥‘2)
299		rtprmirr 26934	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℙ ∧ 3 ∈ (ℤ≥‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300	293, 298, 299	mp2an 704	. . . . . . . . . . . . . 14 ⊢ (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301		eldifn 4086	. . . . . . . . . . . . . 14 ⊢ ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302	300, 301	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303		nelne2 3056	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304	302, 303	mpan2 703	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305		qre 12981	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306	305	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307		2pos 12349	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
308	281, 286	subeq0ad 11583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309	308	biimpa 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310	307, 309	breqtrrid 5149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
311	80	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312		n2dvds3 16433	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 2 ∥ 3
313	312	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314	306, 311, 313	expgt0b 33170	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315	310, 314	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < 𝑥)
316	306, 315	elrpd 13061	. . . . . . . . . . . . . . 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 26911	. . . . . . . . . . . . . 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 11990	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323	322	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = (𝑥↑𝑐1))
324	272	cxp1d 26880	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐1) = 𝑥)
325	323, 324	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
326	325	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
327		cxpexp 26842	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥↑𝑐3) = (𝑥↑3))
328	272, 263, 327	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐3) = (𝑥↑3))
329	328	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330	329	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331	319, 326, 330	3eqtr3rd 2807	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332	309	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)))
333	331, 332	eqtr3d 2800	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 = (2↑𝑐(1 / 3)))
334	304, 333	mteqand 3049	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335	292, 334	eqnetrd 3025	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) ≠ 0)
336	335	neneqd 2963	. . . . . . . . 9 ⊢ (𝑥 ∈ ℚ → ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
337	336	rgen 3081	. . . . . . . 8 ⊢ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0
338	337	a1i 11	. . . . . . 7 ⊢ (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
339		rabeq0 4345	. . . . . . 7 ⊢ ({𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
340	338, 339	sylibr 237	. . . . . 6 ⊢ (⊤ → {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341	105, 340	eqtrd 2798	. . . . 5 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = ∅)
342	90, 91, 92, 2, 34, 96, 100, 341, 130	ply1dg3rt0irred 33883	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Irred‘𝑃))
343		eqid 2763	. . . . . . 7 ⊢ (Irred‘𝑃) = (Irred‘𝑃)
344	343, 29	irredn0 20510	. . . . . 6 ⊢ ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g‘𝑃))
345	46, 342, 344	syl2anc 595	. . . . 5 ⊢ (⊤ → 𝐹 ≠ (0g‘𝑃))
346	3	fveq2i 6884	. . . . . . 7 ⊢ (deg1‘𝑄) = (deg1‘(ℂfld ↾s ℚ))
347	92, 346	eqtri 2786	. . . . . 6 ⊢ 𝐷 = (deg1‘(ℂfld ↾s ℚ))
348		eqid 2763	. . . . . 6 ⊢ (Monic1p‘(ℂfld ↾s ℚ)) = (Monic1p‘(ℂfld ↾s ℚ))
349		eqid 2763	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
350	349	qrng1 27795	. . . . . 6 ⊢ 1 = (1r‘(ℂfld ↾s ℚ))
351	5, 34, 29, 347, 348, 350	ismon1p 26309	. . . . 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 34115	. . 3 ⊢ (⊤ → 𝐹 = (𝑀‘𝐴))
354	353, 130	jca 520	. 2 ⊢ (⊤ → (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3))
355	354	mptru 1577	1 ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 400   = wceq 1570  ⊤wtru 1571   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  {crab 3416   ∖ cdif 3902   ⊆ wss 3905  ∅c0 4286  ifcif 4487  {csn 4589   class class class wbr 5109   ↦ cmpt 5192   I cid 5555  ^◡ccnv 5660   ↾ cres 5663   “ cima 5664   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410  ℂcc 11102  ℝcr 11103  0cc0 11104  1c1 11105   + caddc 11107   · cmul 11109   < clt 11247   ≤ cle 11248   − cmin 11445  -cneg 11446   / cdiv 11875  ℕcn 12237  2c2 12299  3c3 12300  ℕ₀cn0 12508  ℤcz 12595  ℤ_≥cuz 12866  ℚcq 12976  ↑cexp 14102   ∥ cdvds 16314  ℙcprime 16733  Basecbs 17273   ↾_s cress 17294  +_gcplusg 17314  ._rcmulr 17315  Scalarcsca 17317  0_gc0g 17496  Mndcmnd 18796  Grpcgrp 19004  -_gcsg 19006  ._gcmg 19137  SubGrpcsubg 19190  mulGrpcmgp 20220  Ringcrg 20319  CRingccrg 20320  Irredcir 20443  NzRingcnzr 20618  SubRingcsubrg 20677  DivRingcdr 20836  Fieldcfield 20837  SubDRingcsdrg 20898  LModclmod 20990  ℂ_fldccnfld 21531  algSccascl 22011  var₁cv1 22345  Poly₁cpl1 22346  coe₁cco1 22347   evalSub₁ ces1 22482  eval₁ce1 22483  deg₁cdg1 26220  Monic_1pcmn1 26292  ↑_𝑐ccxp 26729   minPoly cminply 34098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cnex 11160  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181  ax-pre-sup 11182  ax-addf 11183  ax-mulf 11184

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-ofr 7675  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-tpos 8218  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-card 9930  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-div 11876  df-nn 12238  df-2 12307  df-3 12308  df-4 12309  df-5 12310  df-6 12311  df-7 12312  df-8 12313  df-9 12314  df-n0 12509  df-z 12596  df-dec 12716  df-uz 12867  df-q 12977  df-rp 13021  df-xneg 13141  df-xadd 13142  df-xmul 13143  df-ioo 13380  df-ioc 13381  df-ico 13382  df-icc 13383  df-fz 13540  df-fzo 13688  df-fl 13830  df-mod 13908  df-seq 14043  df-exp 14103  df-fac 14315  df-bc 14344  df-hash 14372  df-shft 15109  df-cj 15155  df-re 15156  df-im 15157  df-sqrt 15291  df-abs 15292  df-limsup 15527  df-clim 15544  df-rlim 15545  df-sum 15743  df-ef 16125  df-sin 16127  df-cos 16128  df-pi 16130  df-dvds 16315  df-gcd 16557  df-prm 16734  df-numer 16798  df-denom 16799  df-struct 17211  df-sets 17228  df-slot 17246  df-ndx 17258  df-base 17274  df-ress 17295  df-plusg 17327  df-mulr 17328  df-starv 17329  df-sca 17330  df-vsca 17331  df-ip 17332  df-tset 17333  df-ple 17334  df-ds 17336  df-unif 17337  df-hom 17338  df-cco 17339  df-rest 17479  df-topn 17480  df-0g 17498  df-gsum 17499  df-topgen 17500  df-pt 17501  df-prds 17504  df-pws 17506  df-xrs 17560  df-qtop 17565  df-imas 17566  df-xps 17568  df-mre 17642  df-mrc 17643  df-acs 17645  df-mgm 18702  df-sgrp 18781  df-mnd 18797  df-mhm 18845  df-submnd 18846  df-grp 19007  df-minusg 19008  df-sbg 19009  df-mulg 19138  df-subg 19193  df-ghm 19288  df-cntz 19391  df-cmn 19856  df-abl 19857  df-mgp 20221  df-rng 20235  df-ur 20268  df-srg 20273  df-ring 20321  df-cring 20322  df-oppr 20424  df-dvdsr 20444  df-unit 20445  df-irred 20446  df-invr 20475  df-dvr 20488  df-rhm 20559  df-nzr 20619  df-subrng 20654  df-subrg 20678  df-rlreg 20802  df-domn 20803  df-idom 20804  df-drng 20838  df-field 20839  df-sdrg 20899  df-lmod 20992  df-lss 21062  df-lsp 21102  df-sra 21303  df-rgmod 21304  df-lidl 21341  df-rsp 21342  df-psmet 21523  df-xmet 21524  df-met 21525  df-bl 21526  df-mopn 21527  df-fbas 21528  df-fg 21529  df-cnfld 21532  df-assa 22012  df-asp 22013  df-ascl 22014  df-psr 22068  df-mvr 22069  df-mpl 22070  df-opsr 22072  df-evls 22234  df-evl 22235  df-psr1 22349  df-vr1 22350  df-ply1 22351  df-coe1 22352  df-evls1 22484  df-evl1 22485  df-top 23060  df-topon 23077  df-topsp 23099  df-bases 23112  df-cld 23185  df-ntr 23186  df-cls 23187  df-nei 23264  df-lp 23302  df-perf 23303  df-cn 23393  df-cnp 23394  df-haus 23481  df-tx 23728  df-hmeo 23921  df-fil 24012  df-fm 24104  df-flim 24105  df-flf 24106  df-xms 24486  df-ms 24487  df-tms 24488  df-cncf 25046  df-limc 26034  df-dv 26035  df-mdeg 26221  df-deg1 26222  df-mon1 26297  df-uc1p 26298  df-q1p 26299  df-r1p 26300  df-ig1p 26301  df-log 26730  df-cxp 26731  df-irng 34083  df-minply 34099

This theorem is used by:  2sqr3nconstr  34180