Metamath Proof Explorer

Theorem mvrcl

Description: A power series variable is a polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mvrcl.s 
|- P = ( I mPoly R )
mvrcl.v 
|- V = ( I mVar R )
mvrcl.b 
|- B = ( Base ` P )
mvrcl.i 
|- ( ph -> I e. W )
mvrcl.r 
|- ( ph -> R e. Ring )
mvrcl.x 
|- ( ph -> X e. I )
Assertion mvrcl 
|- ( ph -> ( V ` X ) e. B )

Proof

Step Hyp Ref Expression
1 mvrcl.s 
 |-  P = ( I mPoly R )
2 mvrcl.v 
 |-  V = ( I mVar R )
3 mvrcl.b 
 |-  B = ( Base ` P )
4 mvrcl.i 
 |-  ( ph -> I e. W )
5 mvrcl.r 
 |-  ( ph -> R e. Ring )
6 mvrcl.x 
 |-  ( ph -> X e. I )
7 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
8 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
9 7 2 8 4 5 6 mvrcl2 
 |-  ( ph -> ( V ` X ) e. ( Base ` ( I mPwSer R ) ) )
10 fvexd 
 |-  ( ph -> ( V ` X ) e. _V )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
13 7 11 12 8 9 psrelbas 
 |-  ( ph -> ( V ` X ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
14 13 ffund 
 |-  ( ph -> Fun ( V ` X ) )
15 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
16 snfi 
 |-  { ( y e. I |-> if ( y = X , 1 , 0 ) ) } e. Fin
17 16 a1i 
 |-  ( ph -> { ( y e. I |-> if ( y = X , 1 , 0 ) ) } e. Fin )
18 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 4 adantr 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> I e. W )
21 5 adantr 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> R e. Ring )
22 6 adantr 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> X e. I )
23 simpr 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) )
24 eldifsn 
 |-  ( x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) <-> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ x =/= ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
25 23 24 sylib 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> ( x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } /\ x =/= ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
26 25 simpld 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> x e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } )
27 2 12 18 19 20 21 22 26 mvrval2 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> ( ( V ` X ) ` x ) = if ( x = ( y e. I |-> if ( y = X , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
28 25 simprd 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> x =/= ( y e. I |-> if ( y = X , 1 , 0 ) ) )
29 28 neneqd 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> -. x = ( y e. I |-> if ( y = X , 1 , 0 ) ) )
30 29 iffalsed 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> if ( x = ( y e. I |-> if ( y = X , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
31 27 30 eqtrd 
 |-  ( ( ph /\ x e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> ( ( V ` X ) ` x ) = ( 0g ` R ) )
32 13 31 suppss 
 |-  ( ph -> ( ( V ` X ) supp ( 0g ` R ) ) C_ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } )
33 suppssfifsupp 
 |-  ( ( ( ( V ` X ) e. _V /\ Fun ( V ` X ) /\ ( 0g ` R ) e. _V ) /\ ( { ( y e. I |-> if ( y = X , 1 , 0 ) ) } e. Fin /\ ( ( V ` X ) supp ( 0g ` R ) ) C_ { ( y e. I |-> if ( y = X , 1 , 0 ) ) } ) ) -> ( V ` X ) finSupp ( 0g ` R ) )
34 10 14 15 17 32 33 syl32anc 
 |-  ( ph -> ( V ` X ) finSupp ( 0g ` R ) )
35 1 7 8 18 3 mplelbas 
 |-  ( ( V ` X ) e. B <-> ( ( V ` X ) e. ( Base ` ( I mPwSer R ) ) /\ ( V ` X ) finSupp ( 0g ` R ) ) )
36 9 34 35 sylanbrc 
 |-  ( ph -> ( V ` X ) e. B )