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

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 
|- ( ph -> Z e. V )
fisuppov1.2 
|- ( ph -> .0. e. X )
fisuppov1.3 
|- ( ph -> A e. W )
fisuppov1.4 
|- ( ph -> D C_ A )
fisuppov1.5 
|- ( ( ph /\ x e. D ) -> B e. Y )
fisuppov1.6 
|- ( ph -> F : A --> E )
fisuppov1.7 
|- ( ph -> F finSupp .0. )
fisuppov1.8 
|- ( ( ph /\ y e. Y ) -> ( .0. O y ) = Z )
Assertion fisuppov1 
|- ( ph -> ( x e. D |-> ( ( F ` x ) O B ) ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fisuppov1.1 
 |-  ( ph -> Z e. V )
2 fisuppov1.2 
 |-  ( ph -> .0. e. X )
3 fisuppov1.3 
 |-  ( ph -> A e. W )
4 fisuppov1.4 
 |-  ( ph -> D C_ A )
5 fisuppov1.5 
 |-  ( ( ph /\ x e. D ) -> B e. Y )
6 fisuppov1.6 
 |-  ( ph -> F : A --> E )
7 fisuppov1.7 
 |-  ( ph -> F finSupp .0. )
8 fisuppov1.8 
 |-  ( ( ph /\ y e. Y ) -> ( .0. O y ) = Z )
9 3 4 ssexd 
 |-  ( ph -> D e. _V )
10 9 mptexd 
 |-  ( ph -> ( x e. D |-> ( ( F ` x ) O B ) ) e. _V )
11 funmpt 
 |-  Fun ( x e. D |-> ( ( F ` x ) O B ) )
12 11 a1i 
 |-  ( ph -> Fun ( x e. D |-> ( ( F ` x ) O B ) ) )
13 6 4 feqresmpt 
 |-  ( ph -> ( F |` D ) = ( x e. D |-> ( F ` x ) ) )
14 13 oveq1d 
 |-  ( ph -> ( ( F |` D ) supp .0. ) = ( ( x e. D |-> ( F ` x ) ) supp .0. ) )
15 6 3 fexd 
 |-  ( ph -> F e. _V )
16 ressuppss 
 |-  ( ( F e. _V /\ .0. e. X ) -> ( ( F |` D ) supp .0. ) C_ ( F supp .0. ) )
17 15 2 16 syl2anc 
 |-  ( ph -> ( ( F |` D ) supp .0. ) C_ ( F supp .0. ) )
18 14 17 eqsstrrd 
 |-  ( ph -> ( ( x e. D |-> ( F ` x ) ) supp .0. ) C_ ( F supp .0. ) )
19 fvexd 
 |-  ( ( ph /\ x e. D ) -> ( F ` x ) e. _V )
20 18 8 19 5 2 suppssov1 
 |-  ( ph -> ( ( x e. D |-> ( ( F ` x ) O B ) ) supp Z ) C_ ( F supp .0. ) )
21 10 1 12 7 20 fsuppsssuppgd 
 |-  ( ph -> ( x e. D |-> ( ( F ` x ) O B ) ) finSupp Z )