This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐵 , 𝐶 , 𝑍 ) )
mptiffisupp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
mptiffisupp.b ⊢ ( 𝜑 → 𝐵 ∈ Fin )
mptiffisupp.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
mptiffisupp.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion mptiffisupp ( 𝜑 → 𝐹 finSupp 𝑍 )

Proof

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