Metamath Proof Explorer

Theorem fsuppssind

Description: Induction on functions F : A --> B with finite support (see fsuppind ) whose supports are subsets of S . (Contributed by SN, 15-Jun-2024)

Ref Expression
Hypotheses fsuppssind.b 
|- B = ( Base ` G )
fsuppssind.z 
|- .0. = ( 0g ` G )
fsuppssind.p 
|- .+ = ( +g ` G )
fsuppssind.g 
|- ( ph -> G e. Grp )
fsuppssind.v 
|- ( ph -> I e. V )
fsuppssind.s 
|- ( ph -> S C_ I )
fsuppssind.0 
|- ( ph -> ( I X. { .0. } ) e. H )
fsuppssind.1 
|- ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. I |-> if ( s = a , b , .0. ) ) e. H )
fsuppssind.2 
|- ( ( ph /\ ( x e. H /\ y e. H ) ) -> ( x oF .+ y ) e. H )
fsuppssind.3 
|- ( ph -> X : I --> B )
fsuppssind.4 
|- ( ph -> X finSupp .0. )
fsuppssind.5 
|- ( ph -> ( X supp .0. ) C_ S )
Assertion fsuppssind 
|- ( ph -> X e. H )

Proof

Step Hyp Ref Expression
1 fsuppssind.b 
 |-  B = ( Base ` G )
2 fsuppssind.z 
 |-  .0. = ( 0g ` G )
3 fsuppssind.p 
 |-  .+ = ( +g ` G )
4 fsuppssind.g 
 |-  ( ph -> G e. Grp )
5 fsuppssind.v 
 |-  ( ph -> I e. V )
6 fsuppssind.s 
 |-  ( ph -> S C_ I )
7 fsuppssind.0 
 |-  ( ph -> ( I X. { .0. } ) e. H )
8 fsuppssind.1 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. I |-> if ( s = a , b , .0. ) ) e. H )
9 fsuppssind.2 
 |-  ( ( ph /\ ( x e. H /\ y e. H ) ) -> ( x oF .+ y ) e. H )
10 fsuppssind.3 
 |-  ( ph -> X : I --> B )
11 fsuppssind.4 
 |-  ( ph -> X finSupp .0. )
12 fsuppssind.5 
 |-  ( ph -> ( X supp .0. ) C_ S )
13 10 6 fssresd 
 |-  ( ph -> ( X |` S ) : S --> B )
14 2 fvexi 
 |-  .0. e. _V
15 14 a1i 
 |-  ( ph -> .0. e. _V )
16 11 15 fsuppres 
 |-  ( ph -> ( X |` S ) finSupp .0. )
17 13 16 jca 
 |-  ( ph -> ( ( X |` S ) : S --> B /\ ( X |` S ) finSupp .0. ) )
18 5 6 ssexd 
 |-  ( ph -> S e. _V )
19 1 2 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
20 4 19 syl 
 |-  ( ph -> .0. e. B )
21 fconst6g 
 |-  ( .0. e. B -> ( S X. { .0. } ) : S --> B )
22 20 21 syl 
 |-  ( ph -> ( S X. { .0. } ) : S --> B )
23 xpundir 
 |-  ( ( S u. ( I \ S ) ) X. { .0. } ) = ( ( S X. { .0. } ) u. ( ( I \ S ) X. { .0. } ) )
24 undif 
 |-  ( S C_ I <-> ( S u. ( I \ S ) ) = I )
25 6 24 sylib 
 |-  ( ph -> ( S u. ( I \ S ) ) = I )
26 25 xpeq1d 
 |-  ( ph -> ( ( S u. ( I \ S ) ) X. { .0. } ) = ( I X. { .0. } ) )
27 23 26 eqtr3id 
 |-  ( ph -> ( ( S X. { .0. } ) u. ( ( I \ S ) X. { .0. } ) ) = ( I X. { .0. } ) )
28 27 7 eqeltrd 
 |-  ( ph -> ( ( S X. { .0. } ) u. ( ( I \ S ) X. { .0. } ) ) e. H )
29 1 fvexi 
 |-  B e. _V
30 29 a1i 
 |-  ( ph -> B e. _V )
