Metamath Proof Explorer

Theorem psrbagaddcl

Description: The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypothesis psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagaddcl ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝐺 ∈ 𝐷 ) → ( 𝐹 ∘f + 𝐺 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 + 𝐺 ) ∈ 𝐷 )