Metamath Proof Explorer

Theorem suppgsumssiun

Description: The support of a function defined as a group sum is a subset of the indexed union of the supports. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses suppgsumssiun.1 
|- Z = ( 0g ` M )
suppgsumssiun.2 
|- ( ph -> M e. Mnd )
suppgsumssiun.3 
|- ( ph -> B e. W )
suppgsumssiun.4 
|- ( ph -> A e. V )
suppgsumssiun.5 
|- ( ( ( ph /\ x e. A ) /\ y e. B ) -> C e. X )
Assertion suppgsumssiun 
|- ( ph -> ( ( x e. A |-> ( M gsum ( y e. B |-> C ) ) ) supp Z ) C_ U_ y e. B ( ( x e. A |-> C ) supp Z ) )

Proof

Step Hyp Ref Expression
1 suppgsumssiun.1 
 |-  Z = ( 0g ` M )
2 suppgsumssiun.2 
 |-  ( ph -> M e. Mnd )
3 suppgsumssiun.3 
 |-  ( ph -> B e. W )
4 suppgsumssiun.4 
 |-  ( ph -> A e. V )
5 suppgsumssiun.5 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> C e. X )
6 nfv 
 |-  F/ x ph
7 nfcv 
 |-  F/_ x A
8 nfcv 
 |-  F/_ x B
9 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
10 nfcv 
 |-  F/_ x supp
11 nfcv 
 |-  F/_ x Z
12 9 10 11 nfov 
 |-  F/_ x ( ( x e. A |-> C ) supp Z )
13 8 12 nfiun 
 |-  F/_ x U_ y e. B ( ( x e. A |-> C ) supp Z )
14 mpt0 
 |-  ( y e. (/) |-> C ) = (/)
15 14 oveq2i 
 |-  ( M gsum ( y e. (/) |-> C ) ) = ( M gsum (/) )
16 1 gsum0 
 |-  ( M gsum (/) ) = Z
17 15 16 eqtri 
 |-  ( M gsum ( y e. (/) |-> C ) ) = Z
18 mpteq1 
 |-  ( B = (/) -> ( y e. B |-> C ) = ( y e. (/) |-> C ) )
19 18 oveq2d 
 |-  ( B = (/) -> ( M gsum ( y e. B |-> C ) ) = ( M gsum ( y e. (/) |-> C ) ) )
20 19 adantl 
 |-  ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B = (/) ) -> ( M gsum ( y e. B |-> C ) ) = ( M gsum ( y e. (/) |-> C ) ) )
21 1 gsumz 
 |-  ( ( M e. Mnd /\ B e. W ) -> ( M gsum ( y e. B |-> Z ) ) = Z )
22 2 3 21 syl2anc 
 |-  ( ph -> ( M gsum ( y e. B |-> Z ) ) = Z )
23 22 adantr 
 |-  ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) -> ( M gsum ( y e. B |-> Z ) ) = Z )
24 23 adantr 
 |-  ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B = (/) ) -> ( M gsum ( y e. B |-> Z ) ) = Z )
25 17 20 24 3eqtr4a 
 |-  ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B = (/) ) -> ( M gsum ( y e. B |-> C ) ) = ( M gsum ( y e. B |-> Z ) ) )
26 nfv 
 |-  F/ y ph
27 nfcv 
 |-  F/_ y A
28 nfiu1 
 |-  F/_ y U_ y e. B ( ( x e. A |-> C ) supp Z )
29 27 28 nfdif 
 |-  F/_ y ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) )
30 29 nfcri 
 |-  F/ y x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) )
31 26 30 nfan 
 |-  F/ y ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) )
32 nfv 
 |-  F/ y B =/= (/)
33 31 32 nfan 
 |-  F/ y ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) )
34 simpllr 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) )
35 iindif2 
 |-  ( B =/= (/) -> |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) = ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) )
36 35 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) = ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) )
37 34 36 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> x e. |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) )
38 eliin 
 |-  ( x e. |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) -> ( x e. |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) <-> A. y e. B x e. ( A \ ( ( x e. A |-> C ) supp Z ) ) ) )
39 38 ibi 
 |-  ( x e. |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) -> A. y e. B x e. ( A \ ( ( x e. A |-> C ) supp Z ) ) )
