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		funmpt	$⊢ Fun (n \in ℕ_{0} ⟼ \{f \in {Base}_{Y} \| f supp 0_{K} \subseteq \{g \in \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = n\}\})$
10		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
11		eqid	$⊢ \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\}$
12		ovexd	$⊢ φ \to (0 \dots N) \in V$
13	6 1 10 8 11 12 5	mhpfval	$⊢ φ \to (0 \dots N) mHomP K = (n \in ℕ_{0} ⟼ \{f \in {Base}_{Y} \| f supp 0_{K} \subseteq \{g \in \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = n\}\})$
14	13	funeqd	$⊢ φ \to (Fun ((0 \dots N) mHomP K) \leftrightarrow Fun (n \in ℕ_{0} ⟼ \{f \in {Base}_{Y} \| f supp 0_{K} \subseteq \{g \in \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = n\}\}))$
15	9 14	mpbiri	$⊢ φ \to Fun ((0 \dots N) mHomP K)$
16	5	fldcrngd	$⊢ φ \to K \in CRing$
17	16	crnggrpd	$⊢ φ \to K \in Grp$
18	1 11 8 2 12 17	mpl0	$⊢ φ \to \underset{˙}{0} = \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{K}\}$
19		0nn0	$⊢ 0 \in ℕ_{0}$
20	19	a1i	$⊢ φ \to 0 \in ℕ_{0}$
21	6 8 11 12 17 20	mhp0cl	$⊢ φ \to \{h \in ({ℕ_{0}}^{(0 \dots N)}) \| h^{-1} [ℕ] \in Fin\} \times \{0_{K}\} \in ((0 \dots N) mHomP K) (0)$
22	18 21	eqeltrd	$⊢ φ \to \underset{˙}{0} \in ((0 \dots N) mHomP K) (0)$
23		elunirn2	$⊢ (Fun ((0 \dots N) mHomP K) \land \underset{˙}{0} \in ((0 \dots N) mHomP K) (0)) \to \underset{˙}{0} \in ⋃ ran ((0 \dots N) mHomP K)$
24	15 22 23	syl2anc	$⊢ φ \to \underset{˙}{0} \in ⋃ ran ((0 \dots N) mHomP K)$
25	6 7 3 8 4 5 24	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 \|-
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27		ovexd	$⊢ (φ \land p \in P) \to (0 \dots N) \in V$
28	16	adantr	$⊢ (φ \land p \in P) \to K \in CRing$
29	7 26 1 8 2 27 28	evl0	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) = ({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}$
30	29	imaeq1d	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) [p] = (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p]$
31	3	eleq2i	$⊢ p \in P \leftrightarrow p \in (N {ℙ𝕣𝕠𝕛}_{n} K)$
32	31	biimpi	$⊢ p \in P \to p \in (N {ℙ𝕣𝕠𝕛}_{n} K)$
33	32	adantl	$⊢ (φ \land p \in P) \to p \in (N {ℙ𝕣𝕠𝕛}_{n} K)$
34	4	adantr	$⊢ (φ \land p \in P) \to N \in ℕ_{0}$
35		isfld	$⊢ K \in Field \leftrightarrow (K \in DivRing \land K \in CRing)$
36	35	simplbi	$⊢ K \in Field \to K \in DivRing$
37	5 36	syl	$⊢ φ \to K \in DivRing$
38	37	adantr	$⊢ (φ \land p \in P) \to K \in DivRing$
39		prjspnval	$⊢ (N \in ℕ_{0} \land K \in DivRing) \to N {ℙ𝕣𝕠𝕛}_{n} K = ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N))$
40	34 38 39	syl2anc	$⊢ (φ \land p \in P) \to N {ℙ𝕣𝕠𝕛}_{n} K = ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N))$
41		eqid	$⊢ K freeLMod (0 \dots N) = K freeLMod (0 \dots N)$
42	41	frlmlvec	$⊢ (K \in DivRing \land (0 \dots N) \in V) \to K freeLMod (0 \dots N) \in LVec$
43	37 12 42	syl2anc	$⊢ φ \to K freeLMod (0 \dots N) \in LVec$
44	43	adantr	$⊢ (φ \land p \in P) \to K freeLMod (0 \dots N) \in LVec$
45		eqid	$⊢ 0_{(K freeLMod (0 \dots N))} = 0_{(K freeLMod (0 \dots N))}$
46		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))}\}$
47		eqid	$⊢ LSpan (K freeLMod (0 \dots N)) = LSpan (K freeLMod (0 \dots N))$
48	45 46 47	prjspval2	$⊢ K freeLMod (0 \dots N) \in LVec \to ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N)) = ⋃_{a \in {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}} \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}$
49	44 48	syl	$⊢ (φ \land p \in P) \to ℙ𝕣𝕠𝕛 (K freeLMod (0 \dots N)) = ⋃_{a \in {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}} \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}$
50	40 49	eqtrd	$⊢ (φ \land p \in P) \to N {ℙ𝕣𝕠𝕛}_{n} K = ⋃_{a \in {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}} \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}$
51	33 50	eleqtrd	$⊢ (φ \land p \in P) \to p \in ⋃_{a \in {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}} \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}$
52		eliun	$⊢ p \in ⋃_{a \in {Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}} \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\} \leftrightarrow \exists a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}$
53	51 52	sylib	$⊢ (φ \land p \in P) \to \exists a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}$
54		eqid	$⊢ \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\}$
55	41 26 8 54	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))}$
56	5 12 55	syl2anc	$⊢ φ \to \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} = {Base}_{(K freeLMod (0 \dots N))}$
57		ssrab2	$⊢ \{k \in ({Base}_{K}^{(0 \dots N)}) \| {finSupp}_{0_{K}} (k)\} \subseteq {Base}_{K}^{(0 \dots N)}$
58	56 57	eqsstrrdi	$⊢ φ \to {Base}_{(K freeLMod (0 \dots N))} \subseteq {Base}_{K}^{(0 \dots N)}$
59	58	ad2antrr	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\})) \to {Base}_{(K freeLMod (0 \dots N))} \subseteq {Base}_{K}^{(0 \dots N)}$
60		eldifi	$⊢ a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \to a \in {Base}_{(K freeLMod (0 \dots N))}$
61	60	adantl	$⊢ ((φ \land p \in P) \land a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to a \in {Base}_{(K freeLMod (0 \dots N))}$
62	61	adantrr	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\})) \to a \in {Base}_{(K freeLMod (0 \dots N))}$
63	59 62	sseldd	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\})) \to a \in ({Base}_{K}^{(0 \dots N)})$
64		velsn	$⊢ p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\} \leftrightarrow p = LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}$
65	64	anbi2i	$⊢ (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\}) \leftrightarrow (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p = LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\})$
66	43	lveclmodd	$⊢ φ \to K freeLMod (0 \dots N) \in LMod$
67	66	ad2antrr	$⊢ ((φ \land p \in P) \land a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to K freeLMod (0 \dots N) \in LMod$
68		eqid	$⊢ {Base}_{(K freeLMod (0 \dots N))} = {Base}_{(K freeLMod (0 \dots N))}$
69	68 47	lspsnid	$⊢ (K freeLMod (0 \dots N) \in LMod \land a \in {Base}_{(K freeLMod (0 \dots N))}) \to a \in LSpan (K freeLMod (0 \dots N)) (\{a\})$
70	67 61 69	syl2anc	$⊢ ((φ \land p \in P) \land a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to a \in LSpan (K freeLMod (0 \dots N)) (\{a\})$
71		eldifn	$⊢ a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \to \neg a \in \{0_{(K freeLMod (0 \dots N))}\}$
72	71	adantl	$⊢ ((φ \land p \in P) \land a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to \neg a \in \{0_{(K freeLMod (0 \dots N))}\}$
73	70 72	eldifd	$⊢ ((φ \land p \in P) \land a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to a \in (LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\})$
74		eleq2	$⊢ p = LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\} \to (a \in p \leftrightarrow a \in (LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}))$
75	73 74	syl5ibrcom	$⊢ ((φ \land p \in P) \land a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to (p = LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\} \to a \in p)$
76	75	impr	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p = LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\})) \to a \in p$
77	65 76	sylan2b	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\})) \to a \in p$
78	63 77	elind	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\})) \to a \in (({Base}_{K}^{(0 \dots N)}) \cap p)$
79	78	ne0d	$⊢ ((φ \land p \in P) \land (a \in ({Base}_{(K freeLMod (0 \dots N))} ∖ \{0_{(K freeLMod (0 \dots N))}\}) \land p \in \{LSpan (K freeLMod (0 \dots N)) (\{a\}) ∖ \{0_{(K freeLMod (0 \dots N))}\}\})) \to ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset$
80	53 79	rexlimddv	$⊢ (φ \land p \in P) \to ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset$
81		xpima2	$⊢ ({Base}_{K}^{(0 \dots N)}) \cap p \neq \emptyset \to (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p] = \{0_{K}\}$
82	80 81	syl	$⊢ (φ \land p \in P) \to (({Base}_{K}^{(0 \dots N)}) \times \{0_{K}\}) [p] = \{0_{K}\}$
83	30 82	eqtrd	$⊢ (φ \land p \in P) \to ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}$
84	83	rabeqcda	$⊢ φ \to \{p \in P \| ((0 \dots N) eval K) (\underset{˙}{0}) [p] = \{0_{K}\}\} = P$
85	25 84	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