Metamath Proof Explorer

Theorem mptiffisupp

Description: Conditions for a mapping function defined with a conditional to have finite support. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses mptiffisupp.f ⊢ F = x ∈ A ⟼ if x ∈ B C Z
mptiffisupp.a ⊢ φ → A ∈ U
mptiffisupp.b ⊢ φ → B ∈ Fin
mptiffisupp.c ⊢ φ ∧ x ∈ B → C ∈ V
mptiffisupp.z ⊢ φ → Z ∈ W
Assertion mptiffisupp ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 mptiffisupp.f ⊢ F = x ∈ A ⟼ if x ∈ B C Z
2 mptiffisupp.a ⊢ φ → A ∈ U
3 mptiffisupp.b ⊢ φ → B ∈ Fin
4 mptiffisupp.c ⊢ φ ∧ x ∈ B → C ∈ V
5 mptiffisupp.z ⊢ φ → Z ∈ W
6 2 mptexd ⊢ φ → x ∈ A ⟼ if x ∈ B C Z ∈ V
7 1 6 eqeltrid ⊢ φ → F ∈ V
8 1 funmpt2 ⊢ Fun ⁡ F
9 8 a1i ⊢ φ → Fun ⁡ F
10 partfun ⊢ x ∈ A ⟼ if x ∈ B C Z = x ∈ A ∩ B ⟼ C ∪ x ∈ A ∖ B ⟼ Z
11 1 10 eqtri ⊢ F = x ∈ A ∩ B ⟼ C ∪ x ∈ A ∖ B ⟼ Z
12 11 oveq1i ⊢ F supp Z = x ∈ A ∩ B ⟼ C ∪ x ∈ A ∖ B ⟼ Z supp Z
13 inss2 ⊢ A ∩ B ⊆ B
14 13 a1i ⊢ φ → A ∩ B ⊆ B
15 14 sselda ⊢ φ ∧ x ∈ A ∩ B → x ∈ B
16 15 4 syldan ⊢ φ ∧ x ∈ A ∩ B → C ∈ V
17 16 fmpttd ⊢ φ → x ∈ A ∩ B ⟼ C : A ∩ B ⟶ V
18 incom ⊢ B ∩ A = A ∩ B
19 infi ⊢ B ∈ Fin → B ∩ A ∈ Fin
20 3 19 syl ⊢ φ → B ∩ A ∈ Fin
21 18 20 eqeltrrid ⊢ φ → A ∩ B ∈ Fin
22 17 21 5 fidmfisupp ⊢ φ → finSupp Z⁡ x ∈ A ∩ B ⟼ C
23 difexg ⊢ A ∈ U → A ∖ B ∈ V
24 mptexg ⊢ A ∖ B ∈ V → x ∈ A ∖ B ⟼ Z ∈ V
25 2 23 24 3syl ⊢ φ → x ∈ A ∖ B ⟼ Z ∈ V
26 funmpt ⊢ Fun ⁡ x ∈ A ∖ B ⟼ Z
27 26 a1i ⊢ φ → Fun ⁡ x ∈ A ∖ B ⟼ Z
28 supppreima ⊢ Fun ⁡ x ∈ A ∖ B ⟼ Z ∧ x ∈ A ∖ B ⟼ Z ∈ V ∧ Z ∈ W → x ∈ A ∖ B ⟼ Z supp Z = x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z
29 26 25 5 28 mp3an2i ⊢ φ → x ∈ A ∖ B ⟼ Z supp Z = x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z
30 simpr ⊢ φ ∧ A ∖ B = ∅ → A ∖ B = ∅
31 30 mpteq1d ⊢ φ ∧ A ∖ B = ∅ → x ∈ A ∖ B ⟼ Z = x ∈ ∅ ⟼ Z
32 mpt0 ⊢ x ∈ ∅ ⟼ Z = ∅
33 31 32 eqtrdi ⊢ φ ∧ A ∖ B = ∅ → x ∈ A ∖ B ⟼ Z = ∅
34 33 cnveqd ⊢ φ ∧ A ∖ B = ∅ → x ∈ A ∖ B ⟼ Z -1 = ∅ -1
35 cnv0 ⊢ ∅ -1 = ∅
36 34 35 eqtrdi ⊢ φ ∧ A ∖ B = ∅ → x ∈ A ∖ B ⟼ Z -1 = ∅
37 36 imaeq1d ⊢ φ ∧ A ∖ B = ∅ → x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = ∅ ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z
38 0ima ⊢ ∅ ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = ∅
39 37 38 eqtrdi ⊢ φ ∧ A ∖ B = ∅ → x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = ∅
40 eqid ⊢ x ∈ A ∖ B ⟼ Z = x ∈ A ∖ B ⟼ Z
41 simpr ⊢ φ ∧ A ∖ B ≠ ∅ → A ∖ B ≠ ∅
42 40 41 rnmptc ⊢ φ ∧ A ∖ B ≠ ∅ → ran ⁡ x ∈ A ∖ B ⟼ Z = Z
43 42 difeq1d ⊢ φ ∧ A ∖ B ≠ ∅ → ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = Z ∖ Z
44 difid ⊢ Z ∖ Z = ∅
45 43 44 eqtrdi ⊢ φ ∧ A ∖ B ≠ ∅ → ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = ∅
46 45 imaeq2d ⊢ φ ∧ A ∖ B ≠ ∅ → x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = x ∈ A ∖ B ⟼ Z -1 ∅
47 ima0 ⊢ x ∈ A ∖ B ⟼ Z -1 ∅ = ∅
48 46 47 eqtrdi ⊢ φ ∧ A ∖ B ≠ ∅ → x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = ∅
49 39 48 pm2.61dane ⊢ φ → x ∈ A ∖ B ⟼ Z -1 ran ⁡ x ∈ A ∖ B ⟼ Z ∖ Z = ∅
50 29 49 eqtrd ⊢ φ → x ∈ A ∖ B ⟼ Z supp Z = ∅
51 0fi ⊢ ∅ ∈ Fin
52 50 51 eqeltrdi ⊢ φ → x ∈ A ∖ B ⟼ Z supp Z ∈ Fin
53 25 5 27 52 isfsuppd ⊢ φ → finSupp Z⁡ x ∈ A ∖ B ⟼ Z
54 22 53 fsuppun ⊢ φ → x ∈ A ∩ B ⟼ C ∪ x ∈ A ∖ B ⟼ Z supp Z ∈ Fin
55 12 54 eqeltrid ⊢ φ → F supp Z ∈ Fin
56 7 5 9 55 isfsuppd ⊢ φ → finSupp Z⁡ F