Metamath Proof Explorer

Theorem ofoacom

Description: Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion ofoacom 
|- ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> ( F oF +o G ) = ( G oF +o F ) )

Proof

Step Hyp Ref Expression
1 elmapfn 
 |-  ( F e. ( _om ^m A ) -> F Fn A )
2 1 ad2antrl 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> F Fn A )
3 elmapfn 
 |-  ( G e. ( _om ^m A ) -> G Fn A )
4 3 ad2antll 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> G Fn A )
5 simpl 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> A e. V )
6 inidm 
 |-  ( A i^i A ) = A
7 2 4 5 5 6 offn 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> ( F oF +o G ) Fn A )
8 4 2 5 5 6 offn 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> ( G oF +o F ) Fn A )
9 elmapi 
 |-  ( F e. ( _om ^m A ) -> F : A --> _om )
10 9 ad2antrl 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> F : A --> _om )
11 10 ffvelcdmda 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( F ` a ) e. _om )
12 elmapi 
 |-  ( G e. ( _om ^m A ) -> G : A --> _om )
13 12 ad2antll 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> G : A --> _om )
14 13 ffvelcdmda 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( G ` a ) e. _om )
15 nnacom 
 |-  ( ( ( F ` a ) e. _om /\ ( G ` a ) e. _om ) -> ( ( F ` a ) +o ( G ` a ) ) = ( ( G ` a ) +o ( F ` a ) ) )
16 11 14 15 syl2anc 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( ( F ` a ) +o ( G ` a ) ) = ( ( G ` a ) +o ( F ` a ) ) )
17 2 4 jca 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> ( F Fn A /\ G Fn A ) )
18 5 anim1i 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( A e. V /\ a e. A ) )
19 fnfvof 
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( A e. V /\ a e. A ) ) -> ( ( F oF +o G ) ` a ) = ( ( F ` a ) +o ( G ` a ) ) )
20 17 18 19 syl2an2r 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( ( F oF +o G ) ` a ) = ( ( F ` a ) +o ( G ` a ) ) )
21 4 2 jca 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> ( G Fn A /\ F Fn A ) )
22 fnfvof 
 |-  ( ( ( G Fn A /\ F Fn A ) /\ ( A e. V /\ a e. A ) ) -> ( ( G oF +o F ) ` a ) = ( ( G ` a ) +o ( F ` a ) ) )
23 21 18 22 syl2an2r 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( ( G oF +o F ) ` a ) = ( ( G ` a ) +o ( F ` a ) ) )
24 16 20 23 3eqtr4d 
 |-  ( ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) /\ a e. A ) -> ( ( F oF +o G ) ` a ) = ( ( G oF +o F ) ` a ) )
25 7 8 24 eqfnfvd 
 |-  ( ( A e. V /\ ( F e. ( _om ^m A ) /\ G e. ( _om ^m A ) ) ) -> ( F oF +o G ) = ( G oF +o F ) )