This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressply1evl

Description: Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025)

Ref Expression
Hypotheses ressply1evl2.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
ressply1evl2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
ressply1evl2.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
ressply1evl2.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
ressply1evl2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
ressply1evl.e ⊢ 𝐸 = ( eval1 ‘ 𝑆 )
ressply1evl.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
ressply1evl.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion ressply1evl ( 𝜑 → 𝑄 = ( 𝐸 ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ressply1evl2.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 ressply1evl2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 ressply1evl2.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 ressply1evl2.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 ressply1evl2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
6 ressply1evl.e ⊢ 𝐸 = ( eval1 ‘ 𝑆 )
7 ressply1evl.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
8 ressply1evl.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9 6 2 evl1fval1 ⊢ 𝐸 = ( 𝑆 evalSub1 𝐾 )
10 eqid ⊢ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) = ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) )
11 eqid ⊢ ( 𝑆 ↾s 𝐾 ) = ( 𝑆 ↾s 𝐾 )
12 eqid ⊢ ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑆 ∈ CRing )
14 7 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
15 2 subrgid ⊢ ( 𝑆 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
16 14 15 syl ⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
18 eqid ⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
19 eqid ⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
20 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
21 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
22 18 4 3 5 8 19 20 21 ressply1bas2 ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
23 inss2 ⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
24 22 23 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
25 2 ressid ⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐾 ) = 𝑆 )
26 7 25 syl ⊢ ( 𝜑 → ( 𝑆 ↾s 𝐾 ) = 𝑆 )
27 26 fveq2d ⊢ ( 𝜑 → ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) = ( Poly1 ‘ 𝑆 ) )
28 27 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
29 24 28 sseqtrrd ⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) )
30 29 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑚 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) )
31 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
32 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑆 ) ) = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
33 eqid ⊢ ( coe1 ‘ 𝑚 ) = ( coe1 ‘ 𝑚 )
34 9 2 10 11 12 13 17 30 31 32 33 evls1fpws ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → ( 𝐸 ‘ 𝑚 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑚 ) ‘ 𝑘 ) ( .r ‘ 𝑆 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑥 ) ) ) ) ) )
35 8 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑚 ∈ 𝐵 )
37 1 2 3 4 5 13 35 36 31 32 33 evls1fpws ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → ( 𝑄 ‘ 𝑚 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑚 ) ‘ 𝑘 ) ( .r ‘ 𝑆 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑥 ) ) ) ) ) )
38 34 37 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) )
39 38 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐵 ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) )
40 eqid ⊢ ( 𝑆 ↑s 𝐾 ) = ( 𝑆 ↑s 𝐾 )
41 6 18 40 2 evl1rhm ⊢ ( 𝑆 ∈ CRing → 𝐸 ∈ ( ( Poly1 ‘ 𝑆 ) RingHom ( 𝑆 ↑s 𝐾 ) ) )
42 eqid ⊢ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑆 ↑s 𝐾 ) )
43 21 42 rhmf ⊢ ( 𝐸 ∈ ( ( Poly1 ‘ 𝑆 ) RingHom ( 𝑆 ↑s 𝐾 ) ) → 𝐸 : ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
44 7 41 43 3syl ⊢ ( 𝜑 → 𝐸 : ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
45 44 ffnd ⊢ ( 𝜑 → 𝐸 Fn ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
46 1 2 40 4 3 evls1rhm ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
47 7 8 46 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
48 5 42 rhmf ⊢ ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
49 47 48 syl ⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
50 49 ffnd ⊢ ( 𝜑 → 𝑄 Fn 𝐵 )
51 fvreseq1 ⊢ ( ( ( 𝐸 Fn ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ 𝑄 Fn 𝐵 ) ∧ 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) → ( ( 𝐸 ↾ 𝐵 ) = 𝑄 ↔ ∀ 𝑚 ∈ 𝐵 ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) ) )
52 45 50 24 51 syl21anc ⊢ ( 𝜑 → ( ( 𝐸 ↾ 𝐵 ) = 𝑄 ↔ ∀ 𝑚 ∈ 𝐵 ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) ) )
53 39 52 mpbird ⊢ ( 𝜑 → ( 𝐸 ↾ 𝐵 ) = 𝑄 )
54 53 eqcomd ⊢ ( 𝜑 → 𝑄 = ( 𝐸 ↾ 𝐵 ) )