31 30 5 6 fsuppssindlem2 
 |-  ( ph -> ( ( S X. { .0. } ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( ( S X. { .0. } ) : S --> B /\ ( ( S X. { .0. } ) u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
32 22 28 31 mpbir2and 
 |-  ( ph -> ( S X. { .0. } ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } )
33 simplrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. S ) -> b e. B )
34 20 ad2antrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. S ) -> .0. e. B )
35 33 34 ifcld 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. S ) -> if ( s = a , b , .0. ) e. B )
36 35 fmpttd 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. S |-> if ( s = a , b , .0. ) ) : S --> B )
37 fconstmpt 
 |-  ( ( I \ S ) X. { .0. } ) = ( s e. ( I \ S ) |-> .0. )
38 37 uneq2i 
 |-  ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( ( I \ S ) X. { .0. } ) ) = ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( s e. ( I \ S ) |-> .0. ) )
39 eldifn 
 |-  ( s e. ( I \ S ) -> -. s e. S )
40 eleq1a 
 |-  ( a e. S -> ( s = a -> s e. S ) )
41 40 con3dimp 
 |-  ( ( a e. S /\ -. s e. S ) -> -. s = a )
42 41 adantlr 
 |-  ( ( ( a e. S /\ b e. B ) /\ -. s e. S ) -> -. s = a )
43 42 adantll 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ -. s e. S ) -> -. s = a )
44 39 43 sylan2 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. ( I \ S ) ) -> -. s = a )
45 44 iffalsed 
 |-  ( ( ( ph /\ ( a e. S /\ b e. B ) ) /\ s e. ( I \ S ) ) -> if ( s = a , b , .0. ) = .0. )
46 45 mpteq2dva 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. ( I \ S ) |-> if ( s = a , b , .0. ) ) = ( s e. ( I \ S ) |-> .0. ) )
47 46 uneq2d 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( s e. ( I \ S ) |-> if ( s = a , b , .0. ) ) ) = ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( s e. ( I \ S ) |-> .0. ) ) )
48 mptun 
 |-  ( s e. ( S u. ( I \ S ) ) |-> if ( s = a , b , .0. ) ) = ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( s e. ( I \ S ) |-> if ( s = a , b , .0. ) ) )
49 6 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> S C_ I )
50 49 24 sylib 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( S u. ( I \ S ) ) = I )
51 50 mpteq1d 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. ( S u. ( I \ S ) ) |-> if ( s = a , b , .0. ) ) = ( s e. I |-> if ( s = a , b , .0. ) ) )
52 48 51 eqtr3id 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( s e. ( I \ S ) |-> if ( s = a , b , .0. ) ) ) = ( s e. I |-> if ( s = a , b , .0. ) ) )
53 47 52 eqtr3d 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( s e. ( I \ S ) |-> .0. ) ) = ( s e. I |-> if ( s = a , b , .0. ) ) )
54 38 53 syl5eq 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( ( I \ S ) X. { .0. } ) ) = ( s e. I |-> if ( s = a , b , .0. ) ) )
55 54 8 eqeltrd 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( ( I \ S ) X. { .0. } ) ) e. H )
56 29 a1i 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> B e. _V )
57 5 adantr 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> I e. V )
58 56 57 49 fsuppssindlem2 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( ( s e. S |-> if ( s = a , b , .0. ) ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( ( s e. S |-> if ( s = a , b , .0. ) ) : S --> B /\ ( ( s e. S |-> if ( s = a , b , .0. ) ) u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
59 36 55 58 mpbir2and 
 |-  ( ( ph /\ ( a e. S /\ b e. B ) ) -> ( s e. S |-> if ( s = a , b , .0. ) ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } )
60 30 5 6 fsuppssindlem2 
 |-  ( ph -> ( s e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
61 30 5 6 fsuppssindlem2 
 |-  ( ph -> ( t e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
62 60 61 anbi12d 
 |-  ( ph -> ( ( s e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } /\ t e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } ) <-> ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) )
63 1 3 grpcl 
 |-  ( ( G e. Grp /\ u e. B /\ v e. B ) -> ( u .+ v ) e. B )
64 4 63 syl3an1 
 |-  ( ( ph /\ u e. B /\ v e. B ) -> ( u .+ v ) e. B )
65 64 3expb 
 |-  ( ( ph /\ ( u e. B /\ v e. B ) ) -> ( u .+ v ) e. B )
66 65 adantlr 
 |-  ( ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) /\ ( u e. B /\ v e. B ) ) -> ( u .+ v ) e. B )
67 simprll 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> s : S --> B )
68 simprrl 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> t : S --> B )
69 18 adantr 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> S e. _V )
70 inidm 
 |-  ( S i^i S ) = S
71 66 67 68 69 69 70 off 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( s oF .+ t ) : S --> B )
72 67 ffnd 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> s Fn S )
73 68 ffnd 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> t Fn S )
74 fnconstg 
 |-  ( .0. e. _V -> ( ( I \ S ) X. { .0. } ) Fn ( I \ S ) )
