Theorem 2sqr3minply 33976

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 2741	. . . 4 ⊢ (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
2		2sqr3minply.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑄)
3		2sqr3minply.q	. . . . . 6 ⊢ 𝑄 = (ℂfld ↾s ℚ)
4	3	fveq2i 6834	. . . . 5 ⊢ (Poly1‘𝑄) = (Poly1‘(ℂfld ↾s ℚ))
5	2, 4	eqtri 2764	. . . 4 ⊢ 𝑃 = (Poly1‘(ℂfld ↾s ℚ))
6		cnfldbas 21355	. . . 4 ⊢ ℂ = (Base‘ℂfld)
7		cndrng 21380	. . . . . 6 ⊢ ℂfld ∈ DivRing
8		cncrng 21372	. . . . . 6 ⊢ ℂfld ∈ CRing
9		isfld 20716	. . . . . 6 ⊢ (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
10	7, 8, 9	mpbir2an 718	. . . . 5 ⊢ ℂfld ∈ Field
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂfld ∈ Field)
12		qsubdrg 21398	. . . . . . 7 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
13	12	simpli 485	. . . . . 6 ⊢ ℚ ∈ (SubRing‘ℂfld)
14	12	simpri 487	. . . . . 6 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
15		issdrg 20764	. . . . . 6 ⊢ (ℚ ∈ (SubDRing‘ℂfld) ↔ (ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing))
16	7, 13, 14, 15	mpbir3an 1349	. . . . 5 ⊢ ℚ ∈ (SubDRing‘ℂfld)
17	16	a1i 11	. . . 4 ⊢ (⊤ → ℚ ∈ (SubDRing‘ℂfld))
18		2sqr3minply.a	. . . . . 6 ⊢ 𝐴 = (2↑𝑐(1 / 3))
19		2cn 12251	. . . . . . 7 ⊢ 2 ∈ ℂ
20		3cn 12257	. . . . . . . 8 ⊢ 3 ∈ ℂ
21		3ne0 12282	. . . . . . . 8 ⊢ 3 ≠ 0
22	20, 21	reccli 11880	. . . . . . 7 ⊢ (1 / 3) ∈ ℂ
23		cxpcl 26660	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
24	19, 22, 23	mp2an 699	. . . . . 6 ⊢ (2↑𝑐(1 / 3)) ∈ ℂ
25	18, 24	eqeltri 2837	. . . . 5 ⊢ 𝐴 ∈ ℂ
26	25	a1i 11	. . . 4 ⊢ (⊤ → 𝐴 ∈ ℂ)
27		cnfld0 21375	. . . 4 ⊢ 0 = (0g‘ℂfld)
28		2sqr3minply.m	. . . 4 ⊢ 𝑀 = (ℂfld minPoly ℚ)
29		eqid 2741	. . . 4 ⊢ (0g‘𝑃) = (0g‘𝑃)
30		2sqr3minply.f	. . . . . . . 8 ⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2))
31	30	fveq2i 6834	. . . . . . 7 ⊢ ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))
32	31	fveq1i 6832	. . . . . 6 ⊢ (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴)
33	32	a1i 11	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴))
34		eqid 2741	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
35		2sqr3minply.1	. . . . . 6 ⊢ − = (-g‘𝑃)
36		cnfldsub 21379	. . . . . 6 ⊢ − = (-g‘ℂfld)
37	8	a1i 11	. . . . . 6 ⊢ (⊤ → ℂfld ∈ CRing)
38	13	a1i 11	. . . . . 6 ⊢ (⊤ → ℚ ∈ (SubRing‘ℂfld))
39		eqid 2741	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
40	39, 34	mgpbas 20121	. . . . . . 7 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41		2sqr3minply.2	. . . . . . 7 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
42	3	qdrng 27605	. . . . . . . . . . 11 ⊢ 𝑄 ∈ DivRing
43	42	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝑄 ∈ DivRing)
44	43	drngringd 20713	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ Ring)
45	2	ply1ring 22236	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring)
46	44, 45	syl 17	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ Ring)
47	39	ringmgp 20215	. . . . . . . 8 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
48	46, 47	syl 17	. . . . . . 7 ⊢ (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49		3nn0 12450	. . . . . . . 8 ⊢ 3 ∈ ℕ0
50	49	a1i 11	. . . . . . 7 ⊢ (⊤ → 3 ∈ ℕ0)
51		2sqr3minply.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑄)
52	51, 2, 34	vr1cl 22206	. . . . . . . 8 ⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
53	44, 52	syl 17	. . . . . . 7 ⊢ (⊤ → 𝑋 ∈ (Base‘𝑃))
54	40, 41, 48, 50, 53	mulgnn0cld 19066	. . . . . 6 ⊢ (⊤ → (3 ↑ 𝑋) ∈ (Base‘𝑃))
55		2sqr3minply.k	. . . . . . . 8 ⊢ 𝐾 = (algSc‘𝑃)
56	44	mptru 1555	. . . . . . . . 9 ⊢ 𝑄 ∈ Ring
57	2	ply1sca 22241	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
58	56, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑄 = (Scalar‘𝑃)
59	2	ply1lmod 22240	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod)
60	44, 59	syl 17	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ LMod)
61	3	qrngbas 27604	. . . . . . . 8 ⊢ ℚ = (Base‘𝑄)
62	55, 58, 46, 60, 61, 34	asclf 21860	. . . . . . 7 ⊢ (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63		2z 12554	. . . . . . . 8 ⊢ 2 ∈ ℤ
64		zq 12899	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
65	63, 64	mp1i 13	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℚ)
66	62, 65	ffvelcdmd 7030	. . . . . 6 ⊢ (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
67	1, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26	evls1subd 33667	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴) = ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)))
68		eqid 2741	. . . . . . . . . 10 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
69	1, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26	evls1expd 22357	. . . . . . . . 9 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
70	1, 51, 3, 6, 37, 38	evls1var 22328	. . . . . . . . . . . 12 ⊢ (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
71	70	fveq1d 6833	. . . . . . . . . . 11 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72		fvresi 7121	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
73	25, 72	mp1i 13	. . . . . . . . . . 11 ⊢ (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
74	71, 73	eqtrd 2776	. . . . . . . . . 10 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
75	74	oveq2d 7376	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76		cnfldexp 21384	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
77	26, 50, 76	syl2anc 591	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
78	69, 75, 77	3eqtrd 2780	. . . . . . . 8 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (𝐴↑3))
79	18	oveq1i 7370	. . . . . . . . 9 ⊢ (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80		3nn 12255	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
81		cxproot 26676	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
82	19, 80, 81	mp2an 699	. . . . . . . . 9 ⊢ ((2↑𝑐(1 / 3))↑3) = 2
83	79, 82	eqtri 2764	. . . . . . . 8 ⊢ (𝐴↑3) = 2
84	78, 83	eqtrdi 2792	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = 2)
85	1, 2, 3, 6, 55, 37, 38, 65, 26	evls1scafv 22356	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
86	84, 85	oveq12d 7378	. . . . . 6 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
87	19	subidi 11460	. . . . . 6 ⊢ (2 − 2) = 0
88	86, 87	eqtrdi 2792	. . . . 5 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0)
89	33, 67, 88	3eqtrd 2780	. . . 4 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0)
90	3	qrng0 27606	. . . . 5 ⊢ 0 = (0g‘𝑄)
91		eqid 2741	. . . . 5 ⊢ (eval1‘𝑄) = (eval1‘𝑄)
92		2sqr3minply.d	. . . . 5 ⊢ 𝐷 = (deg1‘𝑄)
93		fldsdrgfld 20774	. . . . . . . 8 ⊢ ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂfld ↾s ℚ) ∈ Field)
94	10, 16, 93	mp2an 699	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) ∈ Field
95	3, 94	eqeltri 2837	. . . . . 6 ⊢ 𝑄 ∈ Field
96	95	a1i 11	. . . . 5 ⊢ (⊤ → 𝑄 ∈ Field)
97	46	ringgrpd 20218	. . . . . . 7 ⊢ (⊤ → 𝑃 ∈ Grp)
98	34, 35	grpsubcl 18991	. . . . . . 7 ⊢ ((𝑃 ∈ Grp ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
99	97, 54, 66, 98	syl3anc 1380	. . . . . 6 ⊢ (⊤ → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
100	30, 99	eqeltrid 2845	. . . . 5 ⊢ (⊤ → 𝐹 ∈ (Base‘𝑃))
101	96	fldcrngd 20718	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ CRing)
102	91, 2, 34, 101, 61, 100	evl1fvf 33658	. . . . . . . 8 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹):ℚ⟶ℚ)
103	102	ffnd 6660	. . . . . . 7 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹) Fn ℚ)
104		fniniseg2 7007	. . . . . . 7 ⊢ (((eval1‘𝑄)‘𝐹) Fn ℚ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
105	103, 104	syl 17	. . . . . 6 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
106		cnfldmul 21359	. . . . . . . . . . . . . . 15 ⊢ · = (.r‘ℂfld)
107	3, 106	ressmulr 17265	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → · = (.r‘𝑄))
108	13, 107	ax-mp 5	. . . . . . . . . . . . 13 ⊢ · = (.r‘𝑄)
109		cnfldadd 21357	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘ℂfld)
110	3, 109	ressplusg 17249	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → + = (+g‘𝑄))
111	13, 110	ax-mp 5	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑄)
112		eqid 2741	. . . . . . . . . . . . 13 ⊢ (.g‘(mulGrp‘𝑄)) = (.g‘(mulGrp‘𝑄))
113		eqid 2741	. . . . . . . . . . . . 13 ⊢ (coe1‘𝐹) = (coe1‘𝐹)
114	30	fveq2i 6834	. . . . . . . . . . . . . . . . . 18 ⊢ (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2)))
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2))))
116	30	fveq2i 6834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2)))
117	116	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))))
118		3pos 12281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 3
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 < 3)
120		2ne0 12280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 2 ≠ 0)
122	92, 2, 61, 55, 90	deg1scl 26100	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
123	44, 65, 121, 122	syl3anc 1380	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(𝐾‘2)) = 0)
124		drngnzr 20724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
125	42, 124	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 𝑄 ∈ NzRing)
126	92, 2, 51, 39, 41	deg1pw 26108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 ↑ 𝑋)) = 3)
127	125, 50, 126	syl2anc 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(3 ↑ 𝑋)) = 3)
128	119, 123, 127	3brtr4d 5107	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 ↑ 𝑋)))
129	2, 92, 44, 34, 35, 54, 66, 128	deg1sub 26095	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) = (𝐷‘(3 ↑ 𝑋)))
130	117, 129, 127	3eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝐷‘𝐹) = 3)
131	115, 130	fveq12d 6838	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3))
132		eqid 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (-g‘𝑄) = (-g‘𝑄)
133	2, 34, 35, 132	coe1subfv 22256	. . . . . . . . . . . . . . . . 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 1382	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
135		subrgsubg 20553	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℚ ∈ (SubRing‘ℂfld) → ℚ ∈ (SubGrp‘ℂfld))
136	13, 135	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ℚ ∈ (SubGrp‘ℂfld))
137		eqid 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(3 ↑ 𝑋)) = (coe1‘(3 ↑ 𝑋))
138	137, 34, 2, 61	coe1fvalcl 22201	. . . . . . . . . . . . . . . . . . 19 ⊢ (((3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
139	54, 50, 138	syl2anc 591	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
140		eqid 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141	140, 34, 2, 61	coe1fvalcl 22201	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
142	66, 50, 141	syl2anc 591	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
143	36, 3, 132	subgsub 19109	. . . . . . . . . . . . . . . . . 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 1380	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
145		iftrue 4463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
146	3	qrng1 27607	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 = (1r‘𝑄)
147	2, 51, 41, 44, 50, 90, 146	coe1mon 33682	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(3 ↑ 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148		1cnd 11134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 1 ∈ ℂ)
149	145, 147, 50, 148	fvmptd4 6964	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) = 1)
150	21	neii 2938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 3 = 0
151		eqeq1 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152	150, 151	mtbiri 329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 3 → ¬ 𝑖 = 0)
153	152	iffalsed 4468	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
154	2, 55, 61, 90	coe1scl 22277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
155	44, 65, 154	syl2anc 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156		0nn0 12447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℕ0
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 ∈ ℕ0)
158	153, 155, 50, 157	fvmptd4 6964	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159	149, 158	oveq12d 7378	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160		1m0e1 12292	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
161	159, 160	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = 1)
162	144, 161	eqtr3d 2778	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)) = 1)
163	131, 134, 162	3eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1)
164	130	fveq2d 6835	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘3))
165	163, 164	eqtr3d 2778	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 = ((coe1‘𝐹)‘3))
166	165	mptru 1555	. . . . . . . . . . . . 13 ⊢ 1 = ((coe1‘𝐹)‘3)
167	115	fveq1d 6833	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘2) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2))
168		2nn0 12449	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
169	168	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 2 ∈ ℕ0)
170	2, 34, 35, 132	coe1subfv 22256	. . . . . . . . . . . . . . . . 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 1382	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)))
172		2re 12250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
173		2lt3 12343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < 3
174	172, 173	ltneii 11254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 3
175		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176	174, 175	mpbiri 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 3)
177	176	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178	177	neneqd 2941	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179	178	iffalsed 4468	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180	147, 179, 169, 157	fvmptd 6947	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘2) = 0)
181		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182	120, 181	mpbiri 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 0)
183	182	neneqd 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 0)
184	183	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185	184	iffalsed 4468	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186	155, 185, 169, 157	fvmptd 6947	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187	180, 186	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)) = (0(-g‘𝑄)0))
188	171, 187	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (0(-g‘𝑄)0))
189	158, 142	eqeltrrd 2842	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 0 ∈ ℚ)
190	36, 3, 132	subgsub 19109	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ) → (0 − 0) = (0(-g‘𝑄)0))
191	136, 189, 189, 190	syl3anc 1380	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 0) = (0(-g‘𝑄)0))
192		0m0e0 12291	. . . . . . . . . . . . . . . 16 ⊢ (0 − 0) = 0
193	191, 192	eqtr3di 2791	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)0) = 0)
194	167, 188, 193	3eqtrrd 2781	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘2))
195	194	mptru 1555	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘2)
196	115	fveq1d 6833	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘1) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1))
197		1nn0 12448	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
198	197	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 1 ∈ ℕ0)
199	2, 34, 35, 132	coe1subfv 22256	. . . . . . . . . . . . . . . . 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 1382	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)))
201		1re 11139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
202		1lt3 12344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 3
203	201, 202	ltneii 11254	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 3
204		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205	203, 204	mpbiri 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 3)
206	205	neneqd 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 3)
207	206	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208	207	iffalsed 4468	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209	147, 208, 198, 157	fvmptd 6947	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘1) = 0)
210		ax-1ne0 11102	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
211		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212	210, 211	mpbiri 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 0)
213	212	neneqd 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
214	213	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215	214	iffalsed 4468	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216	155, 215, 198, 157	fvmptd 6947	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217	209, 216	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)) = (0(-g‘𝑄)0))
218	200, 217	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (0(-g‘𝑄)0))
219	196, 218, 193	3eqtrrd 2781	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘1))
220	219	mptru 1555	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘1)
221	115	fveq1d 6833	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘0) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0))
222	2, 34, 35, 132	coe1subfv 22256	. . . . . . . . . . . . . . . . 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 1382	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)))
224	21	necomi 2990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 3
225		neeq1 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226	224, 225	mpbiri 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → 𝑖 ≠ 3)
227	226	neneqd 2941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 0 → ¬ 𝑖 = 3)
228	227	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229	228	iffalsed 4468	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230	147, 229, 157, 157	fvmptd 6947	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘0) = 0)
231		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232	231	iftrued 4465	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233	155, 232, 157, 169	fvmptd 6947	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234	230, 233	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)) = (0(-g‘𝑄)2))
235	223, 234	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (0(-g‘𝑄)2))
236		df-neg 11375	. . . . . . . . . . . . . . . 16 ⊢ -2 = (0 − 2)
237	36, 3, 132	subgsub 19109	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ) → (0 − 2) = (0(-g‘𝑄)2))
238	136, 189, 65, 237	syl3anc 1380	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 2) = (0(-g‘𝑄)2))
239	236, 238	eqtr2id 2789	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)2) = -2)
240	221, 235, 239	3eqtrrd 2781	. . . . . . . . . . . . . 14 ⊢ (⊤ → -2 = ((coe1‘𝐹)‘0))
241	240	mptru 1555	. . . . . . . . . . . . 13 ⊢ -2 = ((coe1‘𝐹)‘0)
242	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ Field)
243	242	fldcrngd 20718	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ CRing)
244	100	mptru 1555	. . . . . . . . . . . . . 14 ⊢ 𝐹 ∈ (Base‘𝑃)
245	244	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝐹 ∈ (Base‘𝑃))
246	130	mptru 1555	. . . . . . . . . . . . . 14 ⊢ (𝐷‘𝐹) = 3
247	246	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → (𝐷‘𝐹) = 3)
248		id 22	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℚ)
249	2, 91, 61, 34, 108, 111, 112, 113, 92, 166, 195, 220, 241, 243, 245, 247, 248	evl1deg3 33673	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250		qsscn 12905	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ ℂ
251		eqid 2741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252		eqid 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253	252, 6	mgpbas 20121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ = (Base‘(mulGrp‘ℂfld))
254	251, 253	ressbas2 17203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255	250, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
256	3, 252	mgpress 20126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld)) → ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄))
257	7, 13, 256	mp2an 699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄)
258	257	fveq2i 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘((mulGrp‘ℂfld) ↾s ℚ)) = (Base‘(mulGrp‘𝑄))
259	255, 258	eqtri 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
260		eqid 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
261	260	ringmgp 20215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
262	56, 261	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (mulGrp‘𝑄) ∈ Mnd)
263	49	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ0)
264	259, 112, 262, 263, 248	mulgnn0cld 19066	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265	250, 264	sselid 3915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266	265	mullidd 11158	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267	257	eqcomi 2750	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268	250, 253	sseqtri 3965	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269	268	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
270	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ)
271	267, 269, 248, 270	ressmulgnnd 19049	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272		qcn 12908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273		cnfldexp 21384	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274	272, 263, 273	syl2anc 591	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275	266, 271, 274	3eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276	168	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277	259, 112, 262, 276, 248	mulgnn0cld 19066	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278	250, 277	sselid 3915	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279	278	mul02d 11339	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280	275, 279	oveq12d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281	272, 263	expcld 14103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282	281	addridd 11341	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283	280, 282	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284	272	mul02d 11339	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285	284	oveq1d 7375	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
286	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℂ)
287	286	negcld 11487	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → -2 ∈ ℂ)
288	287	addlidd 11342	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → (0 + -2) = -2)
289	285, 288	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290	283, 289	oveq12d 7378	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291	281, 286	negsubd 11506	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292	249, 290, 291	3eqtrd 2780	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293		2prm 16656	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℙ
294		3z 12555	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
295		3re 12256	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℝ
296	172, 295, 173	ltleii 11264	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 3
297	63	eluz1i 12791	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ (ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298	294, 296, 297	mpbir2an 718	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ (ℤ≥‘2)
299		rtprmirr 26746	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℙ ∧ 3 ∈ (ℤ≥‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300	293, 298, 299	mp2an 699	. . . . . . . . . . . . . 14 ⊢ (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301		eldifn 4065	. . . . . . . . . . . . . 14 ⊢ ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302	300, 301	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303		nelne2 3034	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304	302, 303	mpan2 698	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305		qre 12898	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306	305	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307		2pos 12279	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
308	281, 286	subeq0ad 11510	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309	308	biimpa 478	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310	307, 309	breqtrrid 5113	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
311	80	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312		n2dvds3 16335	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 2 ∥ 3
313	312	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314	306, 311, 313	expgt0b 32913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315	310, 314	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < 𝑥)
316	306, 315	elrpd 12978	. . . . . . . . . . . . . . 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 26723	. . . . . . . . . . . . . 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 11921	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323	322	oveq2d 7376	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = (𝑥↑𝑐1))
324	272	cxp1d 26692	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐1) = 𝑥)
325	323, 324	eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
326	325	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
327		cxpexp 26654	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥↑𝑐3) = (𝑥↑3))
328	272, 263, 327	syl2anc 591	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐3) = (𝑥↑3))
329	328	oveq1d 7375	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330	329	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331	319, 326, 330	3eqtr3rd 2785	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332	309	oveq1d 7375	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)))
333	331, 332	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 = (2↑𝑐(1 / 3)))
334	304, 333	mteqand 3027	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335	292, 334	eqnetrd 3003	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) ≠ 0)
336	335	neneqd 2941	. . . . . . . . 9 ⊢ (𝑥 ∈ ℚ → ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
337	336	rgen 3057	. . . . . . . 8 ⊢ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0
338	337	a1i 11	. . . . . . 7 ⊢ (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
339		rabeq0 4319	. . . . . . 7 ⊢ ({𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
340	338, 339	sylibr 236	. . . . . 6 ⊢ (⊤ → {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341	105, 340	eqtrd 2776	. . . . 5 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = ∅)
342	90, 91, 92, 2, 34, 96, 100, 341, 130	ply1dg3rt0irred 33679	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Irred‘𝑃))
343		eqid 2741	. . . . . . 7 ⊢ (Irred‘𝑃) = (Irred‘𝑃)
344	343, 29	irredn0 20398	. . . . . 6 ⊢ ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g‘𝑃))
345	46, 342, 344	syl2anc 591	. . . . 5 ⊢ (⊤ → 𝐹 ≠ (0g‘𝑃))
346	3	fveq2i 6834	. . . . . . 7 ⊢ (deg1‘𝑄) = (deg1‘(ℂfld ↾s ℚ))
347	92, 346	eqtri 2764	. . . . . 6 ⊢ 𝐷 = (deg1‘(ℂfld ↾s ℚ))
348		eqid 2741	. . . . . 6 ⊢ (Monic1p‘(ℂfld ↾s ℚ)) = (Monic1p‘(ℂfld ↾s ℚ))
349		eqid 2741	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
350	349	qrng1 27607	. . . . . 6 ⊢ 1 = (1r‘(ℂfld ↾s ℚ))
351	5, 34, 29, 347, 348, 350	ismon1p 26130	. . . . 5 ⊢ (𝐹 ∈ (Monic1p‘(ℂfld ↾s ℚ)) ↔ (𝐹 ∈ (Base‘𝑃) ∧ 𝐹 ≠ (0g‘𝑃) ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1))
352	100, 345, 163, 351	syl3anbrc 1351	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Monic1p‘(ℂfld ↾s ℚ)))
353	1, 5, 6, 11, 17, 26, 27, 28, 29, 89, 342, 352	irredminply 33912	. . 3 ⊢ (⊤ → 𝐹 = (𝑀‘𝐴))
354	353, 130	jca 517	. 2 ⊢ (⊤ → (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3))
355	354	mptru 1555	1 ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)

Syntax hints:  ¬ wn 3   ∧ wa 397   = wceq 1548  ⊤wtru 1549   ∈ wcel 2121   ≠ wne 2936  ∀wral 3055  {crab 3393   ∖ cdif 3882   ⊆ wss 3885  ∅c0 4264  ifcif 4457  {csn 4558   class class class wbr 5075   ↦ cmpt 5156   I cid 5515  ^◡ccnv 5620   ↾ cres 5623   “ cima 5624   Fn wfn 6484  ‘cfv 6489  (class class class)co 7360  ℂcc 11031  ℝcr 11032  0cc0 11033  1c1 11034   + caddc 11036   · cmul 11038   < clt 11174   ≤ cle 11175   − cmin 11372  -cneg 11373   / cdiv 11802  ℕcn 12169  2c2 12231  3c3 12232  ℕ₀cn0 12432  ℤcz 12519  ℤ_≥cuz 12783  ℚcq 12893  ↑cexp 14018   ∥ cdvds 16216  ℙcprime 16635  Basecbs 17174   ↾_s cress 17195  +_gcplusg 17215  ._rcmulr 17216  Scalarcsca 17218  0_gc0g 17397  Mndcmnd 18697  Grpcgrp 18904  -_gcsg 18906  ._gcmg 19038  SubGrpcsubg 19091  mulGrpcmgp 20116  Ringcrg 20209  CRingccrg 20210  Irredcir 20331  NzRingcnzr 20488  SubRingcsubrg 20545  DivRingcdr 20705  Fieldcfield 20706  SubDRingcsdrg 20762  LModclmod 20854  ℂ_fldccnfld 21351  algSccascl 21831  var₁cv1 22165  Poly₁cpl1 22166  coe₁cco1 22167   evalSub₁ ces1 22303  eval₁ce1 22304  deg₁cdg1 26041  Monic_1pcmn1 26113  ↑_𝑐ccxp 26541   minPoly cminply 33895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-inf2 9557  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-pre-sup 11111  ax-addf 11112  ax-mulf 11113

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-iin 4927  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-ofr 7625  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8105  df-tpos 8170  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-fi 9318  df-sup 9349  df-inf 9350  df-oi 9419  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-q 12894  df-rp 12938  df-xneg 13058  df-xadd 13059  df-xmul 13060  df-ioo 13297  df-ioc 13298  df-ico 13299  df-icc 13300  df-fz 13457  df-fzo 13604  df-fl 13746  df-mod 13824  df-seq 13959  df-exp 14019  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15024  df-cj 15056  df-re 15057  df-im 15058  df-sqrt 15192  df-abs 15193  df-limsup 15428  df-clim 15445  df-rlim 15446  df-sum 15644  df-ef 16027  df-sin 16029  df-cos 16030  df-pi 16032  df-dvds 16217  df-gcd 16459  df-prm 16636  df-numer 16700  df-denom 16701  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-starv 17230  df-sca 17231  df-vsca 17232  df-ip 17233  df-tset 17234  df-ple 17235  df-ds 17237  df-unif 17238  df-hom 17239  df-cco 17240  df-rest 17380  df-topn 17381  df-0g 17399  df-gsum 17400  df-topgen 17401  df-pt 17402  df-prds 17405  df-pws 17407  df-xrs 17461  df-qtop 17466  df-imas 17467  df-xps 17469  df-mre 17543  df-mrc 17544  df-acs 17546  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18746  df-submnd 18747  df-grp 18907  df-minusg 18908  df-sbg 18909  df-mulg 19039  df-subg 19094  df-ghm 19183  df-cntz 19287  df-cmn 19752  df-abl 19753  df-mgp 20117  df-rng 20129  df-ur 20158  df-srg 20163  df-ring 20211  df-cring 20212  df-oppr 20312  df-dvdsr 20332  df-unit 20333  df-irred 20334  df-invr 20363  df-dvr 20376  df-rhm 20447  df-nzr 20489  df-subrng 20522  df-subrg 20546  df-rlreg 20670  df-domn 20671  df-idom 20672  df-drng 20707  df-field 20708  df-sdrg 20763  df-lmod 20856  df-lss 20926  df-lsp 20966  df-sra 21167  df-rgmod 21168  df-lidl 21205  df-rsp 21206  df-psmet 21343  df-xmet 21344  df-met 21345  df-bl 21346  df-mopn 21347  df-fbas 21348  df-fg 21349  df-cnfld 21352  df-assa 21832  df-asp 21833  df-ascl 21834  df-psr 21888  df-mvr 21889  df-mpl 21890  df-opsr 21892  df-evls 22054  df-evl 22055  df-psr1 22169  df-vr1 22170  df-ply1 22171  df-coe1 22172  df-evls1 22305  df-evl1 22306  df-top 22881  df-topon 22898  df-topsp 22920  df-bases 22933  df-cld 23006  df-ntr 23007  df-cls 23008  df-nei 23085  df-lp 23123  df-perf 23124  df-cn 23214  df-cnp 23215  df-haus 23302  df-tx 23549  df-hmeo 23742  df-fil 23833  df-fm 23925  df-flim 23926  df-flf 23927  df-xms 24307  df-ms 24308  df-tms 24309  df-cncf 24867  df-limc 25855  df-dv 25856  df-mdeg 26042  df-deg1 26043  df-mon1 26118  df-uc1p 26119  df-q1p 26120  df-r1p 26121  df-ig1p 26122  df-log 26542  df-cxp 26543  df-irng 33880  df-minply 33896

This theorem is referenced by:  2sqr3nconstr  33977