Metamath Proof Explorer

Theorem evlsval2

Description: Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlsval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsval.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
evlsval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
evlsval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evlsval.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
evlsval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
evlsval.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
evlsval.x ⊢ 𝑋 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
evlsval.y ⊢ 𝑌 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
Assertion evlsval2 ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) ∧ ( ( 𝑄 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑄 ∘ 𝑉 ) = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 evlsval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsval.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3 evlsval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
4 evlsval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evlsval.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
6 evlsval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
7 evlsval.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
8 evlsval.x ⊢ 𝑋 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
9 evlsval.y ⊢ 𝑌 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
10 1 2 3 4 5 6 7 8 9 evlsval ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ℩ 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) ) )
11 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
12 simp1 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐼 ∈ 𝑍 )
13 4 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
14 13 3adant1 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
15 simp2 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑆 ∈ CRing )
16 ovex ⊢ ( 𝐵 ↑m 𝐼 ) ∈ V
17 5 pwscrng ⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐵 ↑m 𝐼 ) ∈ V ) → 𝑇 ∈ CRing )
18 15 16 17 sylancl ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑇 ∈ CRing )
19 6 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
20 19 3ad2ant3 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ⊆ 𝐵 )
21 20 resmptd ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) )
22 21 8 eqtr4di ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) = 𝑋 )
23 crngring ⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
24 23 3ad2ant2 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑆 ∈ Ring )
25 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
26 5 6 25 pwsdiagrhm ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐵 ↑m 𝐼 ) ∈ V ) → ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) )
27 24 16 26 sylancl ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) )
28 simp3 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
29 4 resrhm ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ∈ ( 𝑈 RingHom 𝑇 ) )
30 27 28 29 syl2anc ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) ↾ 𝑅 ) ∈ ( 𝑈 RingHom 𝑇 ) )
31 22 30 eqeltrrd ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑋 ∈ ( 𝑈 RingHom 𝑇 ) )
32 6 fvexi ⊢ 𝐵 ∈ V
33 simpl1 ⊢ ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑍 )
34 elmapg ⊢ ( ( 𝐵 ∈ V ∧ 𝐼 ∈ 𝑍 ) → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑔 : 𝐼 ⟶ 𝐵 ) )
35 32 33 34 sylancr ⊢ ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑔 : 𝐼 ⟶ 𝐵 ) )
36 35 biimpa ⊢ ( ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑔 : 𝐼 ⟶ 𝐵 )
37 simplr ⊢ ( ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑥 ∈ 𝐼 )
38 36 37 ffvelcdmd ⊢ ( ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
39 38 fmpttd ⊢ ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) : ( 𝐵 ↑m 𝐼 ) ⟶ 𝐵 )
40 simpl2 ⊢ ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ CRing )
41 5 6 11 pwselbasb ⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐵 ↑m 𝐼 ) ∈ V ) → ( ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ↔ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) : ( 𝐵 ↑m 𝐼 ) ⟶ 𝐵 ) )
42 40 16 41 sylancl ⊢ ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) ↔ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) : ( 𝐵 ↑m 𝐼 ) ⟶ 𝐵 ) )
43 39 42 mpbird ⊢ ( ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝑇 ) )
44 43 9 fmptd ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑌 : 𝐼 ⟶ ( Base ‘ 𝑇 ) )
45 2 11 7 3 12 14 18 31 44 evlseu ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ∃! 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) )
46 riotacl2 ⊢ ( ∃! 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) → ( ℩ 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) ) ∈ { 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ∣ ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) } )
47 45 46 syl ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ℩ 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) ) ∈ { 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ∣ ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) } )
48 10 47 eqeltrd ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ { 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ∣ ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) } )
49 coeq1 ⊢ ( 𝑚 = 𝑄 → ( 𝑚 ∘ 𝐴 ) = ( 𝑄 ∘ 𝐴 ) )
50 49 eqeq1d ⊢ ( 𝑚 = 𝑄 → ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ↔ ( 𝑄 ∘ 𝐴 ) = 𝑋 ) )
51 coeq1 ⊢ ( 𝑚 = 𝑄 → ( 𝑚 ∘ 𝑉 ) = ( 𝑄 ∘ 𝑉 ) )
52 51 eqeq1d ⊢ ( 𝑚 = 𝑄 → ( ( 𝑚 ∘ 𝑉 ) = 𝑌 ↔ ( 𝑄 ∘ 𝑉 ) = 𝑌 ) )
53 50 52 anbi12d ⊢ ( 𝑚 = 𝑄 → ( ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) ↔ ( ( 𝑄 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑄 ∘ 𝑉 ) = 𝑌 ) ) )
54 53 elrab ⊢ ( 𝑄 ∈ { 𝑚 ∈ ( 𝑊 RingHom 𝑇 ) ∣ ( ( 𝑚 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑚 ∘ 𝑉 ) = 𝑌 ) } ↔ ( 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) ∧ ( ( 𝑄 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑄 ∘ 𝑉 ) = 𝑌 ) ) )
55 48 54 sylib ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ∈ ( 𝑊 RingHom 𝑇 ) ∧ ( ( 𝑄 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑄 ∘ 𝑉 ) = 𝑌 ) ) )