Metamath Proof Explorer

Theorem mplmon

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

Ref Expression
Hypotheses mplmon.s 
|- P = ( I mPoly R )
mplmon.b 
|- B = ( Base ` P )
mplmon.z 
|- .0. = ( 0g ` R )
mplmon.o 
|- .1. = ( 1r ` R )
mplmon.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplmon.i 
|- ( ph -> I e. W )
mplmon.r 
|- ( ph -> R e. Ring )
mplmon.x 
|- ( ph -> X e. D )
Assertion mplmon 
|- ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B )

Proof

Step Hyp Ref Expression
1 mplmon.s 
 |-  P = ( I mPoly R )
2 mplmon.b 
 |-  B = ( Base ` P )
3 mplmon.z 
 |-  .0. = ( 0g ` R )
4 mplmon.o 
 |-  .1. = ( 1r ` R )
5 mplmon.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
6 mplmon.i 
 |-  ( ph -> I e. W )
7 mplmon.r 
 |-  ( ph -> R e. Ring )
8 mplmon.x 
 |-  ( ph -> X e. D )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 9 4 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
11 9 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
12 10 11 ifcld 
 |-  ( R e. Ring -> if ( y = X , .1. , .0. ) e. ( Base ` R ) )
13 7 12 syl 
 |-  ( ph -> if ( y = X , .1. , .0. ) e. ( Base ` R ) )
14 13 adantr 
 |-  ( ( ph /\ y e. D ) -> if ( y = X , .1. , .0. ) e. ( Base ` R ) )
15 14 fmpttd 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
16 fvex 
 |-  ( Base ` R ) e. _V
17 ovex 
 |-  ( NN0 ^m I ) e. _V
18 5 17 rabex2 
 |-  D e. _V
19 16 18 elmap 
 |-  ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( ( Base ` R ) ^m D ) <-> ( y e. D |-> if ( y = X , .1. , .0. ) ) : D --> ( Base ` R ) )
20 15 19 sylibr 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( ( Base ` R ) ^m D ) )
21 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
22 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
23 21 9 5 22 6 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( ( Base ` R ) ^m D ) )
24 20 23 eleqtrrd 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( Base ` ( I mPwSer R ) ) )
25 18 mptex 
 |-  ( y e. D |-> if ( y = X , .1. , .0. ) ) e. _V
26 funmpt 
 |-  Fun ( y e. D |-> if ( y = X , .1. , .0. ) )
27 3 fvexi 
 |-  .0. e. _V
28 25 26 27 3pm3.2i 
 |-  ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. _V /\ Fun ( y e. D |-> if ( y = X , .1. , .0. ) ) /\ .0. e. _V )
29 28 a1i 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. _V /\ Fun ( y e. D |-> if ( y = X , .1. , .0. ) ) /\ .0. e. _V ) )
30 snfi 
 |-  { X } e. Fin
31 30 a1i 
 |-  ( ph -> { X } e. Fin )
32 eldifsni 
 |-  ( y e. ( D \ { X } ) -> y =/= X )
33 32 adantl 
 |-  ( ( ph /\ y e. ( D \ { X } ) ) -> y =/= X )
34 33 neneqd 
 |-  ( ( ph /\ y e. ( D \ { X } ) ) -> -. y = X )
35 34 iffalsed 
 |-  ( ( ph /\ y e. ( D \ { X } ) ) -> if ( y = X , .1. , .0. ) = .0. )
36 18 a1i 
 |-  ( ph -> D e. _V )
37 35 36 suppss2 
 |-  ( ph -> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) supp .0. ) C_ { X } )
38 suppssfifsupp 
 |-  ( ( ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. _V /\ Fun ( y e. D |-> if ( y = X , .1. , .0. ) ) /\ .0. e. _V ) /\ ( { X } e. Fin /\ ( ( y e. D |-> if ( y = X , .1. , .0. ) ) supp .0. ) C_ { X } ) ) -> ( y e. D |-> if ( y = X , .1. , .0. ) ) finSupp .0. )
39 29 31 37 38 syl12anc 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) finSupp .0. )
40 1 21 22 3 2 mplelbas 
 |-  ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B <-> ( ( y e. D |-> if ( y = X , .1. , .0. ) ) e. ( Base ` ( I mPwSer R ) ) /\ ( y e. D |-> if ( y = X , .1. , .0. ) ) finSupp .0. ) )
41 24 39 40 sylanbrc 
 |-  ( ph -> ( y e. D |-> if ( y = X , .1. , .0. ) ) e. B )