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 funmpt ⊢ Fun ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ 𝑌 ) ∣ ( 𝑓 supp ( 0g ‘ 𝐾 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } )
10 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
12 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
13 6 1 10 8 11 12 5 mhpfval ⊢ ( 𝜑 → ( ( 0 ... 𝑁 ) mHomP 𝐾 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ 𝑌 ) ∣ ( 𝑓 supp ( 0g ‘ 𝐾 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
14 13 funeqd ⊢ ( 𝜑 → ( Fun ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ↔ Fun ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ 𝑌 ) ∣ ( 𝑓 supp ( 0g ‘ 𝐾 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) ) )
15 9 14 mpbiri ⊢ ( 𝜑 → Fun ( ( 0 ... 𝑁 ) mHomP 𝐾 ) )
16 5 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
17 16 crnggrpd ⊢ ( 𝜑 → 𝐾 ∈ Grp )
18 1 11 8 2 12 17 mpl0 ⊢ ( 𝜑 → 0 = ( { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝐾 ) } ) )
19 0nn0 ⊢ 0 ∈ ℕ0
20 19 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
21 6 8 11 12 17 20 mhp0cl ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝑁 ) ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝐾 ) } ) ∈ ( ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ‘ 0 ) )
22 18 21 eqeltrd ⊢ ( 𝜑 → 0 ∈ ( ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ‘ 0 ) )
23 elunirn2 ⊢ ( ( Fun ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ∧ 0 ∈ ( ( ( 0 ... 𝑁 ) mHomP 𝐾 ) ‘ 0 ) ) → 0 ∈ ∪ ran ( ( 0 ... 𝑁 ) mHomP 𝐾 ) )
24 15 22 23 syl2anc ⊢ ( 𝜑 → 0 ∈ ∪ ran ( ( 0 ... 𝑁 ) mHomP 𝐾 ) )
25 6 7 3 8 4 5 24 prjcrvval ⊢ ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 0 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } } )
26 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
27 ovexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 0 ... 𝑁 ) ∈ V )
28 16 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ∈ CRing )
29 7 26 1 8 2 27 28 evl0 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) = ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) )
30 29 imaeq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) )
31 3 eleq2i ⊢ ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) )
32 31 biimpi ⊢ ( 𝑝 ∈ 𝑃 → 𝑝 ∈ ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) )
34 4 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑁 ∈ ℕ0 )
35 isfld ⊢ ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
36 35 simplbi ⊢ ( 𝐾 ∈ Field → 𝐾 ∈ DivRing )
37 5 36 syl ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ∈ DivRing )
39 prjspnval ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ DivRing ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
40 34 38 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
41 eqid ⊢ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
42 41 frlmlvec ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LVec )
43 37 12 42 syl2anc ⊢ ( 𝜑 → ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LVec )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LVec )
45 eqid ⊢ ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) )
46 eqid ⊢ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) = ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } )
47 eqid ⊢ ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) )
48 45 46 47 prjspval2 ⊢ ( ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LVec → ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ∪ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } )
49 44 48 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ℙ𝕣𝕠𝕛 ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ∪ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } )
50 40 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑁 ℙ𝕣𝕠𝕛n 𝐾 ) = ∪ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } )
51 33 50 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ ∪ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } )
52 eliun ⊢ ( 𝑝 ∈ ∪ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } )
53 51 52 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ∃ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } )
54 eqid ⊢ { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) }
55 41 26 8 54 frlmbas ⊢ ( ( 𝐾 ∈ Field ∧ ( 0 ... 𝑁 ) ∈ V ) → { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
56 5 12 55 syl2anc ⊢ ( 𝜑 → { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
57 ssrab2 ⊢ { 𝑘 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∣ 𝑘 finSupp ( 0g ‘ 𝐾 ) } ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) )
58 56 57 eqsstrrdi ⊢ ( 𝜑 → ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ) → ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ⊆ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
60 eldifi ⊢ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) → 𝑎 ∈ ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
61 60 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) → 𝑎 ∈ ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
62 61 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ) → 𝑎 ∈ ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) )
63 59 62 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ) → 𝑎 ∈ ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) )
64 velsn ⊢ ( 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ↔ 𝑝 = ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) )
65 64 anbi2i ⊢ ( ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ↔ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 = ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) )
66 43 lveclmodd ⊢ ( 𝜑 → ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LMod )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) → ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LMod )
68 eqid ⊢ ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) = ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) )
69 68 47 lspsnid ⊢ ( ( ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ∈ LMod ∧ 𝑎 ∈ ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ) → 𝑎 ∈ ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) )
70 67 61 69 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) → 𝑎 ∈ ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) )
71 eldifn ⊢ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) → ¬ 𝑎 ∈ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) → ¬ 𝑎 ∈ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } )
73 70 72 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) → 𝑎 ∈ ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) )
74 eleq2 ⊢ ( 𝑝 = ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) → ( 𝑎 ∈ 𝑝 ↔ 𝑎 ∈ ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) )
75 73 74 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) → ( 𝑝 = ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) → 𝑎 ∈ 𝑝 ) )
76 75 impr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 = ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ) ) → 𝑎 ∈ 𝑝 )
77 65 76 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ) → 𝑎 ∈ 𝑝 )
78 63 77 elind ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ) → 𝑎 ∈ ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) )
79 78 ne0d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( ( Base ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) ∧ 𝑝 ∈ { ( ( ( LSpan ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) ‘ { 𝑎 } ) ∖ { ( 0g ‘ ( 𝐾 freeLMod ( 0 ... 𝑁 ) ) ) } ) } ) ) → ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ )
80 53 79 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ )
81 xpima2 ⊢ ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) ∩ 𝑝 ) ≠ ∅ → ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
82 80 81 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( Base ‘ 𝐾 ) ↑m ( 0 ... 𝑁 ) ) × { ( 0g ‘ 𝐾 ) } ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
83 30 82 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } )
84 83 rabeqcda ⊢ ( 𝜑 → { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 0 ... 𝑁 ) eval 𝐾 ) ‘ 0 ) “ 𝑝 ) = { ( 0g ‘ 𝐾 ) } } = 𝑃 )
85 25 84 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ℙ𝕣𝕠𝕛Crv 𝐾 ) ‘ 0 ) = 𝑃 )