40 39 r19.21bi 
 |-  ( ( x e. |^|_ y e. B ( A \ ( ( x e. A |-> C ) supp Z ) ) /\ y e. B ) -> x e. ( A \ ( ( x e. A |-> C ) supp Z ) ) )
41 37 40 sylancom 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> x e. ( A \ ( ( x e. A |-> C ) supp Z ) ) )
42 41 eldifbd 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> -. x e. ( ( x e. A |-> C ) supp Z ) )
43 34 eldifad 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> x e. A )
44 nfv 
 |-  F/ x ( ( ph /\ B =/= (/) ) /\ y e. B )
45 5 an32s 
 |-  ( ( ( ph /\ y e. B ) /\ x e. A ) -> C e. X )
46 45 adantllr 
 |-  ( ( ( ( ph /\ B =/= (/) ) /\ y e. B ) /\ x e. A ) -> C e. X )
47 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
48 44 46 47 fnmptd 
 |-  ( ( ( ph /\ B =/= (/) ) /\ y e. B ) -> ( x e. A |-> C ) Fn A )
49 48 adantllr 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( x e. A |-> C ) Fn A )
50 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> A e. V )
51 eqid 
 |-  ( Base ` M ) = ( Base ` M )
52 51 1 mndidcl 
 |-  ( M e. Mnd -> Z e. ( Base ` M ) )
53 2 52 syl 
 |-  ( ph -> Z e. ( Base ` M ) )
54 53 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> Z e. ( Base ` M ) )
55 elsuppfn 
 |-  ( ( ( x e. A |-> C ) Fn A /\ A e. V /\ Z e. ( Base ` M ) ) -> ( x e. ( ( x e. A |-> C ) supp Z ) <-> ( x e. A /\ ( ( x e. A |-> C ) ` x ) =/= Z ) ) )
56 49 50 54 55 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( x e. ( ( x e. A |-> C ) supp Z ) <-> ( x e. A /\ ( ( x e. A |-> C ) ` x ) =/= Z ) ) )
57 43 56 mpbirand 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( x e. ( ( x e. A |-> C ) supp Z ) <-> ( ( x e. A |-> C ) ` x ) =/= Z ) )
58 difssd 
 |-  ( ph -> ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) C_ A )
59 58 sselda 
 |-  ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) -> x e. A )
60 59 5 syldanl 
 |-  ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ y e. B ) -> C e. X )
61 60 adantlr 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> C e. X )
62 47 fvmpt2 
 |-  ( ( x e. A /\ C e. X ) -> ( ( x e. A |-> C ) ` x ) = C )
63 43 61 62 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( ( x e. A |-> C ) ` x ) = C )
64 63 neeq1d 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( ( ( x e. A |-> C ) ` x ) =/= Z <-> C =/= Z ) )
65 57 64 bitrd 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( x e. ( ( x e. A |-> C ) supp Z ) <-> C =/= Z ) )
66 65 necon2bbid 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> ( C = Z <-> -. x e. ( ( x e. A |-> C ) supp Z ) ) )
67 42 66 mpbird 
 |-  ( ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) /\ y e. B ) -> C = Z )
68 33 67 mpteq2da 
 |-  ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) -> ( y e. B |-> C ) = ( y e. B |-> Z ) )
69 68 oveq2d 
 |-  ( ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) /\ B =/= (/) ) -> ( M gsum ( y e. B |-> C ) ) = ( M gsum ( y e. B |-> Z ) ) )
70 25 69 pm2.61dane 
 |-  ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) -> ( M gsum ( y e. B |-> C ) ) = ( M gsum ( y e. B |-> Z ) ) )
71 70 23 eqtrd 
 |-  ( ( ph /\ x e. ( A \ U_ y e. B ( ( x e. A |-> C ) supp Z ) ) ) -> ( M gsum ( y e. B |-> C ) ) = Z )
72 6 7 13 71 4 suppss2f 
 |-  ( ph -> ( ( x e. A |-> ( M gsum ( y e. B |-> C ) ) ) supp Z ) C_ U_ y e. B ( ( x e. A |-> C ) supp Z ) )