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

Metamath Proof Explorer

Theorem suppovss

Description: A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023)

Ref Expression
Hypotheses suppovss.f 
|- F = ( x e. A , y e. B |-> C )
suppovss.g 
|- G = ( x e. A |-> ( y e. B |-> C ) )
suppovss.a 
|- ( ph -> A e. V )
suppovss.b 
|- ( ph -> B e. W )
suppovss.z 
|- ( ph -> Z e. D )
suppovss.1 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
Assertion suppovss 
|- ( ph -> ( F supp Z ) C_ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) )

Proof

Step Hyp Ref Expression
1 suppovss.f 
 |-  F = ( x e. A , y e. B |-> C )
2 suppovss.g 
 |-  G = ( x e. A |-> ( y e. B |-> C ) )
3 suppovss.a 
 |-  ( ph -> A e. V )
4 suppovss.b 
 |-  ( ph -> B e. W )
5 suppovss.z 
 |-  ( ph -> Z e. D )
6 suppovss.1 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
7 6 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. B C e. D )
8 1 fmpo 
 |-  ( A. x e. A A. y e. B C e. D <-> F : ( A X. B ) --> D )
9 7 8 sylib 
 |-  ( ph -> F : ( A X. B ) --> D )
10 simpr 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> z = <. x , y >. )
11 10 fveq2d 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` z ) = ( F ` <. x , y >. ) )
12 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
13 simpllr 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> x e. ( A \ ( G supp ( B X. { Z } ) ) ) )
14 13 eldifad 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> x e. A )
15 simplr 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> y e. B )
16 simplll 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ph )
17 16 14 15 6 syl12anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> C e. D )
18 1 ovmpt4g 
 |-  ( ( x e. A /\ y e. B /\ C e. D ) -> ( x F y ) = C )
19 14 15 17 18 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( x F y ) = C )
20 12 19 eqtr3id 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` <. x , y >. ) = C )
21 4 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. W )
22 21 mptexd 
 |-  ( ( ph /\ x e. A ) -> ( y e. B |-> C ) e. _V )
23 22 2 fmptd 
 |-  ( ph -> G : A --> _V )
24 ssidd 
 |-  ( ph -> ( G supp ( B X. { Z } ) ) C_ ( G supp ( B X. { Z } ) ) )
25 snex 
 |-  { Z } e. _V
26 25 a1i 
 |-  ( ph -> { Z } e. _V )
27 4 26 xpexd 
 |-  ( ph -> ( B X. { Z } ) e. _V )
28 23 24 3 27 suppssr 
 |-  ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( G ` x ) = ( B X. { Z } ) )
29 28 fveq1d 
 |-  ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( ( G ` x ) ` y ) = ( ( B X. { Z } ) ` y ) )
30 16 13 29 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = ( ( B X. { Z } ) ` y ) )
31 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
32 2 fvmpt2 
 |-  ( ( x e. A /\ ( y e. B |-> C ) e. _V ) -> ( G ` x ) = ( y e. B |-> C ) )
33 31 22 32 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) = ( y e. B |-> C ) )
34 6 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> C e. D )
35 33 34 fvmpt2d 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ( G ` x ) ` y ) = C )
36 16 14 15 35 syl21anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = C )
37 16 5 syl 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> Z e. D )
38 fvconst2g 
 |-  ( ( Z e. D /\ y e. B ) -> ( ( B X. { Z } ) ` y ) = Z )
39 37 15 38 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( ( B X. { Z } ) ` y ) = Z )
40 30 36 39 3eqtr3d 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> C = Z )
41 11 20 40 3eqtrd 
 |-  ( ( ( ( ph /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
42 41 adantl3r 
 |-  ( ( ( ( ( ph /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) /\ x e. ( A \ ( G supp ( B X. { Z } ) ) ) ) /\ y e. B ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
43 elxp2 
 |-  ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) <-> E. x e. ( A \ ( G supp ( B X. { Z } ) ) ) E. y e. B z = <. x , y >. )
44 43 biimpi 
 |-  ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) -> E. x e. ( A \ ( G supp ( B X. { Z } ) ) ) E. y e. B z = <. x , y >. )
45 44 adantl 
 |-  ( ( ph /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) -> E. x e. ( A \ ( G supp ( B X. { Z } ) ) ) E. y e. B z = <. x , y >. )
46 42 45 r19.29vva 
 |-  ( ( ph /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) -> ( F ` z ) = Z )
