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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagaddclOLD ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹f + 𝐺 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 nn0addcl ( ( 𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
3 2 adantl ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ ( 𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ) ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
4 simp2 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐹𝐷 )
5 1 psrbag ( 𝐼𝑉 → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
6 5 3ad2ant1 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
7 4 6 mpbid ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) )
8 7 simpld ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
9 simp3 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐺𝐷 )
10 1 psrbag ( 𝐼𝑉 → ( 𝐺𝐷 ↔ ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( 𝐺 “ ℕ ) ∈ Fin ) ) )
11 10 3ad2ant1 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐺𝐷 ↔ ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( 𝐺 “ ℕ ) ∈ Fin ) ) )
12 9 11 mpbid ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( 𝐺 “ ℕ ) ∈ Fin ) )
13 12 simpld ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
14 simp1 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐼𝑉 )
15 inidm ( 𝐼𝐼 ) = 𝐼
16 3 8 13 14 14 15 off ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹f + 𝐺 ) : 𝐼 ⟶ ℕ0 )
17 frnnn0supp ( ( 𝐼𝑉 ∧ ( 𝐹f + 𝐺 ) : 𝐼 ⟶ ℕ0 ) → ( ( 𝐹f + 𝐺 ) supp 0 ) = ( ( 𝐹f + 𝐺 ) “ ℕ ) )
18 14 16 17 syl2anc ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝐹f + 𝐺 ) supp 0 ) = ( ( 𝐹f + 𝐺 ) “ ℕ ) )
19 fvexd ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ 𝑥𝐼 ) → ( 𝐹𝑥 ) ∈ V )
20 fvexd ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ 𝑥𝐼 ) → ( 𝐺𝑥 ) ∈ V )
21 8 feqmptd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐹 = ( 𝑥𝐼 ↦ ( 𝐹𝑥 ) ) )
22 13 feqmptd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 𝐺 = ( 𝑥𝐼 ↦ ( 𝐺𝑥 ) ) )
23 14 19 20 21 22 offval2 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹f + 𝐺 ) = ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) ) )
24 23 oveq1d ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝐹f + 𝐺 ) supp 0 ) = ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) ) supp 0 ) )
25 18 24 eqtr3d ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝐹f + 𝐺 ) “ ℕ ) = ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) ) supp 0 ) )
26 frnnn0supp ( ( 𝐼𝑉𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )
27 14 8 26 syl2anc ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹 supp 0 ) = ( 𝐹 “ ℕ ) )
28 7 simprd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹 “ ℕ ) ∈ Fin )
29 27 28 eqeltrd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹 supp 0 ) ∈ Fin )
30 frnnn0supp ( ( 𝐼𝑉𝐺 : 𝐼 ⟶ ℕ0 ) → ( 𝐺 supp 0 ) = ( 𝐺 “ ℕ ) )
31 14 13 30 syl2anc ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐺 supp 0 ) = ( 𝐺 “ ℕ ) )
32 12 simprd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐺 “ ℕ ) ∈ Fin )
33 31 32 eqeltrd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐺 supp 0 ) ∈ Fin )
34 unfi ( ( ( 𝐹 supp 0 ) ∈ Fin ∧ ( 𝐺 supp 0 ) ∈ Fin ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
35 29 33 34 syl2anc ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ∈ Fin )
36 ssun1 ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) )
37 36 a1i ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
38 c0ex 0 ∈ V
39 38 a1i ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → 0 ∈ V )
40 8 37 14 39 suppssr ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐹𝑥 ) = 0 )
41 ssun2 ( 𝐺 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) )
42 41 a1i ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐺 supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
43 13 42 14 39 suppssr ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺𝑥 ) = 0 )
44 40 43 oveq12d ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) = ( 0 + 0 ) )
45 00id ( 0 + 0 ) = 0
46 44 45 eqtrdi ( ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) = 0 )
47 46 14 suppss2 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) ) supp 0 ) ⊆ ( ( 𝐹 supp 0 ) ∪ ( 𝐺 supp 0 ) ) )
48 35 47 ssfid ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝑥𝐼 ↦ ( ( 𝐹𝑥 ) + ( 𝐺𝑥 ) ) ) supp 0 ) ∈ Fin )
49 25 48 eqeltrd ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝐹f + 𝐺 ) “ ℕ ) ∈ Fin )
50 1 psrbag ( 𝐼𝑉 → ( ( 𝐹f + 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹f + 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝐹f + 𝐺 ) “ ℕ ) ∈ Fin ) ) )
51 50 3ad2ant1 ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( ( 𝐹f + 𝐺 ) ∈ 𝐷 ↔ ( ( 𝐹f + 𝐺 ) : 𝐼 ⟶ ℕ0 ∧ ( ( 𝐹f + 𝐺 ) “ ℕ ) ∈ Fin ) ) )
52 16 49 51 mpbir2and ( ( 𝐼𝑉𝐹𝐷𝐺𝐷 ) → ( 𝐹f + 𝐺 ) ∈ 𝐷 )