Theorem mndvlid

Description: Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	mndvcl.b	|- B = ( Base ` M )
	mndvcl.p	|- .+ = ( +g ` M )
	mndvlid.z	|- .0. = ( 0g ` M )
Assertion	mndvlid	|- ( ( M e. Mnd /\ X e. ( B ^m I ) ) -> ( ( I X. { .0. } ) oF .+ X ) = X )

Proof

Step	Hyp	Ref	Expression
1		mndvcl.b	|- B = ( Base ` M )
2		mndvcl.p	|- .+ = ( +g ` M )
3		mndvlid.z	|- .0. = ( 0g ` M )
4		elmapex	|- ( X e. ( B ^m I ) -> ( B e. _V /\ I e. _V ) )
5	4	simprd	|- ( X e. ( B ^m I ) -> I e. _V )
6	5	adantl	|- ( ( M e. Mnd /\ X e. ( B ^m I ) ) -> I e. _V )
7		elmapi	|- ( X e. ( B ^m I ) -> X : I --> B )
8	7	adantl	|- ( ( M e. Mnd /\ X e. ( B ^m I ) ) -> X : I --> B )
9	1 3	mndidcl	|- ( M e. Mnd -> .0. e. B )
10	9	adantr	|- ( ( M e. Mnd /\ X e. ( B ^m I ) ) -> .0. e. B )
11	1 2 3	mndlid	|- ( ( M e. Mnd /\ x e. B ) -> ( .0. .+ x ) = x )
12	11	adantlr	|- ( ( ( M e. Mnd /\ X e. ( B ^m I ) ) /\ x e. B ) -> ( .0. .+ x ) = x )
13	6 8 10 12	caofid0l	|- ( ( M e. Mnd /\ X e. ( B ^m I ) ) -> ( ( I X. { .0. } ) oF .+ X ) = X )