Theorem mndvlid

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

	Ref	Expression
Hypotheses	mndvcl.b	$$⊢B={\mathrm{Base}}_M$$
	mndvcl.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	mndvlid.z	$$⊢\underset{\dot{}}{0}=0_M$$
Assertion	mndvlid	$$⊢\left(M\in \mathrm{Mnd}\wedge X\in \left(B^I\right)\right)\to \left(I\times \left\{\underset{\dot{}}{0}\right\}\right){\underset{\dot{}}{+}}_{f}X=X$$

Proof

Step	Hyp	Ref	Expression
1		mndvcl.b	$$⊢B={\mathrm{Base}}_M$$
2		mndvcl.p	$$⊢\underset{\dot{}}{+}={+}_M$$
3		mndvlid.z	$$⊢\underset{\dot{}}{0}=0_M$$
4		elmapex	$$⊢X\in \left(B^I\right)\to \left(B\in \mathrm{V}\wedge I\in \mathrm{V}\right)$$
5	4	simprd	$$⊢X\in \left(B^I\right)\to I\in \mathrm{V}$$
6	5	adantl	$$⊢\left(M\in \mathrm{Mnd}\wedge X\in \left(B^I\right)\right)\to I\in \mathrm{V}$$
7		elmapi	$$⊢X\in \left(B^I\right)\to X:I⟶B$$
8	7	adantl	$$⊢\left(M\in \mathrm{Mnd}\wedge X\in \left(B^I\right)\right)\to X:I⟶B$$
9	1 3	mndidcl	$$⊢M\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
10	9	adantr	$$⊢\left(M\in \mathrm{Mnd}\wedge X\in \left(B^I\right)\right)\to \underset{\dot{}}{0}\in B$$
11	1 2 3	mndlid	$$⊢\left(M\in \mathrm{Mnd}\wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
12	11	adantlr	$$⊢\left(\left(M\in \mathrm{Mnd}\wedge X\in \left(B^I\right)\right)\wedge x\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}x=x$$
13	6 8 10 12	caofid0l	$$⊢\left(M\in \mathrm{Mnd}\wedge X\in \left(B^I\right)\right)\to \left(I\times \left\{\underset{\dot{}}{0}\right\}\right){\underset{\dot{}}{+}}_{f}X=X$$