Theorem mdegle0 24830

Description: A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.)

Hypotheses

Ref	Expression
mdegaddle.y	⊢ 𝑌 = (𝐼 mPoly 𝑅)
mdegaddle.d	⊢ 𝐷 = (𝐼 mDeg 𝑅)
mdegaddle.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
mdegaddle.r	⊢ (𝜑 → 𝑅 ∈ Ring)
mdegle0.b	⊢ 𝐵 = (Base‘𝑌)
mdegle0.a	⊢ 𝐴 = (algSc‘𝑌)
mdegle0.f	⊢ (𝜑 → 𝐹 ∈ 𝐵)

Assertion

Ref	Expression
mdegle0	⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0})))))

Proof of Theorem mdegle0

Dummy variables 𝑥 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mdegle0.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
2		0xr 10767	. . 3 ⊢ 0 ∈ ℝ*
3		mdegaddle.d	. . . 4 ⊢ 𝐷 = (𝐼 mDeg 𝑅)
4		mdegaddle.y	. . . 4 ⊢ 𝑌 = (𝐼 mPoly 𝑅)
5		mdegle0.b	. . . 4 ⊢ 𝐵 = (Base‘𝑌)
6		eqid 2738	. . . 4 ⊢ (0g‘𝑅) = (0g‘𝑅)
7		eqid 2738	. . . 4 ⊢ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}
8		eqid 2738	. . . 4 ⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))
9	3, 4, 5, 6, 7, 8	mdegleb 24817	. . 3 ⊢ ((𝐹 ∈ 𝐵 ∧ 0 ∈ ℝ*) → ((𝐷‘𝐹) ≤ 0 ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅))))
10	1, 2, 9	sylancl 589	. 2 ⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅))))
11	7, 8	tdeglem1 24808	. . . . . . . . . 10 ⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}⟶ℕ0
12	11	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}⟶ℕ0)
13	12	ffvelrnda 6862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0)
14		nn0re 11986	. . . . . . . . 9 ⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℝ)
15		nn0ge0 12002	. . . . . . . . 9 ⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥))
16	14, 15	jca 515	. . . . . . . 8 ⊢ (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℕ0 → (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥)))
17		ne0gt0 10824	. . . . . . . 8 ⊢ ((((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ∈ ℝ ∧ 0 ≤ ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥)) → (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ 0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥)))
18	13, 16, 17	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ 0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥)))
19	7, 8	tdeglem4 24812	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} → (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) = 0 ↔ 𝑥 = (𝐼 × {0})))
20	19	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) = 0 ↔ 𝑥 = (𝐼 × {0})))
21	20	necon3abid 2970	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ≠ 0 ↔ ¬ 𝑥 = (𝐼 × {0})))
22	18, 21	bitr3d 284	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) ↔ ¬ 𝑥 = (𝐼 × {0})))
23	22	imbi1d 345	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
24		eqeq2 2750	. . . . . . . 8 ⊢ ((𝐹‘(𝐼 × {0})) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
25	24	bibi1d 347	. . . . . . 7 ⊢ ((𝐹‘(𝐼 × {0})) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → (((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) ↔ ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))))
26		eqeq2 2750	. . . . . . . 8 ⊢ ((0g‘𝑅) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
27	26	bibi1d 347	. . . . . . 7 ⊢ ((0g‘𝑅) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) → (((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))) ↔ ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))))
28		fveq2 6675	. . . . . . . . 9 ⊢ (𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (𝐹‘(𝐼 × {0})))
29		pm2.24 124	. . . . . . . . 9 ⊢ (𝑥 = (𝐼 × {0}) → (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅)))
30	28, 29	2thd 268	. . . . . . . 8 ⊢ (𝑥 = (𝐼 × {0}) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
31	30	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 = (𝐼 × {0})) → ((𝐹‘𝑥) = (𝐹‘(𝐼 × {0})) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
32		biimt 364	. . . . . . . 8 ⊢ (¬ 𝑥 = (𝐼 × {0}) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
33	32	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑥 = (𝐼 × {0})) → ((𝐹‘𝑥) = (0g‘𝑅) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
34	25, 27, 31, 33	ifbothda 4453	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
35	34	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)) ↔ (¬ 𝑥 = (𝐼 × {0}) → (𝐹‘𝑥) = (0g‘𝑅))))
36	23, 35	bitr4d 285	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
37	36	ralbidva 3108	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
38		eqid 2738	. . . . . . 7 ⊢ (Base‘𝑅) = (Base‘𝑅)
39	4, 38, 5, 7, 1	mplelf 20815	. . . . . 6 ⊢ (𝜑 → 𝐹:{𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}⟶(Base‘𝑅))
40	39	feqmptd 6738	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)))
41		mdegle0.a	. . . . . 6 ⊢ 𝐴 = (algSc‘𝑌)
42		mdegaddle.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
43		mdegaddle.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
44	7	psrbag0 20875	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑉 → (𝐼 × {0}) ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin})
45	42, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐼 × {0}) ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin})
46	39, 45	ffvelrnd 6863	. . . . . 6 ⊢ (𝜑 → (𝐹‘(𝐼 × {0})) ∈ (Base‘𝑅))
47	4, 7, 6, 38, 41, 42, 43, 46	mplascl 20877	. . . . 5 ⊢ (𝜑 → (𝐴‘(𝐹‘(𝐼 × {0}))) = (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
48	40, 47	eqeq12d 2754	. . . 4 ⊢ (𝜑 → (𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))) ↔ (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅)))))
49		fvex 6688	. . . . . 6 ⊢ (𝐹‘𝑥) ∈ V
50	49	rgenw 3065	. . . . 5 ⊢ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) ∈ V
51		mpteqb 6795	. . . . 5 ⊢ (∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) ∈ V → ((𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
52	50, 51	mp1i 13	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (𝐹‘𝑥)) = (𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
53	48, 52	bitrd 282	. . 3 ⊢ (𝜑 → (𝐹 = (𝐴‘(𝐹‘(𝐼 × {0}))) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (𝐹‘𝑥) = if(𝑥 = (𝐼 × {0}), (𝐹‘(𝐼 × {0})), (0g‘𝑅))))
54	37, 53	bitr4d 285	. 2 ⊢ (𝜑 → (∀𝑥 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (0 < ((𝑏 ∈ {𝑎 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦ (ℂfld Σg 𝑏))‘𝑥) → (𝐹‘𝑥) = (0g‘𝑅)) ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0})))))
55	10, 54	bitrd 282	1 ⊢ (𝜑 → ((𝐷‘𝐹) ≤ 0 ↔ 𝐹 = (𝐴‘(𝐹‘(𝐼 × {0})))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2113   ≠ wne 2934  ∀wral 3053  {crab 3057  Vcvv 3398  ifcif 4415  {csn 4517   class class class wbr 5031   ↦ cmpt 5111   × cxp 5524  ^◡ccnv 5525   “ cima 5529  ⟶wf 6336  ‘cfv 6340  (class class class)co 7171   ↑_m cmap 8438  Fincfn 8556  ℝcr 10615  0cc0 10616  ℝ^*cxr 10753   < clt 10754   ≤ cle 10755  ℕcn 11717  ℕ₀cn0 11977  Basecbs 16587  0_gc0g 16817   Σ_g cgsu 16818  Ringcrg 19417  ℂ_fldccnfld 20218  algSccascl 20669   mPoly cmpl 20720   mDeg cmdg 24803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693  ax-pre-sup 10694  ax-addf 10695  ax-mulf 10696

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-se 5485  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-of 7426  df-ofr 7427  df-om 7601  df-1st 7715  df-2nd 7716  df-supp 7858  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-er 8321  df-map 8440  df-pm 8441  df-ixp 8509  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-fsupp 8908  df-sup 8980  df-oi 9048  df-card 9442  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-nn 11718  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784  df-7 11785  df-8 11786  df-9 11787  df-n0 11978  df-z 12064  df-dec 12181  df-uz 12326  df-fz 12983  df-fzo 13126  df-seq 13462  df-hash 13784  df-struct 16589  df-ndx 16590  df-slot 16591  df-base 16593  df-sets 16594  df-ress 16595  df-plusg 16682  df-mulr 16683  df-starv 16684  df-sca 16685  df-vsca 16686  df-tset 16688  df-ple 16689  df-ds 16691  df-unif 16692  df-0g 16819  df-gsum 16820  df-mre 16961  df-mrc 16962  df-acs 16964  df-mgm 17969  df-sgrp 18018  df-mnd 18029  df-mhm 18073  df-submnd 18074  df-grp 18223  df-minusg 18224  df-mulg 18344  df-subg 18395  df-ghm 18475  df-cntz 18566  df-cmn 19027  df-abl 19028  df-mgp 19360  df-ur 19372  df-ring 19419  df-cring 19420  df-subrg 19653  df-cnfld 20219  df-ascl 20672  df-psr 20723  df-mpl 20725  df-mdeg 24805

This theorem is referenced by:  deg1le0  24864