47 46 adantlr 
 |-  ( ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) /\ z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) ) -> ( F ` z ) = Z )
48 simpr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> z = <. x , y >. )
49 48 fveq2d 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` z ) = ( F ` <. x , y >. ) )
50 simpllr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> x e. A )
51 simplr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) )
52 51 eldifad 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> y e. B )
53 simplll 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ph )
54 53 50 52 6 syl12anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> C e. D )
55 50 52 54 18 syl3anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( x F y ) = C )
56 12 55 eqtr3id 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` <. x , y >. ) = C )
57 53 50 52 35 syl21anc 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = C )
58 fvexd 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ( G ` x ) ` y ) e. _V )
59 34 33 58 fmpt2d 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) : B --> _V )
60 ssiun2 
 |-  ( x e. A -> ( ( G ` x ) supp Z ) C_ U_ x e. A ( ( G ` x ) supp Z ) )
61 60 adantl 
 |-  ( ( ph /\ x e. A ) -> ( ( G ` x ) supp Z ) C_ U_ x e. A ( ( G ` x ) supp Z ) )
62 fveq2 
 |-  ( x = k -> ( G ` x ) = ( G ` k ) )
63 62 oveq1d 
 |-  ( x = k -> ( ( G ` x ) supp Z ) = ( ( G ` k ) supp Z ) )
64 63 cbviunv 
 |-  U_ x e. A ( ( G ` x ) supp Z ) = U_ k e. A ( ( G ` k ) supp Z )
65 61 64 sseqtrdi 
 |-  ( ( ph /\ x e. A ) -> ( ( G ` x ) supp Z ) C_ U_ k e. A ( ( G ` k ) supp Z ) )
66 simpl 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ph )
67 simpr 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> k e. ( A \ ( G supp ( B X. { Z } ) ) ) )
68 67 eldifad 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> k e. A )
69 23 24 3 27 suppssr 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( G ` k ) = ( B X. { Z } ) )
70 eleq1w 
 |-  ( x = k -> ( x e. A <-> k e. A ) )
71 70 anbi2d 
 |-  ( x = k -> ( ( ph /\ x e. A ) <-> ( ph /\ k e. A ) ) )
72 62 fneq1d 
 |-  ( x = k -> ( ( G ` x ) Fn B <-> ( G ` k ) Fn B ) )
73 71 72 imbi12d 
 |-  ( x = k -> ( ( ( ph /\ x e. A ) -> ( G ` x ) Fn B ) <-> ( ( ph /\ k e. A ) -> ( G ` k ) Fn B ) ) )
74 59 ffnd 
 |-  ( ( ph /\ x e. A ) -> ( G ` x ) Fn B )
75 73 74 chvarvv 
 |-  ( ( ph /\ k e. A ) -> ( G ` k ) Fn B )
76 4 adantr 
 |-  ( ( ph /\ k e. A ) -> B e. W )
77 5 adantr 
 |-  ( ( ph /\ k e. A ) -> Z e. D )
78 fnsuppeq0 
 |-  ( ( ( G ` k ) Fn B /\ B e. W /\ Z e. D ) -> ( ( ( G ` k ) supp Z ) = (/) <-> ( G ` k ) = ( B X. { Z } ) ) )
79 75 76 77 78 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( ( ( G ` k ) supp Z ) = (/) <-> ( G ` k ) = ( B X. { Z } ) ) )
80 79 biimpar 
 |-  ( ( ( ph /\ k e. A ) /\ ( G ` k ) = ( B X. { Z } ) ) -> ( ( G ` k ) supp Z ) = (/) )
81 66 68 69 80 syl21anc 
 |-  ( ( ph /\ k e. ( A \ ( G supp ( B X. { Z } ) ) ) ) -> ( ( G ` k ) supp Z ) = (/) )
82 81 ralrimiva 
 |-  ( ph -> A. k e. ( A \ ( G supp ( B X. { Z } ) ) ) ( ( G ` k ) supp Z ) = (/) )
