Metamath Proof Explorer

Theorem ofaddmndmap

Description: The function operation applied to the addition for functions (with the same domain) into a monoid is a function (with the same domain) into the monoid. (Contributed by AV, 6-Apr-2019)

Ref Expression
Hypotheses ofaddmndmap.r 
|- R = ( Base ` M )
ofaddmndmap.p 
|- .+ = ( +g ` M )
Assertion ofaddmndmap 
|- ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF .+ B ) e. ( R ^m V ) )

Proof

Step Hyp Ref Expression
1 ofaddmndmap.r 
 |-  R = ( Base ` M )
2 ofaddmndmap.p 
 |-  .+ = ( +g ` M )
3 simpl1 
 |-  ( ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( x e. R /\ y e. R ) ) -> M e. Mnd )
4 simprl 
 |-  ( ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( x e. R /\ y e. R ) ) -> x e. R )
5 simprr 
 |-  ( ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( x e. R /\ y e. R ) ) -> y e. R )
6 1 2 mndcl 
 |-  ( ( M e. Mnd /\ x e. R /\ y e. R ) -> ( x .+ y ) e. R )
7 3 4 5 6 syl3anc 
 |-  ( ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) /\ ( x e. R /\ y e. R ) ) -> ( x .+ y ) e. R )
8 elmapi 
 |-  ( A e. ( R ^m V ) -> A : V --> R )
9 8 adantr 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> A : V --> R )
10 9 3ad2ant3 
 |-  ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> A : V --> R )
11 elmapi 
 |-  ( B e. ( R ^m V ) -> B : V --> R )
12 11 adantl 
 |-  ( ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) -> B : V --> R )
13 12 3ad2ant3 
 |-  ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> B : V --> R )
14 simp2 
 |-  ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> V e. Y )
15 inidm 
 |-  ( V i^i V ) = V
16 7 10 13 14 14 15 off 
 |-  ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF .+ B ) : V --> R )
17 1 fvexi 
 |-  R e. _V
18 elmapg 
 |-  ( ( R e. _V /\ V e. Y ) -> ( ( A oF .+ B ) e. ( R ^m V ) <-> ( A oF .+ B ) : V --> R ) )
19 17 14 18 sylancr 
 |-  ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( ( A oF .+ B ) e. ( R ^m V ) <-> ( A oF .+ B ) : V --> R ) )
20 16 19 mpbird 
 |-  ( ( M e. Mnd /\ V e. Y /\ ( A e. ( R ^m V ) /\ B e. ( R ^m V ) ) ) -> ( A oF .+ B ) e. ( R ^m V ) )