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 ⊢ 𝑃 = ( 𝑁 ℙrojn 𝐾 )
prjcrv0.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
prjcrv0.k ⊢ ( 𝜑 → 𝐾 ∈ Field )
Assertion prjcrv0 ( 𝜑 → ( ( 𝑁 ℙrojCrv 𝐾 ) ‘ 0 ) = 𝑃 )

Proof

Step Hyp Ref Expression
1 prjcrv0.y ⊢ 𝑌 = ( ( 0 ... 𝑁 ) mPoly 𝐾 )
2 prjcrv0.0 ⊢ 0 = ( 0g ‘ 𝑌 )
3 prjcrv0.p ⊢ 𝑃 = ( 𝑁 ℙrojn 𝐾 )
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 ⊢ ( 𝜑 → ( ( 𝑁 ℙrojCrv 𝐾 ) ‘ 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 4 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑁 ∈ ℕ0 )
27 5 flddrngd ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ∈ DivRing )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
30 3 24 25 26 28 29 elprjspnss ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ⊆ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) )
31 eqid ⊢ { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) }
32 24 19 8 31 frlmbas ⊢ ( ( 𝐾 ∈ Field ∧ ( 0 ... 𝑁 ) ∈ V ) → { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
33 5 11 32 syl2anc ⊢ ( 𝜑 → { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
34 ssrab2 ⊢ { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) )
35 33 34 eqsstrrdi ⊢ ( 𝜑 → ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
36 35 ssdifssd ⊢ ( 𝜑 → ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
38 30 37 sstrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
39 sseqin2 ⊢ ( 𝑝 ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ↔ ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) = 𝑝 )
40 38 39 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) = 𝑝 )
41 3 26 28 29 prjspnn0 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ≠ ∅ )
42 40 41 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ )
43 xpima2 ⊢ ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ → ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
45 23 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
46 45 rabeqcda ⊢ ( 𝜑 → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } } = 𝑃 )
47 18 46 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ℙrojCrv 𝐾 ) ‘ 0 ) = 𝑃 )