Metamath Proof Explorer

Theorem selvval2lem5

Description: The fifth argument passed to evalSub is in the domain (a function I --> E ). (Contributed by SN, 22-Feb-2024)

Ref Expression
Hypotheses selvval2lem5.u 
|- U = ( ( I \ J ) mPoly R )
selvval2lem5.t 
|- T = ( J mPoly U )
selvval2lem5.c 
|- C = ( algSc ` T )
selvval2lem5.e 
|- E = ( Base ` T )
selvval2lem5.f 
|- F = ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) )
selvval2lem5.i 
|- ( ph -> I e. V )
selvval2lem5.r 
|- ( ph -> R e. CRing )
selvval2lem5.j 
|- ( ph -> J C_ I )
Assertion selvval2lem5 
|- ( ph -> F e. ( E ^m I ) )

Proof

Step Hyp Ref Expression
1 selvval2lem5.u 
 |-  U = ( ( I \ J ) mPoly R )
2 selvval2lem5.t 
 |-  T = ( J mPoly U )
3 selvval2lem5.c 
 |-  C = ( algSc ` T )
4 selvval2lem5.e 
 |-  E = ( Base ` T )
5 selvval2lem5.f 
 |-  F = ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) )
6 selvval2lem5.i 
 |-  ( ph -> I e. V )
7 selvval2lem5.r 
 |-  ( ph -> R e. CRing )
8 selvval2lem5.j 
 |-  ( ph -> J C_ I )
9 eqid 
 |-  ( J mVar U ) = ( J mVar U )
10 6 8 ssexd 
 |-  ( ph -> J e. _V )
11 10 adantr 
 |-  ( ( ph /\ x e. J ) -> J e. _V )
12 difexg 
 |-  ( I e. V -> ( I \ J ) e. _V )
13 6 12 syl 
 |-  ( ph -> ( I \ J ) e. _V )
14 crngring 
 |-  ( R e. CRing -> R e. Ring )
15 7 14 syl 
 |-  ( ph -> R e. Ring )
16 1 mplring 
 |-  ( ( ( I \ J ) e. _V /\ R e. Ring ) -> U e. Ring )
17 13 15 16 syl2anc 
 |-  ( ph -> U e. Ring )
18 17 adantr 
 |-  ( ( ph /\ x e. J ) -> U e. Ring )
19 simpr 
 |-  ( ( ph /\ x e. J ) -> x e. J )
20 2 9 4 11 18 19 mvrcl 
 |-  ( ( ph /\ x e. J ) -> ( ( J mVar U ) ` x ) e. E )
21 20 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ x e. J ) -> ( ( J mVar U ) ` x ) e. E )
22 eqid 
 |-  ( Base ` U ) = ( Base ` U )
23 2 4 22 3 10 17 mplasclf 
 |-  ( ph -> C : ( Base ` U ) --> E )
24 23 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> C : ( Base ` U ) --> E )
25 eqid 
 |-  ( ( I \ J ) mVar R ) = ( ( I \ J ) mVar R )
26 13 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( I \ J ) e. _V )
27 15 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> R e. Ring )
28 eldif 
 |-  ( x e. ( I \ J ) <-> ( x e. I /\ -. x e. J ) )
29 28 biimpri 
 |-  ( ( x e. I /\ -. x e. J ) -> x e. ( I \ J ) )
30 29 adantll 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> x e. ( I \ J ) )
31 1 25 22 26 27 30 mvrcl 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( ( ( I \ J ) mVar R ) ` x ) e. ( Base ` U ) )
32 24 31 ffvelrnd 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) e. E )
33 21 32 ifclda 
 |-  ( ( ph /\ x e. I ) -> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) e. E )
34 33 5 fmptd 
 |-  ( ph -> F : I --> E )
35 fvexd 
 |-  ( ph -> ( Base ` T ) e. _V )
36 4 35 eqeltrid 
 |-  ( ph -> E e. _V )
37 36 6 elmapd 
 |-  ( ph -> ( F e. ( E ^m I ) <-> F : I --> E ) )
38 34 37 mpbird 
 |-  ( ph -> F e. ( E ^m I ) )