Theorem 2sqr3minply 33620

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 2726	. . . 4 ⊢ (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
2		2sqr3minply.p	. . . . 5 ⊢ 𝑃 = (Poly1‘𝑄)
3		2sqr3minply.q	. . . . . 6 ⊢ 𝑄 = (ℂfld ↾s ℚ)
4	3	fveq2i 6896	. . . . 5 ⊢ (Poly1‘𝑄) = (Poly1‘(ℂfld ↾s ℚ))
5	2, 4	eqtri 2754	. . . 4 ⊢ 𝑃 = (Poly1‘(ℂfld ↾s ℚ))
6		cnfldbas 21343	. . . 4 ⊢ ℂ = (Base‘ℂfld)
7		cndrng 21386	. . . . . 6 ⊢ ℂfld ∈ DivRing
8		cncrng 21376	. . . . . 6 ⊢ ℂfld ∈ CRing
9		isfld 20714	. . . . . 6 ⊢ (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
10	7, 8, 9	mpbir2an 709	. . . . 5 ⊢ ℂfld ∈ Field
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂfld ∈ Field)
12		qsubdrg 21412	. . . . . . 7 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
13	12	simpli 482	. . . . . 6 ⊢ ℚ ∈ (SubRing‘ℂfld)
14	12	simpri 484	. . . . . 6 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
15		issdrg 20763	. . . . . 6 ⊢ (ℚ ∈ (SubDRing‘ℂfld) ↔ (ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing))
16	7, 13, 14, 15	mpbir3an 1338	. . . . 5 ⊢ ℚ ∈ (SubDRing‘ℂfld)
17	16	a1i 11	. . . 4 ⊢ (⊤ → ℚ ∈ (SubDRing‘ℂfld))
18		2sqr3minply.a	. . . . . 6 ⊢ 𝐴 = (2↑𝑐(1 / 3))
19		2cn 12333	. . . . . . 7 ⊢ 2 ∈ ℂ
20		3cn 12339	. . . . . . . 8 ⊢ 3 ∈ ℂ
21		3ne0 12364	. . . . . . . 8 ⊢ 3 ≠ 0
22	20, 21	reccli 11989	. . . . . . 7 ⊢ (1 / 3) ∈ ℂ
23		cxpcl 26698	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
24	19, 22, 23	mp2an 690	. . . . . 6 ⊢ (2↑𝑐(1 / 3)) ∈ ℂ
25	18, 24	eqeltri 2822	. . . . 5 ⊢ 𝐴 ∈ ℂ
26	25	a1i 11	. . . 4 ⊢ (⊤ → 𝐴 ∈ ℂ)
27		cnfld0 21380	. . . 4 ⊢ 0 = (0g‘ℂfld)
28		2sqr3minply.m	. . . 4 ⊢ 𝑀 = (ℂfld minPoly ℚ)
29		eqid 2726	. . . 4 ⊢ (0g‘𝑃) = (0g‘𝑃)
30		2sqr3minply.f	. . . . . . . 8 ⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2))
31	30	fveq2i 6896	. . . . . . 7 ⊢ ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))
32	31	fveq1i 6894	. . . . . 6 ⊢ (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴)
33	32	a1i 11	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴))
34		eqid 2726	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
35		2sqr3minply.1	. . . . . 6 ⊢ − = (-g‘𝑃)
36		cnfldsub 21385	. . . . . 6 ⊢ − = (-g‘ℂfld)
37	8	a1i 11	. . . . . 6 ⊢ (⊤ → ℂfld ∈ CRing)
38	13	a1i 11	. . . . . 6 ⊢ (⊤ → ℚ ∈ (SubRing‘ℂfld))
39		eqid 2726	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
40	39, 34	mgpbas 20119	. . . . . . 7 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41		2sqr3minply.2	. . . . . . 7 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
42	3	qdrng 27646	. . . . . . . . . . 11 ⊢ 𝑄 ∈ DivRing
43	42	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝑄 ∈ DivRing)
44	43	drngringd 20711	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ Ring)
45	2	ply1ring 22233	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring)
46	44, 45	syl 17	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ Ring)
47	39	ringmgp 20218	. . . . . . . 8 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
48	46, 47	syl 17	. . . . . . 7 ⊢ (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49		3nn0 12536	. . . . . . . 8 ⊢ 3 ∈ ℕ0
50	49	a1i 11	. . . . . . 7 ⊢ (⊤ → 3 ∈ ℕ0)
51		2sqr3minply.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑄)
52	51, 2, 34	vr1cl 22203	. . . . . . . 8 ⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
53	44, 52	syl 17	. . . . . . 7 ⊢ (⊤ → 𝑋 ∈ (Base‘𝑃))
54	40, 41, 48, 50, 53	mulgnn0cld 19085	. . . . . 6 ⊢ (⊤ → (3 ↑ 𝑋) ∈ (Base‘𝑃))
55		2sqr3minply.k	. . . . . . . 8 ⊢ 𝐾 = (algSc‘𝑃)
56	44	mptru 1541	. . . . . . . . 9 ⊢ 𝑄 ∈ Ring
57	2	ply1sca 22238	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
58	56, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑄 = (Scalar‘𝑃)
59	2	ply1lmod 22237	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod)
60	44, 59	syl 17	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ LMod)
61	3	qrngbas 27645	. . . . . . . 8 ⊢ ℚ = (Base‘𝑄)
62	55, 58, 46, 60, 61, 34	asclf 21875	. . . . . . 7 ⊢ (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63		2z 12640	. . . . . . . 8 ⊢ 2 ∈ ℤ
64		zq 12984	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
65	63, 64	mp1i 13	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℚ)
66	62, 65	ffvelcdmd 7091	. . . . . 6 ⊢ (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
67	1, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26	evls1subd 33450	. . . . 5 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))‘𝐴) = ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)))
68		eqid 2726	. . . . . . . . . 10 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
69	1, 6, 2, 3, 34, 37, 38, 41, 68, 50, 53, 26	evls1expd 22355	. . . . . . . . 9 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
70	1, 51, 3, 6, 37, 38	evls1var 22326	. . . . . . . . . . . 12 ⊢ (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
71	70	fveq1d 6895	. . . . . . . . . . 11 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72		fvresi 7179	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
73	25, 72	mp1i 13	. . . . . . . . . . 11 ⊢ (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
74	71, 73	eqtrd 2766	. . . . . . . . . 10 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
75	74	oveq2d 7432	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76		cnfldexp 21392	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
77	26, 50, 76	syl2anc 582	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
78	69, 75, 77	3eqtrd 2770	. . . . . . . 8 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (𝐴↑3))
79	18	oveq1i 7426	. . . . . . . . 9 ⊢ (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80		3nn 12337	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
81		cxproot 26714	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
82	19, 80, 81	mp2an 690	. . . . . . . . 9 ⊢ ((2↑𝑐(1 / 3))↑3) = 2
83	79, 82	eqtri 2754	. . . . . . . 8 ⊢ (𝐴↑3) = 2
84	78, 83	eqtrdi 2782	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = 2)
85	1, 2, 3, 6, 55, 37, 38, 65, 26	evls1scafv 22354	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
86	84, 85	oveq12d 7434	. . . . . 6 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
87	19	subidi 11572	. . . . . 6 ⊢ (2 − 2) = 0
88	86, 87	eqtrdi 2782	. . . . 5 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = 0)
89	33, 67, 88	3eqtrd 2770	. . . 4 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝐴) = 0)
90	3	qrng0 27647	. . . . 5 ⊢ 0 = (0g‘𝑄)
91		eqid 2726	. . . . 5 ⊢ (eval1‘𝑄) = (eval1‘𝑄)
92		2sqr3minply.d	. . . . 5 ⊢ 𝐷 = (deg1‘𝑄)
93		fldsdrgfld 20773	. . . . . . . 8 ⊢ ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂfld ↾s ℚ) ∈ Field)
94	10, 16, 93	mp2an 690	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) ∈ Field
95	3, 94	eqeltri 2822	. . . . . 6 ⊢ 𝑄 ∈ Field
96	95	a1i 11	. . . . 5 ⊢ (⊤ → 𝑄 ∈ Field)
97	46	ringgrpd 20221	. . . . . . 7 ⊢ (⊤ → 𝑃 ∈ Grp)
98	34, 35	grpsubcl 19010	. . . . . . 7 ⊢ ((𝑃 ∈ Grp ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
99	97, 54, 66, 98	syl3anc 1368	. . . . . 6 ⊢ (⊤ → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
100	30, 99	eqeltrid 2830	. . . . 5 ⊢ (⊤ → 𝐹 ∈ (Base‘𝑃))
101	96	fldcrngd 20716	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ CRing)
102	91, 2, 34, 101, 61, 100	evl1fvf 33442	. . . . . . . 8 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹):ℚ⟶ℚ)
103	102	ffnd 6721	. . . . . . 7 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹) Fn ℚ)
104		fniniseg2 7067	. . . . . . 7 ⊢ (((eval1‘𝑄)‘𝐹) Fn ℚ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
105	103, 104	syl 17	. . . . . 6 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
106		cnfldmul 21347	. . . . . . . . . . . . . . 15 ⊢ · = (.r‘ℂfld)
107	3, 106	ressmulr 17316	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → · = (.r‘𝑄))
108	13, 107	ax-mp 5	. . . . . . . . . . . . 13 ⊢ · = (.r‘𝑄)
109		cnfldadd 21345	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘ℂfld)
110	3, 109	ressplusg 17299	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → + = (+g‘𝑄))
111	13, 110	ax-mp 5	. . . . . . . . . . . . 13 ⊢ + = (+g‘𝑄)
112		eqid 2726	. . . . . . . . . . . . 13 ⊢ (.g‘(mulGrp‘𝑄)) = (.g‘(mulGrp‘𝑄))
113		eqid 2726	. . . . . . . . . . . . 13 ⊢ (coe1‘𝐹) = (coe1‘𝐹)
114	30	fveq2i 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2)))
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2))))
116	30	fveq2i 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2)))
117	116	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))))
118		3pos 12363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 3
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 < 3)
120		2ne0 12362	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 2 ≠ 0)
122	92, 2, 61, 55, 90	deg1scl 26137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
123	44, 65, 121, 122	syl3anc 1368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(𝐾‘2)) = 0)
124		drngnzr 20722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
125	42, 124	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 𝑄 ∈ NzRing)
126	92, 2, 51, 39, 41	deg1pw 26145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 ↑ 𝑋)) = 3)
127	125, 50, 126	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(3 ↑ 𝑋)) = 3)
128	119, 123, 127	3brtr4d 5177	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 ↑ 𝑋)))
129	2, 92, 44, 34, 35, 54, 66, 128	deg1sub 26132	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) = (𝐷‘(3 ↑ 𝑋)))
130	117, 129, 127	3eqtrd 2770	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝐷‘𝐹) = 3)
131	115, 130	fveq12d 6900	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3))
132		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ (-g‘𝑄) = (-g‘𝑄)
133	2, 34, 35, 132	coe1subfv 22253	. . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
135		subrgsubg 20557	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℚ ∈ (SubRing‘ℂfld) → ℚ ∈ (SubGrp‘ℂfld))
136	13, 135	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ℚ ∈ (SubGrp‘ℂfld))
137		eqid 2726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(3 ↑ 𝑋)) = (coe1‘(3 ↑ 𝑋))
138	137, 34, 2, 61	coe1fvalcl 22198	. . . . . . . . . . . . . . . . . . 19 ⊢ (((3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
139	54, 50, 138	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
140		eqid 2726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141	140, 34, 2, 61	coe1fvalcl 22198	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
142	66, 50, 141	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
143	36, 3, 132	subgsub 19128	. . . . . . . . . . . . . . . . . 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 1368	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
145		iftrue 4529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
146	3	qrng1 27648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 = (1r‘𝑄)
147	2, 51, 41, 44, 50, 90, 146	coe1mon 33463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(3 ↑ 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148		1cnd 11250	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 1 ∈ ℂ)
149	145, 147, 50, 148	fvmptd4 7025	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) = 1)
150	21	neii 2932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 3 = 0
151		eqeq1 2730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152	150, 151	mtbiri 326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 3 → ¬ 𝑖 = 0)
153	152	iffalsed 4534	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
154	2, 55, 61, 90	coe1scl 22274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
155	44, 65, 154	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156		0nn0 12533	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℕ0
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 ∈ ℕ0)
158	153, 155, 50, 157	fvmptd4 7025	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159	149, 158	oveq12d 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160		1m0e1 12379	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
161	159, 160	eqtrdi 2782	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = 1)
162	144, 161	eqtr3d 2768	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)) = 1)
163	131, 134, 162	3eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1)
164	130	fveq2d 6897	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘3))
165	163, 164	eqtr3d 2768	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 = ((coe1‘𝐹)‘3))
166	165	mptru 1541	. . . . . . . . . . . . 13 ⊢ 1 = ((coe1‘𝐹)‘3)
167	115	fveq1d 6895	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘2) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2))
168		2nn0 12535	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
169	168	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 2 ∈ ℕ0)
170	2, 34, 35, 132	coe1subfv 22253	. . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)))
172		2re 12332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
173		2lt3 12430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < 3
174	172, 173	ltneii 11368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 3
175		neeq1 2993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176	174, 175	mpbiri 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 3)
177	176	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178	177	neneqd 2935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179	178	iffalsed 4534	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180	147, 179, 169, 157	fvmptd 7008	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘2) = 0)
181		neeq1 2993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182	120, 181	mpbiri 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 0)
183	182	neneqd 2935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 0)
184	183	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185	184	iffalsed 4534	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186	155, 185, 169, 157	fvmptd 7008	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187	180, 186	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)) = (0(-g‘𝑄)0))
188	171, 187	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (0(-g‘𝑄)0))
189	158, 142	eqeltrrd 2827	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 0 ∈ ℚ)
190	36, 3, 132	subgsub 19128	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ) → (0 − 0) = (0(-g‘𝑄)0))
191	136, 189, 189, 190	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 0) = (0(-g‘𝑄)0))
192		0m0e0 12378	. . . . . . . . . . . . . . . 16 ⊢ (0 − 0) = 0
193	191, 192	eqtr3di 2781	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)0) = 0)
194	167, 188, 193	3eqtrrd 2771	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘2))
195	194	mptru 1541	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘2)
196	115	fveq1d 6895	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘1) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1))
197		1nn0 12534	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
198	197	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 1 ∈ ℕ0)
199	2, 34, 35, 132	coe1subfv 22253	. . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)))
201		1re 11255	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
202		1lt3 12431	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 3
203	201, 202	ltneii 11368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 3
204		neeq1 2993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205	203, 204	mpbiri 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 3)
206	205	neneqd 2935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 3)
207	206	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208	207	iffalsed 4534	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209	147, 208, 198, 157	fvmptd 7008	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘1) = 0)
210		ax-1ne0 11218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
211		neeq1 2993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212	210, 211	mpbiri 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 0)
213	212	neneqd 2935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
214	213	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215	214	iffalsed 4534	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216	155, 215, 198, 157	fvmptd 7008	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217	209, 216	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)) = (0(-g‘𝑄)0))
218	200, 217	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (0(-g‘𝑄)0))
219	196, 218, 193	3eqtrrd 2771	. . . . . . . . . . . . . 14 ⊢ (⊤ → 0 = ((coe1‘𝐹)‘1))
220	219	mptru 1541	. . . . . . . . . . . . 13 ⊢ 0 = ((coe1‘𝐹)‘1)
221	115	fveq1d 6895	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘0) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0))
222	2, 34, 35, 132	coe1subfv 22253	. . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)))
224	21	necomi 2985	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 3
225		neeq1 2993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226	224, 225	mpbiri 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → 𝑖 ≠ 3)
227	226	neneqd 2935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 0 → ¬ 𝑖 = 3)
228	227	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229	228	iffalsed 4534	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230	147, 229, 157, 157	fvmptd 7008	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘0) = 0)
231		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232	231	iftrued 4531	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233	155, 232, 157, 169	fvmptd 7008	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234	230, 233	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)) = (0(-g‘𝑄)2))
235	223, 234	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (0(-g‘𝑄)2))
236		df-neg 11488	. . . . . . . . . . . . . . . 16 ⊢ -2 = (0 − 2)
237	36, 3, 132	subgsub 19128	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ) → (0 − 2) = (0(-g‘𝑄)2))
238	136, 189, 65, 237	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 2) = (0(-g‘𝑄)2))
239	236, 238	eqtr2id 2779	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (0(-g‘𝑄)2) = -2)
240	221, 235, 239	3eqtrrd 2771	. . . . . . . . . . . . . 14 ⊢ (⊤ → -2 = ((coe1‘𝐹)‘0))
241	240	mptru 1541	. . . . . . . . . . . . 13 ⊢ -2 = ((coe1‘𝐹)‘0)
242	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ Field)
243	242	fldcrngd 20716	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝑄 ∈ CRing)
244	100	mptru 1541	. . . . . . . . . . . . . 14 ⊢ 𝐹 ∈ (Base‘𝑃)
245	244	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → 𝐹 ∈ (Base‘𝑃))
246	130	mptru 1541	. . . . . . . . . . . . . 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 33456	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250		qsscn 12990	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ ℂ
251		eqid 2726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252		eqid 2726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253	252, 6	mgpbas 20119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ = (Base‘(mulGrp‘ℂfld))
254	251, 253	ressbas2 17246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255	250, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
256	3, 252	mgpress 20128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld)) → ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄))
257	7, 13, 256	mp2an 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄)
258	257	fveq2i 6896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘((mulGrp‘ℂfld) ↾s ℚ)) = (Base‘(mulGrp‘𝑄))
259	255, 258	eqtri 2754	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
260		eqid 2726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
261	260	ringmgp 20218	. . . . . . . . . . . . . . . . . . . 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 19085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265	250, 264	sselid 3976	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266	265	mullidd 11273	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267	257	eqcomi 2735	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268	250, 253	sseqtri 4015	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269	268	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
270	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ)
271	267, 269, 248, 270	ressmulgnnd 19068	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272		qcn 12993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273		cnfldexp 21392	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274	272, 263, 273	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275	266, 271, 274	3eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276	168	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277	259, 112, 262, 276, 248	mulgnn0cld 19085	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278	250, 277	sselid 3976	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279	278	mul02d 11453	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280	275, 279	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281	272, 263	expcld 14159	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282	281	addridd 11455	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283	280, 282	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284	272	mul02d 11453	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285	284	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
286	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℂ)
287	286	negcld 11599	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → -2 ∈ ℂ)
288	287	addlidd 11456	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → (0 + -2) = -2)
289	285, 288	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290	283, 289	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291	281, 286	negsubd 11618	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292	249, 290, 291	3eqtrd 2770	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293		2prm 16688	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℙ
294		3z 12641	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
295		3re 12338	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℝ
296	172, 295, 173	ltleii 11378	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 3
297	63	eluz1i 12876	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ (ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298	294, 296, 297	mpbir2an 709	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ (ℤ≥‘2)
299		rtprmirr 26785	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℙ ∧ 3 ∈ (ℤ≥‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300	293, 298, 299	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301		eldifn 4124	. . . . . . . . . . . . . 14 ⊢ ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302	300, 301	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303		nelne2 3030	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304	302, 303	mpan2 689	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305		qre 12983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306	305	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307		2pos 12361	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
308	281, 286	subeq0ad 11622	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309	308	biimpa 475	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310	307, 309	breqtrrid 5183	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
311	80	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312		n2dvds3 16368	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 2 ∥ 3
313	312	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314	306, 311, 313	expgt0b 32720	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315	310, 314	mpbird 256	. . . . . . . . . . . . . . . 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 26761	. . . . . . . . . . . . . 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 12030	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323	322	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = (𝑥↑𝑐1))
324	272	cxp1d 26730	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐1) = 𝑥)
325	323, 324	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
326	325	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
327		cxpexp 26692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥↑𝑐3) = (𝑥↑3))
328	272, 263, 327	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐3) = (𝑥↑3))
329	328	oveq1d 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330	329	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331	319, 326, 330	3eqtr3rd 2775	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332	309	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = (2↑𝑐(1 / 3)))
333	331, 332	eqtr3d 2768	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 = (2↑𝑐(1 / 3)))
334	304, 333	mteqand 3023	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335	292, 334	eqnetrd 2998	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) ≠ 0)
336	335	neneqd 2935	. . . . . . . . 9 ⊢ (𝑥 ∈ ℚ → ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
337	336	rgen 3053	. . . . . . . 8 ⊢ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0
338	337	a1i 11	. . . . . . 7 ⊢ (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
339		rabeq0 4382	. . . . . . 7 ⊢ ({𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
340	338, 339	sylibr 233	. . . . . 6 ⊢ (⊤ → {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341	105, 340	eqtrd 2766	. . . . 5 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = ∅)
342	90, 91, 92, 2, 34, 96, 100, 341, 130	ply1dg3rt0irred 33460	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Irred‘𝑃))
343		eqid 2726	. . . . . . 7 ⊢ (Irred‘𝑃) = (Irred‘𝑃)
344	343, 29	irredn0 20401	. . . . . 6 ⊢ ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g‘𝑃))
345	46, 342, 344	syl2anc 582	. . . . 5 ⊢ (⊤ → 𝐹 ≠ (0g‘𝑃))
346	3	fveq2i 6896	. . . . . . 7 ⊢ (deg1‘𝑄) = (deg1‘(ℂfld ↾s ℚ))
347	92, 346	eqtri 2754	. . . . . 6 ⊢ 𝐷 = (deg1‘(ℂfld ↾s ℚ))
348		eqid 2726	. . . . . 6 ⊢ (Monic1p‘(ℂfld ↾s ℚ)) = (Monic1p‘(ℂfld ↾s ℚ))
349		eqid 2726	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ)
350	349	qrng1 27648	. . . . . 6 ⊢ 1 = (1r‘(ℂfld ↾s ℚ))
351	5, 34, 29, 347, 348, 350	ismon1p 26167	. . . . 5 ⊢ (𝐹 ∈ (Monic1p‘(ℂfld ↾s ℚ)) ↔ (𝐹 ∈ (Base‘𝑃) ∧ 𝐹 ≠ (0g‘𝑃) ∧ ((coe1‘𝐹)‘(𝐷‘𝐹)) = 1))
352	100, 345, 163, 351	syl3anbrc 1340	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Monic1p‘(ℂfld ↾s ℚ)))
353	1, 5, 6, 11, 17, 26, 27, 28, 29, 89, 342, 352	irredminply 33589	. . 3 ⊢ (⊤ → 𝐹 = (𝑀‘𝐴))
354	353, 130	jca 510	. 2 ⊢ (⊤ → (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3))
355	354	mptru 1541	1 ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)

