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

Metamath Proof Explorer

Theorem selvcllem5

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

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

Proof

Step Hyp Ref Expression
1 selvcllem5.u 
 |-  U = ( ( I \ J ) mPoly R )
2 selvcllem5.t 
 |-  T = ( J mPoly U )
3 selvcllem5.c 
 |-  C = ( algSc ` T )
4 selvcllem5.e 
 |-  E = ( Base ` T )
5 selvcllem5.f 
 |-  F = ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) )
6 selvcllem5.i 
 |-  ( ph -> I e. V )
7 selvcllem5.r 
 |-  ( ph -> R e. CRing )
8 selvcllem5.j 
 |-  ( ph -> J C_ I )
9 4 fvexi 
 |-  E e. _V
10 9 a1i 
 |-  ( ph -> E e. _V )
11 eqid 
 |-  ( J mVar U ) = ( J mVar U )
12 6 8 ssexd 
 |-  ( ph -> J e. _V )
13 12 adantr 
 |-  ( ( ph /\ x e. J ) -> J e. _V )
14 6 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
15 7 crngringd 
 |-  ( ph -> R e. Ring )
16 1 14 15 mplringd 
 |-  ( 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 11 4 13 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 12 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 14 ad2antrr 
 |-  ( ( ( ph /\ x e. I ) /\ -. x e. J ) -> ( I \ J ) e. _V )
26 15 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 ffvelcdmd 
 |-  ( ( ( 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 10 6 33 elmapdd 
 |-  ( ph -> F e. ( E ^m I ) )