Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( ( 0 ... 𝑁 ) mPoly 𝐾 )
prjcrv0.0 ⊢ 0 = ( 0g ‘ 𝑌 )
prjcrv0.p ⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
prjcrv0.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
prjcrv0.k ⊢ ( 𝜑 → 𝐾 ∈ Field )
Assertion prjcrv0 ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 0 ) = 𝑃 )

Proof

Step Hyp Ref Expression
1 prjcrv0.y ⊢ 𝑌 = ( ( 0 ... 𝑁 ) mPoly 𝐾 )
2 prjcrv0.0 ⊢ 0 = ( 0g ‘ 𝑌 )
3 prjcrv0.p ⊢ 𝑃 = ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 )
4 prjcrv0.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 prjcrv0.k ⊢ ( 𝜑 → 𝐾 ∈ Field )
6 eqid ⊢ ( ( 0 ... 𝑁 ) mHomP 𝐾 ) = ( ( 0 ... 𝑁 ) mHomP 𝐾 )
7 eqid ⊢ ( ( 0 ... 𝑁 ) eval 𝐾 ) = ( ( 0 ... 𝑁 ) eval 𝐾 )
8 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
9 fvssunirn ⊢ ( ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ‘ 𝑁 ) ⊆ ∪ ran ( ( 0 ... 𝑁 ) mHomP 𝐾 )
10 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
12 5 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
13 12 crnggrpd ⊢ ( 𝜑 → 𝐾 ∈ Grp )
14 1 10 8 2 11 13 mpl0 ⊢ ( 𝜑 → 0 = ( { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝐾 ) } ) )
15 6 8 10 11 13 4 mhp0cl ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝐾 ) } ) ∈ ( ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ‘ 𝑁 ) )
16 14 15 eqeltrd ⊢ ( 𝜑 → 0 ∈ ( ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ‘ 𝑁 ) )
17 9 16 sselid ⊢ ( 𝜑 → 0 ∈ ∪ ran ( ( 0 ... 𝑁 ) mHomP 𝐾 ) )
18 6 7 3 8 4 5 17 prjcrvval ⊢ ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 0 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } } )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 0 ... 𝑁 ) ∈ V )
21 12 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ∈ CRing )
22 7 19 1 8 2 20 21 evl0 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) = ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) )
23 22 imaeq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) )
24 eqid ⊢ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
25 eqid ⊢ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) = ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } )
26 5 flddrngd ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
27 3 24 25 4 26 prjspnssbas ⊢ ( 𝜑 → 𝑃 ⊆ 𝒫 ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) )
28 eqid ⊢ { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) }
29 24 19 8 28 frlmbas ⊢ ( ( 𝐾 ∈ Field ∧ ( 0 ... 𝑁 ) ∈ V ) → { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
30 5 11 29 syl2anc ⊢ ( 𝜑 → { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
31 ssrab2 ⊢ { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) )
32 30 31 eqsstrrdi ⊢ ( 𝜑 → ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
33 32 ssdifssd ⊢ ( 𝜑 → ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
34 33 sspwd ⊢ ( 𝜑 → 𝒫 ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ⊆ 𝒫 ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
35 27 34 sstrd ⊢ ( 𝜑 → 𝑃 ⊆ 𝒫 ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
36 35 sselda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝒫 ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
37 36 elpwid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
38 sseqin2 ⊢ ( 𝑝 ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ↔ ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) = 𝑝 )
39 37 38 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) = 𝑝 )
40 4 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑁 ∈ ℕ0 )
41 26 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ∈ DivRing )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
43 3 24 25 40 41 42 prjspnn0 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ≠ ∅ )
44 39 43 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ )
45 xpima2 ⊢ ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ → ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
46 44 45 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
47 23 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
48 47 rabeqcda ⊢ ( 𝜑 → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } } = 𝑃 )
49 18 48 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 0 ) = 𝑃 )