Syntax hints:  ¬ wn 3   ∧ wa 394   = wceq 1534  ⊤wtru 1535   ∈ wcel 2099   ≠ wne 2930  ∀wral 3051  {crab 3419   ∖ cdif 3943   ⊆ wss 3946  ∅c0 4322  ifcif 4523  {csn 4623   class class class wbr 5145   ↦ cmpt 5228   I cid 5571  ^◡ccnv 5673   ↾ cres 5676   “ cima 5677   Fn wfn 6541  ‘cfv 6546  (class class class)co 7416  ℂcc 11147  ℝcr 11148  0cc0 11149  1c1 11150   + caddc 11152   · cmul 11154   < clt 11289   ≤ cle 11290   − cmin 11485  -cneg 11486   / cdiv 11912  ℕcn 12258  2c2 12313  3c3 12314  ℕ₀cn0 12518  ℤcz 12604  ℤ_≥cuz 12868  ℚcq 12978  ↑cexp 14075   ∥ cdvds 16251  ℙcprime 16667  Basecbs 17208   ↾_s cress 17237  +_gcplusg 17261  ._rcmulr 17262  Scalarcsca 17264  0_gc0g 17449  Mndcmnd 18722  Grpcgrp 18923  -_gcsg 18925  ._gcmg 19057  SubGrpcsubg 19110  mulGrpcmgp 20113  Ringcrg 20212  CRingccrg 20213  Irredcir 20334  NzRingcnzr 20490  SubRingcsubrg 20547  DivRingcdr 20703  Fieldcfield 20704  SubDRingcsdrg 20761  LModclmod 20832  ℂ_fldccnfld 21339  algSccascl 21846  var₁cv1 22161  Poly₁cpl1 22162  coe₁cco1 22163   evalSub₁ ces1 22301  eval₁ce1 22302  deg₁cdg1 26075  Monic_1pcmn1 26150  ↑_𝑐ccxp 26579   minPoly cminply 33574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228  ax-mulf 11229

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-ofr 7683  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-tpos 8233  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-z 12605  df-dec 12724  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13140  df-xadd 13141  df-xmul 13142  df-ioo 13376  df-ioc 13377  df-ico 13378  df-icc 13379  df-fz 13533  df-fzo 13676  df-fl 13806  df-mod 13884  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-sum 15686  df-ef 16064  df-sin 16066  df-cos 16067  df-pi 16069  df-dvds 16252  df-gcd 16490  df-prm 16668  df-numer 16732  df-denom 16733  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-pws 17459  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-mhm 18768  df-submnd 18769  df-grp 18926  df-minusg 18927  df-sbg 18928  df-mulg 19058  df-subg 19113  df-ghm 19203  df-cntz 19307  df-cmn 19776  df-abl 19777  df-mgp 20114  df-rng 20132  df-ur 20161  df-srg 20166  df-ring 20214  df-cring 20215  df-oppr 20312  df-dvdsr 20335  df-unit 20336  df-irred 20337  df-invr 20366  df-dvr 20379  df-rhm 20450  df-nzr 20491  df-subrng 20524  df-subrg 20549  df-rlreg 20668  df-domn 20669  df-idom 20670  df-drng 20705  df-field 20706  df-sdrg 20762  df-lmod 20834  df-lss 20905  df-lsp 20945  df-sra 21147  df-rgmod 21148  df-lidl 21193  df-rsp 21194  df-psmet 21331  df-xmet 21332  df-met 21333  df-bl 21334  df-mopn 21335  df-fbas 21336  df-fg 21337  df-cnfld 21340  df-assa 21847  df-asp 21848  df-ascl 21849  df-psr 21902  df-mvr 21903  df-mpl 21904  df-opsr 21906  df-evls 22083  df-evl 22084  df-psr1 22165  df-vr1 22166  df-ply1 22167  df-coe1 22168  df-evls1 22303  df-evl1 22304  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22937  df-cld 23011  df-ntr 23012  df-cls 23013  df-nei 23090  df-lp 23128  df-perf 23129  df-cn 23219  df-cnp 23220  df-haus 23307  df-tx 23554  df-hmeo 23747  df-fil 23838  df-fm 23930  df-flim 23931  df-flf 23932  df-xms 24314  df-ms 24315  df-tms 24316  df-cncf 24886  df-limc 25883  df-dv 25884  df-mdeg 26076  df-deg1 26077  df-mon1 26155  df-uc1p 26156  df-q1p 26157  df-r1p 26158  df-ig1p 26159  df-log 26580  df-cxp 26581  df-irng 33566  df-minply 33575

This theorem is referenced by: (None)