prjcrv0

Description: The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Hypotheses	prjcrv0.y	$⊢ Y = (0 \dots N) mPoly K$
	prjcrv0.0	$⊢ \underset{˙}{0} = 0_{Y}$
	prjcrv0.p	$⊢ P = N {ℙ𝕣𝕠𝕛}_{n} K$
	prjcrv0.n	$⊢ φ \to N \in ℕ_{0}$
	prjcrv0.k	$⊢ φ \to K \in Field$
Assertion	prjcrv0	$⊢ φ \to (N PrjCrv K) (\underset{˙}{0}) = P$

Proof

Step	Hyp	Ref	Expression
1		prjcrv0.y	$⊢ Y = (0 \dots N) mPoly K$
2		prjcrv0.0	$⊢ \underset{˙}{0} = 0_{Y}$
3		prjcrv0.p	$⊢ P = N {ℙ𝕣𝕠𝕛}_{n} K$
4		prjcrv0.n	$⊢ φ \to N \in ℕ_{0}$
5		prjcrv0.k	$⊢ φ \to K \in Field$
6		eqid	$⊢ (0 \dots N) mHomP K = (0 \dots N) mHomP K$
7		eqid	$⊢ (0 \dots N) eval K = (0 \dots N) eval K$
8		eqid	$⊢ 0_{K} = 0_{K}$
9		fvssunirn	$⊢ ((0 \dots N) mHomP K) (N) \subseteq ⋃ ran ((0 \dots N) mHomP K)$
10		eqid	$⊢ \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\}$
11		ovexd	$⊢ φ \to (0 \dots N) \in V$
12	5	fldcrngd	$⊢ φ \to K \in CRing$
13	12	crnggrpd	$⊢ φ \to K \in Grp$
14	1 10 8 2 11 13	mpl0	$⊢ φ \to \underset{˙}{0} = \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{K}\}$
15	6 8 10 11 13 4	mhp0cl	$⊢ φ \to \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{K}\} \in ((0 \dots N) mHomP K) (N)$
16	14 15	eqeltrd	$⊢ φ \to \underset{˙}{0} \in ((0 \dots N) mHomP K) (N)$
17	9 16	sselid	$⊢ φ \to \underset{˙}{0} \in ⋃ ran ((0 \dots N) mHomP K)$
18	6 7 3 8 4 5 17	prjcrvval	$⊢ φ \to (N PrjCrv K) (\underset{˙}{0}) = \{p \in P \| ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}\}$
19		eqid	$⊢ {Base}_{K} = {Base}_{K}$
20		ovexd	$⊢ (φ \land p \in P) \to (0 \dots N) \in V$
21	12	adantr	$⊢ (φ \land p \in P) \to K \in CRing$
22	7 19 1 8 2 20 21	evl0	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) = ({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}$
23	22	imaeq1d	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) [p] = (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p]$
24		eqid	$⊢ K freeLMod (0 \dots N) = K freeLMod (0 \dots N)$
25		eqid	$⊢ {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\} = {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}$
26	4	adantr	$⊢ (φ \land p \in P) \to N \in ℕ_{0}$
27	5	flddrngd	$⊢ φ \to K \in DivRing$
28	27	adantr	$⊢ (φ \land p \in P) \to K \in DivRing$
29		simpr	$⊢ (φ \land p \in P) \to p \in P$
30	3 24 25 26 28 29	elprjspnss	$⊢ (φ \land p \in P) \to p \subseteq {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}$
31		eqid	$⊢ \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\}$
32	24 19 8 31	frlmbas	$⊢ (K \in Field \land (0 \dots N) \in V) \to \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = {Base}_{(K freeLMod (0 \dots N))}$
33	5 11 32	syl2anc	$⊢ φ \to \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = {Base}_{(K freeLMod (0 \dots N))}$
34		ssrab2	$⊢ \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} \subseteq {Base}_{K}^{(0 \dots N)}$
35	33 34	eqsstrrdi	$⊢ φ \to {Base}_{(K freeLMod (0 \dots N))} \subseteq {Base}_{K}^{(0 \dots N)}$
36	35	ssdifssd	$⊢ φ \to {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\} \subseteq {Base}_{K}^{(0 \dots N)}$
37	36	adantr	$⊢ (φ \land p \in P) \to {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\} \subseteq {Base}_{K}^{(0 \dots N)}$
38	30 37	sstrd	$⊢ (φ \land p \in P) \to p \subseteq {Base}_{K}^{(0 \dots N)}$
39		sseqin2	$⊢ p \subseteq {Base}_{K}^{(0 \dots N)} \leftrightarrow ({Base}_{K}^{(0 \dots N)}) \cap p = p$
40	38 39	sylib	$⊢ (φ \land p \in P) \to ({Base}_{K}^{(0 \dots N)}) \cap p = p$
41	3 26 28 29	prjspnn0	$⊢ (φ \land p \in P) \to p \neq \emptyset$
42	40 41	eqnetrd	$⊢ (φ \land p \in P) \to ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset$
43		xpima2	$⊢ ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset \to (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p] = \{0_{K}\}$
44	42 43	syl	$⊢ (φ \land p \in P) \to (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p] = \{0_{K}\}$
45	23 44	eqtrd	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}$
46	45	rabeqcda	$⊢ φ \to \{p \in P \| ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}\} = P$
47	18 46	eqtrd	$⊢ φ \to (N PrjCrv K) (\underset{˙}{0}) = P$

Metamath Proof Explorer

Theorem prjcrv0

Proof