Theorem 2sqr3minply 34479

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 6908	. . . . 5 ⊢ (Poly1‘𝑄) = (Poly1‘(ℂfld ↾s ℚ))
5	2, 4	eqtri 2786	. . . 4 ⊢ 𝑃 = (Poly1‘(ℂfld ↾s ℚ))
6		cnfldbas 21709	. . . 4 ⊢ ℂ = (Base‘ℂfld)
7		cndrng 21734	. . . . . 6 ⊢ ℂfld ∈ DivRing
8		cncrng 21726	. . . . . 6 ⊢ ℂfld ∈ CRing
9		isfld 21020	. . . . . 6 ⊢ (ℂfld ∈ Field ↔ (ℂfld ∈ DivRing ∧ ℂfld ∈ CRing))
10	7, 8, 9	mpbir2an 724	. . . . 5 ⊢ ℂfld ∈ Field
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂfld ∈ Field)
12		qsubdrg 21752	. . . . . . 7 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
13	12	simpli 489	. . . . . 6 ⊢ ℚ ∈ (SubRing‘ℂfld)
14	12	simpri 491	. . . . . 6 ⊢ (ℂfld ↾s ℚ) ∈ DivRing
15		issdrg 21072	. . . . . 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 12442	. . . . . . 7 ⊢ 2 ∈ ℂ
20		3cn 12448	. . . . . . . 8 ⊢ 3 ∈ ℂ
21		3ne0 12476	. . . . . . . 8 ⊢ 3 ≠ 0
22	20, 21	reccli 12071	. . . . . . 7 ⊢ (1 / 3) ∈ ℂ
23		cxpcl 27029	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (1 / 3) ∈ ℂ) → (2↑𝑐(1 / 3)) ∈ ℂ)
24	19, 22, 23	mp2an 705	. . . . . 6 ⊢ (2↑𝑐(1 / 3)) ∈ ℂ
25	18, 24	eqeltri 2860	. . . . 5 ⊢ 𝐴 ∈ ℂ
26	25	a1i 11	. . . 4 ⊢ (⊤ → 𝐴 ∈ ℂ)
27		cnfld0 21729	. . . 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 6908	. . . . . . 7 ⊢ ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) − (𝐾‘2)))
32	31	fveq1i 6906	. . . . . 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 21733	. . . . . 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 20392	. . . . . . 7 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
41		2sqr3minply.2	. . . . . . 7 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
42	3	qdrng 27974	. . . . . . . . . . 11 ⊢ 𝑄 ∈ DivRing
43	42	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → 𝑄 ∈ DivRing)
44	43	drngringd 21015	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ Ring)
45	2	ply1ring 22592	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring)
46	44, 45	syl 18	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ Ring)
47	39	ringmgp 20492	. . . . . . . 8 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
48	46, 47	syl 18	. . . . . . 7 ⊢ (⊤ → (mulGrp‘𝑃) ∈ Mnd)
49		3nn0 12648	. . . . . . . 8 ⊢ 3 ∈ ℕ0
50	49	a1i 11	. . . . . . 7 ⊢ (⊤ → 3 ∈ ℕ0)
51		2sqr3minply.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑄)
52	51, 2, 34	vr1cl 22562	. . . . . . . 8 ⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
53	44, 52	syl 18	. . . . . . 7 ⊢ (⊤ → 𝑋 ∈ (Base‘𝑃))
54	40, 41, 48, 50, 53	mulgnn0cld 19331	. . . . . 6 ⊢ (⊤ → (3 ↑ 𝑋) ∈ (Base‘𝑃))
55		2sqr3minply.k	. . . . . . . 8 ⊢ 𝐾 = (algSc‘𝑃)
56	44	mptru 1577	. . . . . . . . 9 ⊢ 𝑄 ∈ Ring
57	2	ply1sca 22597	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑄 = (Scalar‘𝑃))
58	56, 57	ax-mp 5	. . . . . . . 8 ⊢ 𝑄 = (Scalar‘𝑃)
59	2	ply1lmod 22596	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod)
60	44, 59	syl 18	. . . . . . . 8 ⊢ (⊤ → 𝑃 ∈ LMod)
61	3	qrngbas 27973	. . . . . . . 8 ⊢ ℚ = (Base‘𝑄)
62	55, 58, 46, 60, 61, 34	asclf 22216	. . . . . . 7 ⊢ (⊤ → 𝐾:ℚ⟶(Base‘𝑃))
63		2z 12752	. . . . . . . 8 ⊢ 2 ∈ ℤ
64		zq 13105	. . . . . . . 8 ⊢ (2 ∈ ℤ → 2 ∈ ℚ)
65	63, 64	mp1i 14	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℚ)
66	62, 65	ffvelcdmd 7106	. . . . . 6 ⊢ (⊤ → (𝐾‘2) ∈ (Base‘𝑃))
67	1, 6, 2, 3, 34, 35, 36, 37, 38, 54, 66, 26	evls1subd 34171	. . . . 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 22712	. . . . . . . . 9 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)))
70	1, 51, 3, 6, 37, 38	evls1var 22683	. . . . . . . . . . . 12 ⊢ (⊤ → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
71	70	fveq1d 6907	. . . . . . . . . . 11 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = (( I ↾ ℂ)‘𝐴))
72		fvresi 7198	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (( I ↾ ℂ)‘𝐴) = 𝐴)
73	25, 72	mp1i 14	. . . . . . . . . . 11 ⊢ (⊤ → (( I ↾ ℂ)‘𝐴) = 𝐴)
74	71, 73	eqtrd 2798	. . . . . . . . . 10 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴) = 𝐴)
75	74	oveq2d 7456	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝐴)) = (3(.g‘(mulGrp‘ℂfld))𝐴))
76		cnfldexp 21738	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
77	26, 50, 76	syl2anc 596	. . . . . . . . 9 ⊢ (⊤ → (3(.g‘(mulGrp‘ℂfld))𝐴) = (𝐴↑3))
78	69, 75, 77	3eqtrd 2802	. . . . . . . 8 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) = (𝐴↑3))
79	18	oveq1i 7450	. . . . . . . . 9 ⊢ (𝐴↑3) = ((2↑𝑐(1 / 3))↑3)
80		3nn 12446	. . . . . . . . . 10 ⊢ 3 ∈ ℕ
81		cxproot 27045	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ) → ((2↑𝑐(1 / 3))↑3) = 2)
82	19, 80, 81	mp2an 705	. . . . . . . . 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 22711	. . . . . . 7 ⊢ (⊤ → (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴) = 2)
86	84, 85	oveq12d 7458	. . . . . 6 ⊢ (⊤ → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝐴) − (((ℂfld evalSub1 ℚ)‘(𝐾‘2))‘𝐴)) = (2 − 2))
87	19	subidi 11653	. . . . . 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 27975	. . . . 5 ⊢ 0 = (0g‘𝑄)
91		eqid 2763	. . . . 5 ⊢ (eval1‘𝑄) = (eval1‘𝑄)
92		2sqr3minply.d	. . . . 5 ⊢ 𝐷 = (deg1‘𝑄)
93		fldsdrgfld 21082	. . . . . . . 8 ⊢ ((ℂfld ∈ Field ∧ ℚ ∈ (SubDRing‘ℂfld)) → (ℂfld ↾s ℚ) ∈ Field)
94	10, 16, 93	mp2an 705	. . . . . . 7 ⊢ (ℂfld ↾s ℚ) ∈ Field
95	3, 94	eqeltri 2860	. . . . . 6 ⊢ 𝑄 ∈ Field
96	95	a1i 11	. . . . 5 ⊢ (⊤ → 𝑄 ∈ Field)
97	46	ringgrpd 20496	. . . . . . 7 ⊢ (⊤ → 𝑃 ∈ Grp)
98	34, 35	grpsubcl 19256	. . . . . . 7 ⊢ ((𝑃 ∈ Grp ∧ (3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ (𝐾‘2) ∈ (Base‘𝑃)) → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
99	97, 54, 66, 98	syl3anc 1399	. . . . . 6 ⊢ (⊤ → ((3 ↑ 𝑋) − (𝐾‘2)) ∈ (Base‘𝑃))
100	30, 99	eqeltrid 2868	. . . . 5 ⊢ (⊤ → 𝐹 ∈ (Base‘𝑃))
101	96	fldcrngd 21022	. . . . . . . . 9 ⊢ (⊤ → 𝑄 ∈ CRing)
102	91, 2, 34, 101, 61, 100	evl1fvf 34162	. . . . . . . 8 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹):ℚ⟶ℚ)
103	102	ffnd 6729	. . . . . . 7 ⊢ (⊤ → ((eval1‘𝑄)‘𝐹) Fn ℚ)
104		fniniseg2 7082	. . . . . . 7 ⊢ (((eval1‘𝑄)‘𝐹) Fn ℚ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
105	103, 104	syl 18	. . . . . 6 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0})
106		cnfldmul 21713	. . . . . . . . . . . . . . 15 ⊢ · = (.r‘ℂfld)
107	3, 106	ressmulr 17504	. . . . . . . . . . . . . 14 ⊢ (ℚ ∈ (SubRing‘ℂfld) → · = (.r‘𝑄))
108	13, 107	ax-mp 5	. . . . . . . . . . . . 13 ⊢ · = (.r‘𝑄)
109		cnfldadd 21711	. . . . . . . . . . . . . . 15 ⊢ + = (+g‘ℂfld)
110	3, 109	ressplusg 17488	. . . . . . . . . . . . . 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 6908	. . . . . . . . . . . . . . . . . 18 ⊢ (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2)))
115	114	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (coe1‘𝐹) = (coe1‘((3 ↑ 𝑋) − (𝐾‘2))))
116	30	fveq2i 6908	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2)))
117	116	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘𝐹) = (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))))
118		3pos 12475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 < 3
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 < 3)
120		2ne0 12473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 0
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 2 ≠ 0)
122	92, 2, 61, 55, 90	deg1scl 26458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0) → (𝐷‘(𝐾‘2)) = 0)
123	44, 65, 121, 122	syl3anc 1399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(𝐾‘2)) = 0)
124		drngnzr 21029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ NzRing)
125	42, 124	mp1i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → 𝑄 ∈ NzRing)
126	92, 2, 51, 39, 41	deg1pw 26466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ NzRing ∧ 3 ∈ ℕ0) → (𝐷‘(3 ↑ 𝑋)) = 3)
127	125, 50, 126	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝐷‘(3 ↑ 𝑋)) = 3)
128	119, 123, 127	3brtr4d 5140	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐷‘(𝐾‘2)) < (𝐷‘(3 ↑ 𝑋)))
129	2, 92, 44, 34, 35, 54, 66, 128	deg1sub 26453	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (𝐷‘((3 ↑ 𝑋) − (𝐾‘2))) = (𝐷‘(3 ↑ 𝑋)))
130	117, 129, 127	3eqtrd 2802	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝐷‘𝐹) = 3)
131	115, 130	fveq12d 6912	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3))
132		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (-g‘𝑄) = (-g‘𝑄)
133	2, 34, 35, 132	coe1subfv 22612	. . . . . . . . . . . . . . . . 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 1401	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘3) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
135		subrgsubg 20856	. . . . . . . . . . . . . . . . . . 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 22557	. . . . . . . . . . . . . . . . . . 19 ⊢ (((3 ↑ 𝑋) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
139	54, 50, 138	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) ∈ ℚ)
140		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (coe1‘(𝐾‘2)) = (coe1‘(𝐾‘2))
141	140, 34, 2, 61	coe1fvalcl 22557	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐾‘2) ∈ (Base‘𝑃) ∧ 3 ∈ ℕ0) → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
142	66, 50, 141	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) ∈ ℚ)
143	36, 3, 132	subgsub 19375	. . . . . . . . . . . . . . . . . 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 1399	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (((coe1‘(3 ↑ 𝑋))‘3)(-g‘𝑄)((coe1‘(𝐾‘2))‘3)))
145		iftrue 4491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 3, 1, 0) = 1)
146	3	qrng1 27976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 = (1r‘𝑄)
147	2, 51, 41, 44, 50, 90, 146	coe1mon 34186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(3 ↑ 𝑋)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 3, 1, 0)))
148		1cnd 11326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 1 ∈ ℂ)
149	145, 147, 50, 148	fvmptd4 7038	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘3) = 1)
150	21	neii 2961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ¬ 3 = 0
151		eqeq1 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 3 → (𝑖 = 0 ↔ 3 = 0))
152	150, 151	mtbiri 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 3 → ¬ 𝑖 = 0)
153	152	iffalsed 4496	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 3 → if(𝑖 = 0, 2, 0) = 0)
154	2, 55, 61, 90	coe1scl 22633	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑄 ∈ Ring ∧ 2 ∈ ℚ) → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
155	44, 65, 154	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (coe1‘(𝐾‘2)) = (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, 2, 0)))
156		0nn0 12645	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℕ0
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 0 ∈ ℕ0)
158	153, 155, 50, 157	fvmptd4 7038	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘3) = 0)
159	149, 158	oveq12d 7458	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (((coe1‘(3 ↑ 𝑋))‘3) − ((coe1‘(𝐾‘2))‘3)) = (1 − 0))
160		1m0e1 12486	. . . . . . . . . . . . . . . . . 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 6909	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘(𝐷‘𝐹)) = ((coe1‘𝐹)‘3))
165	163, 164	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 = ((coe1‘𝐹)‘3))
166	165	mptru 1577	. . . . . . . . . . . . 13 ⊢ 1 = ((coe1‘𝐹)‘3)
167	115	fveq1d 6907	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘2) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2))
168		2nn0 12647	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
169	168	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 2 ∈ ℕ0)
170	2, 34, 35, 132	coe1subfv 22612	. . . . . . . . . . . . . . . . 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 1401	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘2) = (((coe1‘(3 ↑ 𝑋))‘2)(-g‘𝑄)((coe1‘(𝐾‘2))‘2)))
172		2re 12441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
173		2lt3 12540	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < 3
174	172, 173	ltneii 11447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ≠ 3
175		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 3 ↔ 2 ≠ 3))
176	174, 175	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 3)
177	176	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑖 = 2) → 𝑖 ≠ 3)
178	177	neneqd 2964	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 3)
179	178	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 3, 1, 0) = 0)
180	147, 179, 169, 157	fvmptd 7021	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘2) = 0)
181		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 2 → (𝑖 ≠ 0 ↔ 2 ≠ 0))
182	120, 181	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 2 → 𝑖 ≠ 0)
183	182	neneqd 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 2 → ¬ 𝑖 = 0)
184	183	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 2) → ¬ 𝑖 = 0)
185	184	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 2) → if(𝑖 = 0, 2, 0) = 0)
186	155, 185, 169, 157	fvmptd 7021	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘2) = 0)
187	180, 186	oveq12d 7458	. . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 0 ∈ ℚ)
190	36, 3, 132	subgsub 19375	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ) → (0 − 0) = (0(-g‘𝑄)0))
191	136, 189, 189, 190	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (0 − 0) = (0(-g‘𝑄)0))
192		0m0e0 12485	. . . . . . . . . . . . . . . 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 6907	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘1) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1))
197		1nn0 12646	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℕ0
198	197	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → 1 ∈ ℕ0)
199	2, 34, 35, 132	coe1subfv 22612	. . . . . . . . . . . . . . . . 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 1401	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘1) = (((coe1‘(3 ↑ 𝑋))‘1)(-g‘𝑄)((coe1‘(𝐾‘2))‘1)))
201		1re 11332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
202		1lt3 12542	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 3
203	201, 202	ltneii 11447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 3
204		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 3 ↔ 1 ≠ 3))
205	203, 204	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 3)
206	205	neneqd 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 3)
207	206	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 3)
208	207	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 3, 1, 0) = 0)
209	147, 208, 198, 157	fvmptd 7021	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘1) = 0)
210		ax-1ne0 11293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
211		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 1 → (𝑖 ≠ 0 ↔ 1 ≠ 0))
212	210, 211	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 1 → 𝑖 ≠ 0)
213	212	neneqd 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 1 → ¬ 𝑖 = 0)
214	213	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 1) → ¬ 𝑖 = 0)
215	214	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 1) → if(𝑖 = 0, 2, 0) = 0)
216	155, 215, 198, 157	fvmptd 7021	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘1) = 0)
217	209, 216	oveq12d 7458	. . . . . . . . . . . . . . . 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 6907	. . . . . . . . . . . . . . 15 ⊢ (⊤ → ((coe1‘𝐹)‘0) = ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0))
222	2, 34, 35, 132	coe1subfv 22612	. . . . . . . . . . . . . . . . 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 1401	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((coe1‘((3 ↑ 𝑋) − (𝐾‘2)))‘0) = (((coe1‘(3 ↑ 𝑋))‘0)(-g‘𝑄)((coe1‘(𝐾‘2))‘0)))
224	21	necomi 3013	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≠ 3
225		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 = 0 → (𝑖 ≠ 3 ↔ 0 ≠ 3))
226	224, 225	mpbiri 261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 0 → 𝑖 ≠ 3)
227	226	neneqd 2964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 0 → ¬ 𝑖 = 3)
228	227	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → ¬ 𝑖 = 3)
229	228	iffalsed 4496	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 3, 1, 0) = 0)
230	147, 229, 157, 157	fvmptd 7021	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(3 ↑ 𝑋))‘0) = 0)
231		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑖 = 0) → 𝑖 = 0)
232	231	iftrued 4493	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑖 = 0) → if(𝑖 = 0, 2, 0) = 2)
233	155, 232, 157, 169	fvmptd 7021	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → ((coe1‘(𝐾‘2))‘0) = 2)
234	230, 233	oveq12d 7458	. . . . . . . . . . . . . . . 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 11568	. . . . . . . . . . . . . . . 16 ⊢ -2 = (0 − 2)
237	36, 3, 132	subgsub 19375	. . . . . . . . . . . . . . . . 17 ⊢ ((ℚ ∈ (SubGrp‘ℂfld) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ) → (0 − 2) = (0(-g‘𝑄)2))
238	136, 189, 65, 237	syl3anc 1399	. . . . . . . . . . . . . . . 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 21022	. . . . . . . . . . . . 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 34177	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)))
250		qsscn 13111	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ ℂ
251		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = ((mulGrp‘ℂfld) ↾s ℚ)
252		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
253	252, 6	mgpbas 20392	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ = (Base‘(mulGrp‘ℂfld))
254	251, 253	ressbas2 17442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℚ ⊆ ℂ → ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ)))
255	250, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℚ = (Base‘((mulGrp‘ℂfld) ↾s ℚ))
256	3, 252	mgpress 20397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld ∈ DivRing ∧ ℚ ∈ (SubRing‘ℂfld)) → ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄))
257	7, 13, 256	mp2an 705	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((mulGrp‘ℂfld) ↾s ℚ) = (mulGrp‘𝑄)
258	257	fveq2i 6908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘((mulGrp‘ℂfld) ↾s ℚ)) = (Base‘(mulGrp‘𝑄))
259	255, 258	eqtri 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
260		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
261	260	ringmgp 20492	. . . . . . . . . . . . . . . . . . . 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 19331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
265	250, 264	sselid 3911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
266	265	mullidd 11351	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (3(.g‘(mulGrp‘𝑄))𝑥))
267	257	eqcomi 2772	. . . . . . . . . . . . . . . . 17 ⊢ (mulGrp‘𝑄) = ((mulGrp‘ℂfld) ↾s ℚ)
268	250, 253	sseqtri 3961	. . . . . . . . . . . . . . . . . 18 ⊢ ℚ ⊆ (Base‘(mulGrp‘ℂfld))
269	268	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → ℚ ⊆ (Base‘(mulGrp‘ℂfld)))
270	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 3 ∈ ℕ)
271	267, 269, 248, 270	ressmulgnnd 19314	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘𝑄))𝑥) = (3(.g‘(mulGrp‘ℂfld))𝑥))
272		qcn 13114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
273		cnfldexp 21738	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
274	272, 263, 273	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (3(.g‘(mulGrp‘ℂfld))𝑥) = (𝑥↑3))
275	266, 271, 274	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (1 · (3(.g‘(mulGrp‘𝑄))𝑥)) = (𝑥↑3))
276	168	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℕ0)
277	259, 112, 262, 276, 248	mulgnn0cld 19331	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℚ)
278	250, 277	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (2(.g‘(mulGrp‘𝑄))𝑥) ∈ ℂ)
279	278	mul02d 11532	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · (2(.g‘(mulGrp‘𝑄))𝑥)) = 0)
280	275, 279	oveq12d 7458	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = ((𝑥↑3) + 0))
281	272, 263	expcld 14313	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑3) ∈ ℂ)
282	281	addridd 11534	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + 0) = (𝑥↑3))
283	280, 282	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) = (𝑥↑3))
284	272	mul02d 11532	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (0 · 𝑥) = 0)
285	284	oveq1d 7455	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = (0 + -2))
286	19	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → 2 ∈ ℂ)
287	286	negcld 11680	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → -2 ∈ ℂ)
288	287	addlidd 11535	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℚ → (0 + -2) = -2)
289	285, 288	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℚ → ((0 · 𝑥) + -2) = -2)
290	283, 289	oveq12d 7458	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → (((1 · (3(.g‘(mulGrp‘𝑄))𝑥)) + (0 · (2(.g‘(mulGrp‘𝑄))𝑥))) + ((0 · 𝑥) + -2)) = ((𝑥↑3) + -2))
291	281, 286	negsubd 11699	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) + -2) = ((𝑥↑3) − 2))
292	249, 290, 291	3eqtrd 2802	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) = ((𝑥↑3) − 2))
293		2prm 16893	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℙ
294		3z 12753	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℤ
295		3re 12447	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℝ
296	172, 295, 173	ltleii 11457	. . . . . . . . . . . . . . . 16 ⊢ 2 ≤ 3
297	63	eluz1i 12997	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ (ℤ≥‘2) ↔ (3 ∈ ℤ ∧ 2 ≤ 3))
298	294, 296, 297	mpbir2an 724	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ (ℤ≥‘2)
299		rtprmirr 27115	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℙ ∧ 3 ∈ (ℤ≥‘2)) → (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ))
300	293, 298, 299	mp2an 705	. . . . . . . . . . . . . 14 ⊢ (2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ)
301		eldifn 4071	. . . . . . . . . . . . . 14 ⊢ ((2↑𝑐(1 / 3)) ∈ (ℝ ∖ ℚ) → ¬ (2↑𝑐(1 / 3)) ∈ ℚ)
302	300, 301	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ (2↑𝑐(1 / 3)) ∈ ℚ
303		nelne2 3057	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ¬ (2↑𝑐(1 / 3)) ∈ ℚ) → 𝑥 ≠ (2↑𝑐(1 / 3)))
304	302, 303	mpan2 704	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℚ → 𝑥 ≠ (2↑𝑐(1 / 3)))
305		qre 13104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
306	305	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 𝑥 ∈ ℝ)
307		2pos 12471	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
308	281, 286	subeq0ad 11701	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℚ → (((𝑥↑3) − 2) = 0 ↔ (𝑥↑3) = 2))
309	308	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑3) = 2)
310	307, 309	breqtrrid 5146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < (𝑥↑3))
311	80	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 3 ∈ ℕ)
312		n2dvds3 16567	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ 2 ∥ 3
313	312	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ¬ 2 ∥ 3)
314	306, 311, 313	expgt0b 33475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (0 < 𝑥 ↔ 0 < (𝑥↑3)))
315	310, 314	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → 0 < 𝑥)
316	306, 315	elrpd 13185	. . . . . . . . . . . . . . 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 27092	. . . . . . . . . . . . . 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 12112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℚ → (3 · (1 / 3)) = 1)
323	322	oveq2d 7456	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = (𝑥↑𝑐1))
324	272	cxp1d 27061	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐1) = 𝑥)
325	323, 324	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
326	325	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → (𝑥↑𝑐(3 · (1 / 3))) = 𝑥)
327		cxpexp 27023	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑥↑𝑐3) = (𝑥↑3))
328	272, 263, 327	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℚ → (𝑥↑𝑐3) = (𝑥↑3))
329	328	oveq1d 7455	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℚ → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
330	329	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑𝑐3)↑𝑐(1 / 3)) = ((𝑥↑3)↑𝑐(1 / 3)))
331	319, 326, 330	3eqtr3rd 2807	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℚ ∧ ((𝑥↑3) − 2) = 0) → ((𝑥↑3)↑𝑐(1 / 3)) = 𝑥)
332	309	oveq1d 7455	. . . . . . . . . . . . 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 3050	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℚ → ((𝑥↑3) − 2) ≠ 0)
335	292, 334	eqnetrd 3026	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℚ → (((eval1‘𝑄)‘𝐹)‘𝑥) ≠ 0)
336	335	neneqd 2964	. . . . . . . . 9 ⊢ (𝑥 ∈ ℚ → ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
337	336	rgen 3082	. . . . . . . 8 ⊢ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0
338	337	a1i 11	. . . . . . 7 ⊢ (⊤ → ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
339		rabeq0 4341	. . . . . . 7 ⊢ ({𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅ ↔ ∀𝑥 ∈ ℚ ¬ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0)
340	338, 339	sylibr 237	. . . . . 6 ⊢ (⊤ → {𝑥 ∈ ℚ ∣ (((eval1‘𝑄)‘𝐹)‘𝑥) = 0} = ∅)
341	105, 340	eqtrd 2798	. . . . 5 ⊢ (⊤ → (◡((eval1‘𝑄)‘𝐹) “ {0}) = ∅)
342	90, 91, 92, 2, 34, 96, 100, 341, 130	ply1dg3rt0irred 34183	. . . 4 ⊢ (⊤ → 𝐹 ∈ (Irred‘𝑃))
343		eqid 2763	. . . . . . 7 ⊢ (Irred‘𝑃) = (Irred‘𝑃)
344	343, 29	irredn0 20680	. . . . . 6 ⊢ ((𝑃 ∈ Ring ∧ 𝐹 ∈ (Irred‘𝑃)) → 𝐹 ≠ (0g‘𝑃))
345	46, 342, 344	syl2anc 596	. . . . 5 ⊢ (⊤ → 𝐹 ≠ (0g‘𝑃))
346	3	fveq2i 6908	. . . . . . 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 27976	. . . . . 6 ⊢ 1 = (1r‘(ℂfld ↾s ℚ))
351	5, 34, 29, 347, 348, 350	ismon1p 26488	. . . . 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 34415	. . 3 ⊢ (⊤ → 𝐹 = (𝑀‘𝐴))
354	353, 130	jca 521	. 2 ⊢ (⊤ → (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3))
355	354	mptru 1577	1 ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  {crab 3416   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281  ifcif 4485  {csn 4588   class class class wbr 5106   ↦ cmpt 5189   I cid 5549  ^◡ccnv 5654   ↾ cres 5657   “ cima 5658   Fn wfn 6550  ‘cfv 6555  (class class class)co 7440  ℂcc 11222  ℝcr 11223  0cc0 11224  1c1 11225   + caddc 11227   · cmul 11229   < clt 11367   ≤ cle 11368   − cmin 11565   -cneg 11566   / cdiv 11997  ℕcn 12359  2c2 12421  3c3 12422  ℕ₀cn0 12630  ℤcz 12717  ℤ_≥cuz 12989  ℚcq 13099  ↑cexp 14228   ∥ cdvds 16448  ℙcprime 16872  Basecbs 17413   ↾_s cress 17434  +_gcplusg 17454  ._rcmulr 17455  Scalarcsca 17457  0_gc0g 17636  Mndcmnd 18949  Grpcgrp 19170  -_gcsg 19172  ._gcmg 19303  SubGrpcsubg 19356  mulGrpcmgp 20387  Ringcrg 20486  CRingccrg 20487  Irredcir 20613  NzRingcnzr 20789  SubRingcsubrg 20848  DivRingcdr 21007  Fieldcfield 21008  SubDRingcsdrg 21070  LModclmod 21162  ℂ_fldccnfld 21705  algSccascl 22187  var₁cv1 22521  Poly₁cpl1 22522  coe₁cco1 22523   evalSub₁ ces1 22658  eval₁ce1 22659  deg₁cdg1 26399  Monic_1pcmn1 26471  ↑_𝑐ccxp 26910   minPoly cminply 34398

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-inf2 9666  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301  ax-pre-sup 11302  ax-addf 11303  ax-mulf 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-isom 6564  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-of 7714  df-ofr 7715  df-om 7899  df-1st 8022  df-2nd 8023  df-supp 8202  df-tpos 8268  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-er 8742  df-map 8874  df-pm 8875  df-ixp 8951  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-fsupp 9379  df-fi 9427  df-sup 9458  df-inf 9459  df-oi 9528  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-div 11998  df-nn 12360  df-2 12429  df-3 12430  df-4 12431  df-5 12432  df-6 12433  df-7 12434  df-8 12435  df-9 12436  df-n0 12631  df-z 12718  df-dec 12839  df-uz 12990  df-q 13100  df-rp 13145  df-xneg 13265  df-xadd 13266  df-xmul 13267  df-ioo 13504  df-ioc 13505  df-ico 13506  df-icc 13507  df-fz 13664  df-fzo 13813  df-fl 13956  df-mod 14034  df-seq 14169  df-exp 14229  df-fac 14442  df-bc 14471  df-hash 14499  df-shft 15246  df-cj 15292  df-re 15293  df-im 15294  df-sqrt 15428  df-abs 15429  df-limsup 15664  df-clim 15681  df-rlim 15682  df-sum 15880  df-ef 16259  df-sin 16261  df-cos 16262  df-pi 16264  df-dvds 16449  df-gcd 16691  df-prm 16873  df-numer 16937  df-denom 16938  df-struct 17351  df-sets 17368  df-slot 17386  df-ndx 17398  df-base 17414  df-ress 17435  df-plusg 17467  df-mulr 17468  df-starv 17469  df-sca 17470  df-vsca 17471  df-ip 17472  df-tset 17473  df-ple 17474  df-ds 17476  df-unif 17477  df-hom 17478  df-cco 17479  df-rest 17619  df-topn 17620  df-0g 17638  df-gsum 17639  df-topgen 17640  df-pt 17641  df-prds 17644  df-pws 17646  df-xrs 17700  df-qtop 17705  df-imas 17706  df-xps 17708  df-mre 17782  df-mrc 17783  df-acs 17785  df-mgm 18842  df-sgrp 18934  df-mnd 18950  df-mhm 19004  df-submnd 19005  df-grp 19173  df-minusg 19174  df-sbg 19175  df-mulg 19304  df-subg 19359  df-ghm 19454  df-cntz 19558  df-cmn 20023  df-abl 20024  df-mgp 20388  df-rng 20402  df-ur 20435  df-srg 20440  df-ring 20488  df-cring 20489  df-oppr 20594  df-dvdsr 20614  df-unit 20615  df-irred 20616  df-invr 20645  df-dvr 20658  df-rhm 20729  df-nzr 20790  df-subrng 20825  df-subrg 20849  df-rlreg 20973  df-domn 20974  df-idom 20975  df-drng 21009  df-field 21010  df-sdrg 21071  df-lmod 21164  df-lss 21234  df-lsp 21274  df-sra 21475  df-rgmod 21476  df-lidl 21513  df-rsp 21514  df-psmet 21697  df-xmet 21698  df-met 21699  df-bl 21700  df-mopn 21701  df-fbas 21702  df-fg 21703  df-cnfld 21706  df-assa 22188  df-asp 22189  df-ascl 22190  df-psr 22244  df-mvr 22245  df-mpl 22246  df-opsr 22248  df-evls 22410  df-evl 22411  df-psr1 22525  df-vr1 22526  df-ply1 22527  df-coe1 22528  df-evls1 22660  df-evl1 22661  df-top 23239  df-topon 23256  df-topsp 23278  df-bases 23291  df-cld 23364  df-ntr 23365  df-cls 23366  df-nei 23443  df-lp 23481  df-perf 23482  df-cn 23572  df-cnp 23573  df-haus 23660  df-tx 23908  df-hmeo 24101  df-fil 24192  df-fm 24284  df-flim 24285  df-flf 24286  df-xms 24666  df-ms 24667  df-tms 24668  df-cncf 25226  df-limc 26213  df-dv 26214  df-mdeg 26400  df-deg1 26401  df-mon1 26476  df-uc1p 26477  df-q1p 26478  df-r1p 26479  df-ig1p 26480  df-log 26911  df-cxp 26912  df-irng 34383  df-minply 34399

This theorem is used by:  2sqr3nconstr  34480