Metamath Proof Explorer


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