Step |
Hyp |
Ref |
Expression |
1 |
|
psrbag.d |
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
2 |
|
nn0addcl |
|- ( ( x e. NN0 /\ y e. NN0 ) -> ( x + y ) e. NN0 ) |
3 |
2
|
adantl |
|- ( ( ( F e. D /\ G e. D ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x + y ) e. NN0 ) |
4 |
1
|
psrbagf |
|- ( F e. D -> F : I --> NN0 ) |
5 |
4
|
adantr |
|- ( ( F e. D /\ G e. D ) -> F : I --> NN0 ) |
6 |
1
|
psrbagf |
|- ( G e. D -> G : I --> NN0 ) |
7 |
6
|
adantl |
|- ( ( F e. D /\ G e. D ) -> G : I --> NN0 ) |
8 |
|
simpl |
|- ( ( F e. D /\ G e. D ) -> F e. D ) |
9 |
5
|
ffnd |
|- ( ( F e. D /\ G e. D ) -> F Fn I ) |
10 |
8 9
|
fndmexd |
|- ( ( F e. D /\ G e. D ) -> I e. _V ) |
11 |
|
inidm |
|- ( I i^i I ) = I |
12 |
3 5 7 10 10 11
|
off |
|- ( ( F e. D /\ G e. D ) -> ( F oF + G ) : I --> NN0 ) |
13 |
|
ovex |
|- ( F oF + G ) e. _V |
14 |
|
frnnn0suppg |
|- ( ( ( F oF + G ) e. _V /\ ( F oF + G ) : I --> NN0 ) -> ( ( F oF + G ) supp 0 ) = ( `' ( F oF + G ) " NN ) ) |
15 |
13 12 14
|
sylancr |
|- ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) = ( `' ( F oF + G ) " NN ) ) |
16 |
1
|
psrbagfsupp |
|- ( F e. D -> F finSupp 0 ) |
17 |
16
|
adantr |
|- ( ( F e. D /\ G e. D ) -> F finSupp 0 ) |
18 |
1
|
psrbagfsupp |
|- ( G e. D -> G finSupp 0 ) |
19 |
18
|
adantl |
|- ( ( F e. D /\ G e. D ) -> G finSupp 0 ) |
20 |
17 19
|
fsuppunfi |
|- ( ( F e. D /\ G e. D ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) e. Fin ) |
21 |
|
0nn0 |
|- 0 e. NN0 |
22 |
21
|
a1i |
|- ( ( F e. D /\ G e. D ) -> 0 e. NN0 ) |
23 |
|
00id |
|- ( 0 + 0 ) = 0 |
24 |
23
|
a1i |
|- ( ( F e. D /\ G e. D ) -> ( 0 + 0 ) = 0 ) |
25 |
10 22 5 7 24
|
suppofssd |
|- ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) ) |
26 |
20 25
|
ssfid |
|- ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) e. Fin ) |
27 |
15 26
|
eqeltrrd |
|- ( ( F e. D /\ G e. D ) -> ( `' ( F oF + G ) " NN ) e. Fin ) |
28 |
1
|
psrbag |
|- ( I e. _V -> ( ( F oF + G ) e. D <-> ( ( F oF + G ) : I --> NN0 /\ ( `' ( F oF + G ) " NN ) e. Fin ) ) ) |
29 |
10 28
|
syl |
|- ( ( F e. D /\ G e. D ) -> ( ( F oF + G ) e. D <-> ( ( F oF + G ) : I --> NN0 /\ ( `' ( F oF + G ) " NN ) e. Fin ) ) ) |
30 |
12 27 29
|
mpbir2and |
|- ( ( F e. D /\ G e. D ) -> ( F oF + G ) e. D ) |