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

Metamath Proof Explorer

Theorem evl1sca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1sca.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1sca.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
evl1sca.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evl1sca.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion evl1sca ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 evl1sca.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2 evl1sca.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 evl1sca.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 evl1sca.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
7 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 2 4 3 7 ply1sclf ⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
9 6 8 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) )
10 ffvelcdm ⊢ ( ( 𝐴 : 𝐵 ⟶ ( Base ‘ 𝑃 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
11 9 10 sylancom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
12 eqid ⊢ ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
13 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
14 2 7 ply1bas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
15 1 12 3 13 14 evl1val ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
16 11 15 syldan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
17 2 4 ply1ascl ⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
18 3 ressid ⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
19 18 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
20 19 oveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 1o mPoly 𝑅 ) )
21 20 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly 𝑅 ) ) )
22 17 21 eqtr4id ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐴 = ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) )
23 22 fveq1d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑋 ) )
24 23 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) )
25 12 3 evlval ⊢ ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
26 eqid ⊢ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 1o mPoly ( 𝑅 ↾s 𝐵 ) )
27 eqid ⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
28 eqid ⊢ ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) )
29 1on ⊢ 1o ∈ On
30 29 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 1o ∈ On )
31 simpl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ CRing )
32 3 subrgid ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
33 6 32 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
34 simpr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
35 25 26 27 3 28 30 31 33 34 evlssca ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
36 24 35 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) )
37 36 coeq1d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 1o eval 𝑅 ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
38 df1o2 ⊢ 1o = { ∅ }
39 3 fvexi ⊢ 𝐵 ∈ V
40 0ex ⊢ ∅ ∈ V
41 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) )
42 38 39 40 41 mapsnf1o3 ⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o )
43 f1of ⊢ ( ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
44 42 43 mp1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
45 41 fmpt ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) ↔ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
46 44 45 sylibr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 1o × { 𝑦 } ) ∈ ( 𝐵 ↑m 1o ) )
47 eqidd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) )
48 fconstmpt ⊢ ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑥 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 )
49 48 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) = ( 𝑥 ∈ ( 𝐵 ↑m 1o ) ↦ 𝑋 ) )
50 eqidd ⊢ ( 𝑥 = ( 1o × { 𝑦 } ) → 𝑋 = 𝑋 )
51 46 47 49 50 fmptcof ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 ) )
52 fconstmpt ⊢ ( 𝐵 × { 𝑋 } ) = ( 𝑦 ∈ 𝐵 ↦ 𝑋 )
53 51 52 eqtr4di ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑋 } ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝐵 × { 𝑋 } ) )
54 16 37 53 3eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )