mndvcl

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

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

Step	Hyp	Ref	Expression
1		mndvcl.b	$⊢ B = {Base}_{M}$
2		mndvcl.p	$⊢ \underset{˙}{+} = +_{M}$
3	1 2	mndcl	$⊢ (M \in Mnd \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
4	3	3expb	$⊢ (M \in Mnd \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
5	4	3ad2antl1	$⊢ ((M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
6		elmapi	$⊢ X \in (B^{I}) \to X : I ⟶ B$
7	6	3ad2ant2	$⊢ (M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to X : I ⟶ B$
8		elmapi	$⊢ Y \in (B^{I}) \to Y : I ⟶ B$
9	8	3ad2ant3	$⊢ (M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to Y : I ⟶ B$
10		elmapex	$⊢ X \in (B^{I}) \to (B \in V \land I \in V)$
11	10	simprd	$⊢ X \in (B^{I}) \to I \in V$
12	11	3ad2ant2	$⊢ (M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to I \in V$
13		inidm	$⊢ I \cap I = I$
14	5 7 9 12 12 13	off	$⊢ (M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to (X {\underset{˙}{+}}_{f} Y) : I ⟶ B$
15	1	fvexi	$⊢ B \in V$
16		elmapg	$⊢ (B \in V \land I \in V) \to (X {\underset{˙}{+}}_{f} Y \in (B^{I}) \leftrightarrow (X {\underset{˙}{+}}_{f} Y) : I ⟶ B)$
17	15 12 16	sylancr	$⊢ (M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to (X {\underset{˙}{+}}_{f} Y \in (B^{I}) \leftrightarrow (X {\underset{˙}{+}}_{f} Y) : I ⟶ B)$
18	14 17	mpbird	$⊢ (M \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to X {\underset{˙}{+}}_{f} Y \in (B^{I})$

Metamath Proof Explorer