mplmon2

Description: Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mplmon2.p	\|- P = ( I mPoly R )
2		mplmon2.v	\|- .x. = ( .s ` P )
3		mplmon2.d	\|- D = { f e. ( NN0 ^m I ) \| ( `' f " NN ) e. Fin }
4		mplmon2.o	\|- .1. = ( 1r ` R )
5		mplmon2.z	\|- .0. = ( 0g ` R )
6		mplmon2.b	\|- B = ( Base ` R )
7		mplmon2.i	\|- ( ph -> I e. W )
8		mplmon2.r	\|- ( ph -> R e. Ring )
9		mplmon2.k	\|- ( ph -> K e. D )
10		mplmon2.x	\|- ( ph -> X e. B )
11		eqid	\|- ( Base ` P ) = ( Base ` P )
12		eqid	\|- ( .r ` R ) = ( .r ` R )
13	1 11 5 4 3 7 8 9	mplmon	\|- ( ph -> ( y e. D \|-> if ( y = K , .1. , .0. ) ) e. ( Base ` P ) )
14	1 2 6 11 12 3 10 13	mplvsca	\|- ( ph -> ( X .x. ( y e. D \|-> if ( y = K , .1. , .0. ) ) ) = ( ( D X. { X } ) oF ( .r ` R ) ( y e. D \|-> if ( y = K , .1. , .0. ) ) ) )
15		ovex	\|- ( NN0 ^m I ) e. _V
16	3 15	rabex2	\|- D e. _V
17	16	a1i	\|- ( ph -> D e. _V )
18	10	adantr	\|- ( ( ph /\ y e. D ) -> X e. B )
19	4	fvexi	\|- .1. e. _V
20	5	fvexi	\|- .0. e. _V
21	19 20	ifex	\|- if ( y = K , .1. , .0. ) e. _V
22	21	a1i	\|- ( ( ph /\ y e. D ) -> if ( y = K , .1. , .0. ) e. _V )
23		fconstmpt	\|- ( D X. { X } ) = ( y e. D \|-> X )
24	23	a1i	\|- ( ph -> ( D X. { X } ) = ( y e. D \|-> X ) )
25		eqidd	\|- ( ph -> ( y e. D \|-> if ( y = K , .1. , .0. ) ) = ( y e. D \|-> if ( y = K , .1. , .0. ) ) )
26	17 18 22 24 25	offval2	\|- ( ph -> ( ( D X. { X } ) oF ( .r ` R ) ( y e. D \|-> if ( y = K , .1. , .0. ) ) ) = ( y e. D \|-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) ) )
27		oveq2	\|- ( .1. = if ( y = K , .1. , .0. ) -> ( X ( .r ` R ) .1. ) = ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) )
28	27	eqeq1d	\|- ( .1. = if ( y = K , .1. , .0. ) -> ( ( X ( .r ` R ) .1. ) = if ( y = K , X , .0. ) <-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) = if ( y = K , X , .0. ) ) )
29		oveq2	\|- ( .0. = if ( y = K , .1. , .0. ) -> ( X ( .r ` R ) .0. ) = ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) )
30	29	eqeq1d	\|- ( .0. = if ( y = K , .1. , .0. ) -> ( ( X ( .r ` R ) .0. ) = if ( y = K , X , .0. ) <-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) = if ( y = K , X , .0. ) ) )
31	6 12 4	ringridm	\|- ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) .1. ) = X )
32	8 10 31	syl2anc	\|- ( ph -> ( X ( .r ` R ) .1. ) = X )
33		iftrue	\|- ( y = K -> if ( y = K , X , .0. ) = X )
34	33	eqcomd	\|- ( y = K -> X = if ( y = K , X , .0. ) )
35	32 34	sylan9eq	\|- ( ( ph /\ y = K ) -> ( X ( .r ` R ) .1. ) = if ( y = K , X , .0. ) )
36	6 12 5	ringrz	\|- ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) .0. ) = .0. )
37	8 10 36	syl2anc	\|- ( ph -> ( X ( .r ` R ) .0. ) = .0. )
38		iffalse	\|- ( -. y = K -> if ( y = K , X , .0. ) = .0. )
39	38	eqcomd	\|- ( -. y = K -> .0. = if ( y = K , X , .0. ) )
40	37 39	sylan9eq	\|- ( ( ph /\ -. y = K ) -> ( X ( .r ` R ) .0. ) = if ( y = K , X , .0. ) )
41	28 30 35 40	ifbothda	\|- ( ph -> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) = if ( y = K , X , .0. ) )
42	41	mpteq2dv	\|- ( ph -> ( y e. D \|-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) ) = ( y e. D \|-> if ( y = K , X , .0. ) ) )
43	14 26 42	3eqtrd	\|- ( ph -> ( X .x. ( y e. D \|-> if ( y = K , .1. , .0. ) ) ) = ( y e. D \|-> if ( y = K , X , .0. ) ) )

Metamath Proof Explorer

Theorem mplmon2

Proof