Metamath Proof Explorer

Theorem suppeqfsuppbi

Description: If two functions have the same support, one function is finitely supported iff the other one is finitely supported. (Contributed by AV, 30-Jun-2019)

Ref Expression
Assertion suppeqfsuppbi 
|- ( ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) -> ( ( F supp Z ) = ( G supp Z ) -> ( F finSupp Z <-> G finSupp Z ) ) )

Proof

Step Hyp Ref Expression
1 simprlr 
 |-  ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) -> Fun F )
2 simprll 
 |-  ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) -> F e. U )
3 simpl 
 |-  ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) -> Z e. _V )
4 funisfsupp 
 |-  ( ( Fun F /\ F e. U /\ Z e. _V ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
5 1 2 3 4 syl3anc 
 |-  ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
6 5 adantr 
 |-  ( ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) /\ ( F supp Z ) = ( G supp Z ) ) -> ( F finSupp Z <-> ( F supp Z ) e. Fin ) )
7 simpr 
 |-  ( ( G e. V /\ Fun G ) -> Fun G )
8 7 adantr 
 |-  ( ( ( G e. V /\ Fun G ) /\ Z e. _V ) -> Fun G )
9 simpl 
 |-  ( ( G e. V /\ Fun G ) -> G e. V )
10 9 adantr 
 |-  ( ( ( G e. V /\ Fun G ) /\ Z e. _V ) -> G e. V )
11 simpr 
 |-  ( ( ( G e. V /\ Fun G ) /\ Z e. _V ) -> Z e. _V )
12 funisfsupp 
 |-  ( ( Fun G /\ G e. V /\ Z e. _V ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
13 8 10 11 12 syl3anc 
 |-  ( ( ( G e. V /\ Fun G ) /\ Z e. _V ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
14 13 ex 
 |-  ( ( G e. V /\ Fun G ) -> ( Z e. _V -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) ) )
15 14 adantl 
 |-  ( ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) -> ( Z e. _V -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) ) )
16 15 impcom 
 |-  ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) -> ( G finSupp Z <-> ( G supp Z ) e. Fin ) )
17 eleq1 
 |-  ( ( F supp Z ) = ( G supp Z ) -> ( ( F supp Z ) e. Fin <-> ( G supp Z ) e. Fin ) )
18 17 bicomd 
 |-  ( ( F supp Z ) = ( G supp Z ) -> ( ( G supp Z ) e. Fin <-> ( F supp Z ) e. Fin ) )
19 16 18 sylan9bb 
 |-  ( ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) /\ ( F supp Z ) = ( G supp Z ) ) -> ( G finSupp Z <-> ( F supp Z ) e. Fin ) )
20 6 19 bitr4d 
 |-  ( ( ( Z e. _V /\ ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) ) /\ ( F supp Z ) = ( G supp Z ) ) -> ( F finSupp Z <-> G finSupp Z ) )
21 20 exp31 
 |-  ( Z e. _V -> ( ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) -> ( ( F supp Z ) = ( G supp Z ) -> ( F finSupp Z <-> G finSupp Z ) ) ) )
22 relfsupp 
 |-  Rel finSupp
23 22 brrelex2i 
 |-  ( F finSupp Z -> Z e. _V )
24 22 brrelex2i 
 |-  ( G finSupp Z -> Z e. _V )
25 23 24 pm5.21ni 
 |-  ( -. Z e. _V -> ( F finSupp Z <-> G finSupp Z ) )
26 25 2a1d 
 |-  ( -. Z e. _V -> ( ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) -> ( ( F supp Z ) = ( G supp Z ) -> ( F finSupp Z <-> G finSupp Z ) ) ) )
27 21 26 pm2.61i 
 |-  ( ( ( F e. U /\ Fun F ) /\ ( G e. V /\ Fun G ) ) -> ( ( F supp Z ) = ( G supp Z ) -> ( F finSupp Z <-> G finSupp Z ) ) )