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

Metamath Proof Explorer

Definition df-evls

Description: Define the evaluation map for the polynomial algebra. The function ( ( I evalSub S )R ) : V --> ( S ^m ( S ^m I ) ) makes sense when I is an index set, S is a ring, R is a subring of S , and where V is the set of polynomials in ( I mPoly R ) . This function maps an element of the formal polynomial algebra (with coefficients in R ) to a function from assignments I --> S of the variables to elements of S formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015)

Ref Expression
Assertion df-evls evalSub = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ces ⊢ evalSub
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 ccrg ⊢ CRing
5 cbs ⊢ Base
6 3 cv ⊢ 𝑠
7 6 5 cfv ⊢ ( Base ‘ 𝑠 )
8 vb ⊢ 𝑏
9 vr ⊢ 𝑟
10 csubrg ⊢ SubRing
11 6 10 cfv ⊢ ( SubRing ‘ 𝑠 )
12 1 cv ⊢ 𝑖
13 cmpl ⊢ mPoly
14 cress ⊢ ↾s
15 9 cv ⊢ 𝑟
16 6 15 14 co ⊢ ( 𝑠 ↾s 𝑟 )
17 12 16 13 co ⊢ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) )
18 vw ⊢ 𝑤
19 vf ⊢ 𝑓
20 18 cv ⊢ 𝑤
21 crh ⊢ RingHom
22 cpws ⊢ ↑s
23 8 cv ⊢ 𝑏
24 cmap ⊢ ↑m
25 23 12 24 co ⊢ ( 𝑏 ↑m 𝑖 )
26 6 25 22 co ⊢ ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) )
27 20 26 21 co ⊢ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) )
28 19 cv ⊢ 𝑓
29 cascl ⊢ algSc
30 20 29 cfv ⊢ ( algSc ‘ 𝑤 )
31 28 30 ccom ⊢ ( 𝑓 ∘ ( algSc ‘ 𝑤 ) )
32 vx ⊢ 𝑥
33 32 cv ⊢ 𝑥
34 33 csn ⊢ { 𝑥 }
35 25 34 cxp ⊢ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } )
36 32 15 35 cmpt ⊢ ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) )
37 31 36 wceq ⊢ ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) )
38 cmvr ⊢ mVar
39 12 16 38 co ⊢ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) )
40 28 39 ccom ⊢ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) )
41 vg ⊢ 𝑔
42 41 cv ⊢ 𝑔
43 33 42 cfv ⊢ ( 𝑔 ‘ 𝑥 )
44 41 25 43 cmpt ⊢ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) )
45 32 12 44 cmpt ⊢ ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
46 40 45 wceq ⊢ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
47 37 46 wa ⊢ ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) )
48 47 19 27 crio ⊢ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
49 18 17 48 csb ⊢ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
50 9 11 49 cmpt ⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
51 8 7 50 csb ⊢ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
52 1 3 2 4 51 cmpo ⊢ ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
53 0 52 wceq ⊢ evalSub = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )