mndvrid

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

	Ref	Expression
Hypotheses	mndvcl.b	$⊢ B = {Base}_{M}$
	mndvcl.p	$⊢ \underset{˙}{+} = +_{M}$
	mndvlid.z	$⊢ \underset{˙}{0} = 0_{M}$
Assertion	mndvrid	$⊢ (M \in Mnd \land X \in (B^{I})) \to X {\underset{˙}{+}}_{f} (I \times \{\underset{˙}{0}\}) = X$

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

Metamath Proof Explorer