pws0g

Description: The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsmnd.y	\|- Y = ( R ^s I )
	pws0g.z	\|- .0. = ( 0g ` R )
Assertion	pws0g	\|- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		pwsmnd.y	\|- Y = ( R ^s I )
2		pws0g.z	\|- .0. = ( 0g ` R )
3		eqid	\|- ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
4		simpr	\|- ( ( R e. Mnd /\ I e. V ) -> I e. V )
5		fvexd	\|- ( ( R e. Mnd /\ I e. V ) -> ( Scalar ` R ) e. _V )
6		fconst6g	\|- ( R e. Mnd -> ( I X. { R } ) : I --> Mnd )
7	6	adantr	\|- ( ( R e. Mnd /\ I e. V ) -> ( I X. { R } ) : I --> Mnd )
8	3 4 5 7	prds0g	\|- ( ( R e. Mnd /\ I e. V ) -> ( 0g o. ( I X. { R } ) ) = ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
9		fconstmpt	\|- ( I X. { .0. } ) = ( x e. I \|-> .0. )
10		elex	\|- ( R e. Mnd -> R e. _V )
11	10	ad2antrr	\|- ( ( ( R e. Mnd /\ I e. V ) /\ x e. I ) -> R e. _V )
12		fconstmpt	\|- ( I X. { R } ) = ( x e. I \|-> R )
13	12	a1i	\|- ( ( R e. Mnd /\ I e. V ) -> ( I X. { R } ) = ( x e. I \|-> R ) )
14		fn0g	\|- 0g Fn _V
15	14	a1i	\|- ( ( R e. Mnd /\ I e. V ) -> 0g Fn _V )
16		dffn5	\|- ( 0g Fn _V <-> 0g = ( r e. _V \|-> ( 0g ` r ) ) )
17	15 16	sylib	\|- ( ( R e. Mnd /\ I e. V ) -> 0g = ( r e. _V \|-> ( 0g ` r ) ) )
18		fveq2	\|- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
19	18 2	eqtr4di	\|- ( r = R -> ( 0g ` r ) = .0. )
20	11 13 17 19	fmptco	\|- ( ( R e. Mnd /\ I e. V ) -> ( 0g o. ( I X. { R } ) ) = ( x e. I \|-> .0. ) )
21	9 20	eqtr4id	\|- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g o. ( I X. { R } ) ) )
22		eqid	\|- ( Scalar ` R ) = ( Scalar ` R )
23	1 22	pwsval	\|- ( ( R e. Mnd /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
24	23	fveq2d	\|- ( ( R e. Mnd /\ I e. V ) -> ( 0g ` Y ) = ( 0g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
25	8 21 24	3eqtr4d	\|- ( ( R e. Mnd /\ I e. V ) -> ( I X. { .0. } ) = ( 0g ` Y ) )

Metamath Proof Explorer

Theorem pws0g

Proof