This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )