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 ) ) )