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	Could not format assertion : No typesetting found for \|- ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) with typecode \|-

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	Could not format ( ph -> ( ( N PrjCrv K ) ` .0. ) = { p e. P \| ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } ) : No typesetting found for \|- ( ph -> ( ( N PrjCrv K ) ` .0. ) = { p e. P \| ( ( ( ( 0 ... N ) eval K ) ` .0. ) " p ) = { ( 0g ` K ) } } ) with typecode \|-
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	5	flddrngd	$⊢ φ \to K \in DivRing$
27	3 24 25 4 26	prjspnssbas	$⊢ φ \to P \subseteq 𝒫 ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})$
28		eqid	$⊢ \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\}$
29	24 19 8 28	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))}$
30	5 11 29	syl2anc	$⊢ φ \to \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = {Base}_{(K freeLMod (0 \dots N))}$
31		ssrab2	$⊢ \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} \subseteq {Base}_{K}^{(0 \dots N)}$
32	30 31	eqsstrrdi	$⊢ φ \to {Base}_{(K freeLMod (0 \dots N))} \subseteq {Base}_{K}^{(0 \dots N)}$
33	32	ssdifssd	$⊢ φ \to {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\} \subseteq {Base}_{K}^{(0 \dots N)}$
34	33	sspwd	$⊢ φ \to 𝒫 ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \subseteq 𝒫 ({Base}_{K}^{(0 \dots N)})$
35	27 34	sstrd	$⊢ φ \to P \subseteq 𝒫 ({Base}_{K}^{(0 \dots N)})$
36	35	sselda	$⊢ (φ \land p \in P) \to p \in 𝒫 ({Base}_{K}^{(0 \dots N)})$
37	36	elpwid	$⊢ (φ \land p \in P) \to p \subseteq {Base}_{K}^{(0 \dots N)}$
38		sseqin2	$⊢ p \subseteq {Base}_{K}^{(0 \dots N)} \leftrightarrow ({Base}_{K}^{(0 \dots N)}) \cap p = p$
39	37 38	sylib	$⊢ (φ \land p \in P) \to ({Base}_{K}^{(0 \dots N)}) \cap p = p$
40	4	adantr	$⊢ (φ \land p \in P) \to N \in ℕ_{0}$
41	26	adantr	$⊢ (φ \land p \in P) \to K \in DivRing$
42		simpr	$⊢ (φ \land p \in P) \to p \in P$
43	3 24 25 40 41 42	prjspnn0	$⊢ (φ \land p \in P) \to p \neq \emptyset$
44	39 43	eqnetrd	$⊢ (φ \land p \in P) \to ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset$
45		xpima2	$⊢ ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset \to (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p] = \{0_{K}\}$
46	44 45	syl	$⊢ (φ \land p \in P) \to (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p] = \{0_{K}\}$
47	23 46	eqtrd	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}$
48	47	rabeqcda	$⊢ φ \to \{p \in P \| ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}\} = P$
49	18 48	eqtrd	Could not format ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) : No typesetting found for \|- ( ph -> ( ( N PrjCrv K ) ` .0. ) = P ) with typecode \|-

Metamath Proof Explorer

Theorem prjcrv0

Proof