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

Metamath Proof Explorer

Theorem fsuppssindlem1

Description: Lemma for fsuppssind . Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024)

Ref Expression
Hypotheses fsuppssindlem1.z ⊢ ( 𝜑 → 0 ∈ 𝑊 )
fsuppssindlem1.v ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
fsuppssindlem1.1 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
fsuppssindlem1.2 ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑆 )
Assertion fsuppssindlem1 ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑥 ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 fsuppssindlem1.z ⊢ ( 𝜑 → 0 ∈ 𝑊 )
2 fsuppssindlem1.v ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 fsuppssindlem1.1 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
4 fsuppssindlem1.2 ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑆 )
5 3 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
6 fvres ⊢ ( 𝑥 ∈ 𝑆 → ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
7 6 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8 eldif ⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ↔ ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ 𝑆 ) )
9 3 4 2 1 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
10 9 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑆 ) ) → 0 = ( 𝐹 ‘ 𝑥 ) )
11 8 10 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ 𝑆 ) ) → 0 = ( 𝐹 ‘ 𝑥 ) )
12 11 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝑆 ) → 0 = ( 𝐹 ‘ 𝑥 ) )
13 7 12 ifeqda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 ∈ 𝑆 , ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
14 13 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
15 5 14 eqtr4d ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑆 , ( ( 𝐹 ↾ 𝑆 ) ‘ 𝑥 ) , 0 ) ) )