fisuppov1

Description: Formula building theorem for finite support: operator with left annihilator. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	fisuppov1.1	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
	fisuppov1.2	⊢ ( 𝜑 → 0 ∈ 𝑋 )
	fisuppov1.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
	fisuppov1.4	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
	fisuppov1.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑌 )
	fisuppov1.6	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐸 )
	fisuppov1.7	⊢ ( 𝜑 → 𝐹 finSupp 0 )
	fisuppov1.8	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 0 𝑂 𝑦 ) = 𝑍 )
Assertion	fisuppov1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		fisuppov1.1	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
2		fisuppov1.2	⊢ ( 𝜑 → 0 ∈ 𝑋 )
3		fisuppov1.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
4		fisuppov1.4	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
5		fisuppov1.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑌 )
6		fisuppov1.6	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐸 )
7		fisuppov1.7	⊢ ( 𝜑 → 𝐹 finSupp 0 )
8		fisuppov1.8	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 0 𝑂 𝑦 ) = 𝑍 )
9	3 4	ssexd	⊢ ( 𝜑 → 𝐷 ∈ V )
10	9	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) ∈ V )
11		funmpt	⊢ Fun ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) )
12	11	a1i	⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) )
13	6 4	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
14	13	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐷 ) supp 0 ) = ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) supp 0 ) )
15	6 3	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
16		ressuppss	⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ 𝑋 ) → ( ( 𝐹 ↾ 𝐷 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
17	15 2 16	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐷 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
18	14 17	eqsstrrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
19		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
20	18 8 19 5 2	suppssov1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ ( 𝐹 supp 0 ) )
21	10 1 12 7 20	fsuppsssuppgd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑂 𝐵 ) ) finSupp 𝑍 )

Metamath Proof Explorer

Theorem fisuppov1

Proof