83 nfcv 
 |-  F/_ k ( A \ ( G supp ( B X. { Z } ) ) )
84 83 iunxdif3 
 |-  ( A. k e. ( A \ ( G supp ( B X. { Z } ) ) ) ( ( G ` k ) supp Z ) = (/) -> U_ k e. ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) ( ( G ` k ) supp Z ) = U_ k e. A ( ( G ` k ) supp Z ) )
85 82 84 syl 
 |-  ( ph -> U_ k e. ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) ( ( G ` k ) supp Z ) = U_ k e. A ( ( G ` k ) supp Z ) )
86 dfin4 
 |-  ( A i^i ( G supp ( B X. { Z } ) ) ) = ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) )
87 suppssdm 
 |-  ( G supp ( B X. { Z } ) ) C_ dom G
88 87 23 fssdm 
 |-  ( ph -> ( G supp ( B X. { Z } ) ) C_ A )
89 sseqin2 
 |-  ( ( G supp ( B X. { Z } ) ) C_ A <-> ( A i^i ( G supp ( B X. { Z } ) ) ) = ( G supp ( B X. { Z } ) ) )
90 88 89 sylib 
 |-  ( ph -> ( A i^i ( G supp ( B X. { Z } ) ) ) = ( G supp ( B X. { Z } ) ) )
91 86 90 eqtr3id 
 |-  ( ph -> ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) = ( G supp ( B X. { Z } ) ) )
92 91 iuneq1d 
 |-  ( ph -> U_ k e. ( A \ ( A \ ( G supp ( B X. { Z } ) ) ) ) ( ( G ` k ) supp Z ) = U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
93 85 92 eqtr3d 
 |-  ( ph -> U_ k e. A ( ( G ` k ) supp Z ) = U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
94 93 adantr 
 |-  ( ( ph /\ x e. A ) -> U_ k e. A ( ( G ` k ) supp Z ) = U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
95 65 94 sseqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( G ` x ) supp Z ) C_ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) )
96 5 adantr 
 |-  ( ( ph /\ x e. A ) -> Z e. D )
97 59 95 21 96 suppssr 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) -> ( ( G ` x ) ` y ) = Z )
98 97 adantr 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( ( G ` x ) ` y ) = Z )
99 57 98 eqtr3d 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> C = Z )
100 49 56 99 3eqtrd 
 |-  ( ( ( ( ph /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
101 100 adantl3r 
 |-  ( ( ( ( ( ph /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) /\ x e. A ) /\ y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) /\ z = <. x , y >. ) -> ( F ` z ) = Z )
102 elxp2 
 |-  ( z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) <-> E. x e. A E. y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) z = <. x , y >. )
103 102 biimpi 
 |-  ( z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) -> E. x e. A E. y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) z = <. x , y >. )
104 103 adantl 
 |-  ( ( ph /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> E. x e. A E. y e. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) z = <. x , y >. )
105 101 104 r19.29vva 
 |-  ( ( ph /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( F ` z ) = Z )
106 105 adantlr 
 |-  ( ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) /\ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( F ` z ) = Z )
107 simpr 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) )
108 difxp 
 |-  ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) = ( ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) u. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) )
109 107 108 eleqtrdi 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> z e. ( ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) u. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) )
110 elun 
 |-  ( z e. ( ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) u. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) <-> ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) \/ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) )
111 109 110 sylib 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( z e. ( ( A \ ( G supp ( B X. { Z } ) ) ) X. B ) \/ z e. ( A X. ( B \ U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) )
112 47 106 111 mpjaodan 
 |-  ( ( ph /\ z e. ( ( A X. B ) \ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) ) ) -> ( F ` z ) = Z )
113 9 112 suppss 
 |-  ( ph -> ( F supp Z ) C_ ( ( G supp ( B X. { Z } ) ) X. U_ k e. ( G supp ( B X. { Z } ) ) ( ( G ` k ) supp Z ) ) )