Metamath Proof Explorer

Theorem psrbagaddclOLD

Description: Obsolete version of psrbagaddcl as of 7-Aug-2024. (Contributed by Mario Carneiro, 9-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbagaddclOLD 
|- ( ( I e. V /\ F e. D /\ G e. D ) -> ( F oF + G ) e. D )

Proof

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 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x + y ) e. NN0 )
4 simp2 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> F e. D )
5 1 psrbag 
 |-  ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
6 5 3ad2ant1 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
7 4 6 mpbid 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
8 7 simpld 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> F : I --> NN0 )
9 simp3 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> G e. D )
10 1 psrbag 
 |-  ( I e. V -> ( G e. D <-> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) ) )
11 10 3ad2ant1 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( G e. D <-> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) ) )
12 9 11 mpbid 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) )
13 12 simpld 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> G : I --> NN0 )
14 simp1 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> I e. V )
15 inidm 
 |-  ( I i^i I ) = I
16 3 8 13 14 14 15 off 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F oF + G ) : I --> NN0 )
17 frnnn0supp 
 |-  ( ( I e. V /\ ( F oF + G ) : I --> NN0 ) -> ( ( F oF + G ) supp 0 ) = ( `' ( F oF + G ) " NN ) )
18 14 16 17 syl2anc 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) = ( `' ( F oF + G ) " NN ) )
19 fvexd 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ x e. I ) -> ( F ` x ) e. _V )
20 fvexd 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ x e. I ) -> ( G ` x ) e. _V )
21 8 feqmptd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> F = ( x e. I |-> ( F ` x ) ) )
22 13 feqmptd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> G = ( x e. I |-> ( G ` x ) ) )
23 14 19 20 21 22 offval2 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F oF + G ) = ( x e. I |-> ( ( F ` x ) + ( G ` x ) ) ) )
24 23 oveq1d 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( ( F oF + G ) supp 0 ) = ( ( x e. I |-> ( ( F ` x ) + ( G ` x ) ) ) supp 0 ) )
25 18 24 eqtr3d 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( `' ( F oF + G ) " NN ) = ( ( x e. I |-> ( ( F ` x ) + ( G ` x ) ) ) supp 0 ) )
26 frnnn0supp 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )
27 14 8 26 syl2anc 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F supp 0 ) = ( `' F " NN ) )
28 7 simprd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( `' F " NN ) e. Fin )
29 27 28 eqeltrd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F supp 0 ) e. Fin )
30 frnnn0supp 
 |-  ( ( I e. V /\ G : I --> NN0 ) -> ( G supp 0 ) = ( `' G " NN ) )
31 14 13 30 syl2anc 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( G supp 0 ) = ( `' G " NN ) )
32 12 simprd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( `' G " NN ) e. Fin )
33 31 32 eqeltrd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( G supp 0 ) e. Fin )
34 unfi 
 |-  ( ( ( F supp 0 ) e. Fin /\ ( G supp 0 ) e. Fin ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) e. Fin )
35 29 33 34 syl2anc 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( ( F supp 0 ) u. ( G supp 0 ) ) e. Fin )
36 ssun1 
 |-  ( F supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) )
37 36 a1i 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
38 c0ex 
 |-  0 e. _V
39 38 a1i 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> 0 e. _V )
40 8 37 14 39 suppssr 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ x e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( F ` x ) = 0 )
41 ssun2 
 |-  ( G supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) )
42 41 a1i 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( G supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
43 13 42 14 39 suppssr 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ x e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( G ` x ) = 0 )
44 40 43 oveq12d 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ x e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( ( F ` x ) + ( G ` x ) ) = ( 0 + 0 ) )
45 00id 
 |-  ( 0 + 0 ) = 0
46 44 45 eqtrdi 
 |-  ( ( ( I e. V /\ F e. D /\ G e. D ) /\ x e. ( I \ ( ( F supp 0 ) u. ( G supp 0 ) ) ) ) -> ( ( F ` x ) + ( G ` x ) ) = 0 )
47 46 14 suppss2 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( ( x e. I |-> ( ( F ` x ) + ( G ` x ) ) ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
48 35 47 ssfid 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( ( x e. I |-> ( ( F ` x ) + ( G ` x ) ) ) supp 0 ) e. Fin )
49 25 48 eqeltrd 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( `' ( F oF + G ) " NN ) e. Fin )
50 1 psrbag 
 |-  ( I e. V -> ( ( F oF + G ) e. D <-> ( ( F oF + G ) : I --> NN0 /\ ( `' ( F oF + G ) " NN ) e. Fin ) ) )
51 50 3ad2ant1 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( ( F oF + G ) e. D <-> ( ( F oF + G ) : I --> NN0 /\ ( `' ( F oF + G ) " NN ) e. Fin ) ) )
52 16 49 51 mpbir2and 
 |-  ( ( I e. V /\ F e. D /\ G e. D ) -> ( F oF + G ) e. D )