75 14 74 mp1i 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( I \ S ) X. { .0. } ) Fn ( I \ S ) )
76 5 difexd 
 |-  ( ph -> ( I \ S ) e. _V )
77 76 adantr 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( I \ S ) e. _V )
78 disjdif 
 |-  ( S i^i ( I \ S ) ) = (/)
79 78 a1i 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( S i^i ( I \ S ) ) = (/) )
80 72 73 75 75 69 77 79 ofun 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s u. ( ( I \ S ) X. { .0. } ) ) oF .+ ( t u. ( ( I \ S ) X. { .0. } ) ) ) = ( ( s oF .+ t ) u. ( ( ( I \ S ) X. { .0. } ) oF .+ ( ( I \ S ) X. { .0. } ) ) ) )
81 14 74 mp1i 
 |-  ( ph -> ( ( I \ S ) X. { .0. } ) Fn ( I \ S ) )
82 fvconst2g 
 |-  ( ( .0. e. _V /\ j e. ( I \ S ) ) -> ( ( ( I \ S ) X. { .0. } ) ` j ) = .0. )
83 15 82 sylan 
 |-  ( ( ph /\ j e. ( I \ S ) ) -> ( ( ( I \ S ) X. { .0. } ) ` j ) = .0. )
84 1 3 2 grplid 
 |-  ( ( G e. Grp /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
85 4 20 84 syl2anc 
 |-  ( ph -> ( .0. .+ .0. ) = .0. )
86 85 adantr 
 |-  ( ( ph /\ j e. ( I \ S ) ) -> ( .0. .+ .0. ) = .0. )
87 14 a1i 
 |-  ( ( ph /\ j e. ( I \ S ) ) -> .0. e. _V )
88 87 82 sylancom 
 |-  ( ( ph /\ j e. ( I \ S ) ) -> ( ( ( I \ S ) X. { .0. } ) ` j ) = .0. )
89 86 88 eqtr4d 
 |-  ( ( ph /\ j e. ( I \ S ) ) -> ( .0. .+ .0. ) = ( ( ( I \ S ) X. { .0. } ) ` j ) )
90 76 81 81 81 83 83 89 offveq 
 |-  ( ph -> ( ( ( I \ S ) X. { .0. } ) oF .+ ( ( I \ S ) X. { .0. } ) ) = ( ( I \ S ) X. { .0. } ) )
91 90 uneq2d 
 |-  ( ph -> ( ( s oF .+ t ) u. ( ( ( I \ S ) X. { .0. } ) oF .+ ( ( I \ S ) X. { .0. } ) ) ) = ( ( s oF .+ t ) u. ( ( I \ S ) X. { .0. } ) ) )
92 91 adantr 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s oF .+ t ) u. ( ( ( I \ S ) X. { .0. } ) oF .+ ( ( I \ S ) X. { .0. } ) ) ) = ( ( s oF .+ t ) u. ( ( I \ S ) X. { .0. } ) ) )
93 80 92 eqtrd 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s u. ( ( I \ S ) X. { .0. } ) ) oF .+ ( t u. ( ( I \ S ) X. { .0. } ) ) ) = ( ( s oF .+ t ) u. ( ( I \ S ) X. { .0. } ) ) )
94 9 caovclg 
 |-  ( ( ph /\ ( ( s u. ( ( I \ S ) X. { .0. } ) ) e. H /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) -> ( ( s u. ( ( I \ S ) X. { .0. } ) ) oF .+ ( t u. ( ( I \ S ) X. { .0. } ) ) ) e. H )
95 94 adantrrl 
 |-  ( ( ph /\ ( ( s u. ( ( I \ S ) X. { .0. } ) ) e. H /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s u. ( ( I \ S ) X. { .0. } ) ) oF .+ ( t u. ( ( I \ S ) X. { .0. } ) ) ) e. H )
96 95 adantrll 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s u. ( ( I \ S ) X. { .0. } ) ) oF .+ ( t u. ( ( I \ S ) X. { .0. } ) ) ) e. H )
97 93 96 eqeltrrd 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s oF .+ t ) u. ( ( I \ S ) X. { .0. } ) ) e. H )
98 30 5 6 fsuppssindlem2 
 |-  ( ph -> ( ( s oF .+ t ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( ( s oF .+ t ) : S --> B /\ ( ( s oF .+ t ) u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
99 98 adantr 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( ( s oF .+ t ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( ( s oF .+ t ) : S --> B /\ ( ( s oF .+ t ) u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) )
100 71 97 99 mpbir2and 
 |-  ( ( ph /\ ( ( s : S --> B /\ ( s u. ( ( I \ S ) X. { .0. } ) ) e. H ) /\ ( t : S --> B /\ ( t u. ( ( I \ S ) X. { .0. } ) ) e. H ) ) ) -> ( s oF .+ t ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } )
101 62 100 sylibda 
 |-  ( ( ph /\ ( s e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } /\ t e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } ) ) -> ( s oF .+ t ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } )
102 1 2 3 4 18 32 59 101 fsuppind 
 |-  ( ( ph /\ ( ( X |` S ) : S --> B /\ ( X |` S ) finSupp .0. ) ) -> ( X |` S ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } )
103 17 102 mpdan 
 |-  ( ph -> ( X |` S ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } )
104 30 18 elmapd 
 |-  ( ph -> ( ( X |` S ) e. ( B ^m S ) <-> ( X |` S ) : S --> B ) )
105 13 104 mpbird 
 |-  ( ph -> ( X |` S ) e. ( B ^m S ) )
106 fveq1 
 |-  ( f = ( X |` S ) -> ( f ` i ) = ( ( X |` S ) ` i ) )
107 106 ifeq1d 
 |-  ( f = ( X |` S ) -> if ( i e. S , ( f ` i ) , .0. ) = if ( i e. S , ( ( X |` S ) ` i ) , .0. ) )
108 107 mpteq2dv 
 |-  ( f = ( X |` S ) -> ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) = ( i e. I |-> if ( i e. S , ( ( X |` S ) ` i ) , .0. ) ) )
109 108 eleq1d 
 |-  ( f = ( X |` S ) -> ( ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H <-> ( i e. I |-> if ( i e. S , ( ( X |` S ) ` i ) , .0. ) ) e. H ) )
110 109 elrab3 
 |-  ( ( X |` S ) e. ( B ^m S ) -> ( ( X |` S ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( i e. I |-> if ( i e. S , ( ( X |` S ) ` i ) , .0. ) ) e. H ) )
111 105 110 syl 
 |-  ( ph -> ( ( X |` S ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> ( i e. I |-> if ( i e. S , ( ( X |` S ) ` i ) , .0. ) ) e. H ) )
112 15 5 10 12 fsuppssindlem1 
 |-  ( ph -> X = ( i e. I |-> if ( i e. S , ( ( X |` S ) ` i ) , .0. ) ) )
113 112 eleq1d 
 |-  ( ph -> ( X e. H <-> ( i e. I |-> if ( i e. S , ( ( X |` S ) ` i ) , .0. ) ) e. H ) )
114 111 113 bitr4d 
 |-  ( ph -> ( ( X |` S ) e. { f e. ( B ^m S ) | ( i e. I |-> if ( i e. S , ( f ` i ) , .0. ) ) e. H } <-> X e. H ) )
115 103 114 mpbid 
 |-  ( ph -> X e. H )