Theorem mndvcl

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

	Ref	Expression
Hypotheses	mndvcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	mndvcl.p	⊢ + = ( +g ‘ 𝑀 )
Assertion	mndvcl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f + 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		mndvcl.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		mndvcl.p	⊢ + = ( +g ‘ 𝑀 )
3	1 2	mndcl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
4	3	3expb	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
5	4	3ad2antl1	⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
6		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑋 : 𝐼 ⟶ 𝐵 )
7	6	3ad2ant2	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑋 : 𝐼 ⟶ 𝐵 )
8		elmapi	⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) → 𝑌 : 𝐼 ⟶ 𝐵 )
9	8	3ad2ant3	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝑌 : 𝐼 ⟶ 𝐵 )
10		elmapex	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → ( 𝐵 ∈ V ∧ 𝐼 ∈ V ) )
11	10	simprd	⊢ ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) → 𝐼 ∈ V )
12	11	3ad2ant2	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → 𝐼 ∈ V )
13		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
14	5 7 9 12 12 13	off	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f + 𝑌 ) : 𝐼 ⟶ 𝐵 )
15	1	fvexi	⊢ 𝐵 ∈ V
16		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 𝐼 ∈ V ) → ( ( 𝑋 ∘f + 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) ↔ ( 𝑋 ∘f + 𝑌 ) : 𝐼 ⟶ 𝐵 ) )
17	15 12 16	sylancr	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( ( 𝑋 ∘f + 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) ↔ ( 𝑋 ∘f + 𝑌 ) : 𝐼 ⟶ 𝐵 ) )
18	14 17	mpbird	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f + 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) )