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

Metamath Proof Explorer

Theorem fsuppssov1

Description: Formula building theorem for finite support: operator with left annihilator. Finite support version of suppssov1 . (Contributed by SN, 26-Apr-2025)

Ref Expression
Hypotheses fsuppssov1.s 
|- ( ph -> ( x e. D |-> A ) finSupp Y )
fsuppssov1.o 
|- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
fsuppssov1.a 
|- ( ( ph /\ x e. D ) -> A e. V )
fsuppssov1.b 
|- ( ( ph /\ x e. D ) -> B e. R )
fsuppssov1.z 
|- ( ph -> Z e. W )
Assertion fsuppssov1 
|- ( ph -> ( x e. D |-> ( A O B ) ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fsuppssov1.s 
 |-  ( ph -> ( x e. D |-> A ) finSupp Y )
2 fsuppssov1.o 
 |-  ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
3 fsuppssov1.a 
 |-  ( ( ph /\ x e. D ) -> A e. V )
4 fsuppssov1.b 
 |-  ( ( ph /\ x e. D ) -> B e. R )
5 fsuppssov1.z 
 |-  ( ph -> Z e. W )
6 relfsupp 
 |-  Rel finSupp
7 6 brrelex1i 
 |-  ( ( x e. D |-> A ) finSupp Y -> ( x e. D |-> A ) e. _V )
8 1 7 syl 
 |-  ( ph -> ( x e. D |-> A ) e. _V )
9 3 fmpttd 
 |-  ( ph -> ( x e. D |-> A ) : D --> V )
10 dmfex 
 |-  ( ( ( x e. D |-> A ) e. _V /\ ( x e. D |-> A ) : D --> V ) -> D e. _V )
11 8 9 10 syl2anc 
 |-  ( ph -> D e. _V )
12 11 mptexd 
 |-  ( ph -> ( x e. D |-> ( A O B ) ) e. _V )
13 funmpt 
 |-  Fun ( x e. D |-> ( A O B ) )
14 13 a1i 
 |-  ( ph -> Fun ( x e. D |-> ( A O B ) ) )
15 ssidd 
 |-  ( ph -> ( ( x e. D |-> A ) supp Y ) C_ ( ( x e. D |-> A ) supp Y ) )
16 6 brrelex2i 
 |-  ( ( x e. D |-> A ) finSupp Y -> Y e. _V )
17 1 16 syl 
 |-  ( ph -> Y e. _V )
18 15 2 3 4 17 suppssov1 
 |-  ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ ( ( x e. D |-> A ) supp Y ) )
19 12 5 14 1 18 fsuppsssuppgd 
 |-  ( ph -> ( x e. D |-> ( A O B ) ) finSupp Z )