Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` M )
Assertion mndvcl 
|- ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( X oF .+ Y ) e. ( B ^m I ) )

Proof

Step Hyp Ref Expression
1 mndvcl.b 
 |-  B = ( Base ` M )
2 mndvcl.p 
 |-  .+ = ( +g ` M )
3 1 2 mndcl 
 |-  ( ( M e. Mnd /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
4 3 3expb 
 |-  ( ( M e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
5 4 3ad2antl1 
 |-  ( ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
6 elmapi 
 |-  ( X e. ( B ^m I ) -> X : I --> B )
7 6 3ad2ant2 
 |-  ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> X : I --> B )
8 elmapi 
 |-  ( Y e. ( B ^m I ) -> Y : I --> B )
9 8 3ad2ant3 
 |-  ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> Y : I --> B )
10 elmapex 
 |-  ( X e. ( B ^m I ) -> ( B e. _V /\ I e. _V ) )
11 10 simprd 
 |-  ( X e. ( B ^m I ) -> I e. _V )
12 11 3ad2ant2 
 |-  ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> I e. _V )
13 inidm 
 |-  ( I i^i I ) = I
14 5 7 9 12 12 13 off 
 |-  ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( X oF .+ Y ) : I --> B )
15 1 fvexi 
 |-  B e. _V
16 elmapg 
 |-  ( ( B e. _V /\ I e. _V ) -> ( ( X oF .+ Y ) e. ( B ^m I ) <-> ( X oF .+ Y ) : I --> B ) )
17 15 12 16 sylancr 
 |-  ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( ( X oF .+ Y ) e. ( B ^m I ) <-> ( X oF .+ Y ) : I --> B ) )
18 14 17 mpbird 
 |-  ( ( M e. Mnd /\ X e. ( B ^m I ) /\ Y e. ( B ^m I ) ) -> ( X oF .+ Y ) e. ( B ^m I ) )