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 6 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 7 13 syl 
 |-  ( ph -> R e. Ring )
15 1 mplring 
 |-  ( ( ( I \ J ) e. _V /\ R e. Ring ) -> U e. Ring )
16 12 14 15 syl2anc 
 |-  ( ph -> U e. Ring )
17 16 adantr 
 |-  ( ( ph /\ x e. J ) -> U e. Ring )
18 simpr 
 |-  ( ( ph /\ x e. J ) -> x e. J )
19 2 9 4 11 17 18 mvrcl 
 |-  ( ( ph /\ x e. J ) -> ( ( J mVar U ) ` x ) e. E )
20 19 adantlr 
 |-  ( ( ( ph /\ x e. I ) /\ x e. J ) -> ( ( J mVar U ) ` x ) e. E )
21 eqid 
 |-  ( Base ` U ) = ( Base ` U )
22 2 4 21 3 10 16 mplasclf 
 |-  ( ph -> C : ( Base ` U ) --> E )
23 22 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> C : ( Base ` U ) --> E )
24 eqid 
 |-  ( ( I \ J ) mVar R ) = ( ( I \ J ) mVar R )
25 12 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( I \ J ) e. _V )
26 14 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> R e. Ring )
27 eldif 
 |-  ( x e. ( I \ J ) <-> ( x e. I /\ -. x e. J ) )
28 27 biimpri 
 |-  ( ( x e. I /\ -. x e. J ) -> x e. ( I \ J ) )
29 28 adantll 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> x e. ( I \ J ) )
30 1 24 21 25 26 29 mvrcl 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( ( ( I \ J ) mVar R ) ` x ) e. ( Base ` U ) )
31 23 30 ffvelrnd 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) e. E )
32 20 31 ifclda 
 |-  ( ( ph /\ x e. I ) -> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) e. E )
33 32 5 fmptd 
 |-  ( ph -> F : I --> E )
34 fvexd 
 |-  ( ph -> ( Base ` T ) e. _V )
35 4 34 eqeltrid 
 |-  ( ph -> E e. _V )
36 35 6 elmapd 
 |-  ( ph -> ( F e. ( E ^m I ) <-> F : I --> E ) )
37 33 36 mpbird 
 |-  ( ph -> F e. ( E ^m I ) )