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 + ˙ = + M
mndvlid.z 0 ˙ = 0 M
Assertion mndvlid M Mnd X B I I × 0 ˙ + ˙ f X = X

Proof

Step Hyp Ref Expression
1 mndvcl.b B = Base M
2 mndvcl.p + ˙ = + M
3 mndvlid.z 0 ˙ = 0 M
4 elmapex X B I B V I V
5 4 simprd X B I I V
6 5 adantl M Mnd X B I I V
7 elmapi X B I X : I B
8 7 adantl M Mnd X B I X : I B
9 1 3 mndidcl M Mnd 0 ˙ B
10 9 adantr M Mnd X B I 0 ˙ B
11 1 2 3 mndlid M Mnd x B 0 ˙ + ˙ x = x
12 11 adantlr M Mnd X B I x B 0 ˙ + ˙ x = x
13 6 8 10 12 caofid0l M Mnd X B I I × 0 ˙ + ˙ f X = X