Metamath Proof Explorer

Theorem fsuppind

Description: Induction on functions F : A --> B with finite support, or in other words the base set of the free module (see frlmelbas and frlmplusgval ). This theorem is structurally general for polynomial proof usage (see mplelbas and mpladd ). Note that hypothesis 0 is redundant when I is nonempty. (Contributed by SN, 18-May-2024)

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

Proof

Step Hyp Ref Expression
1 fsuppind.b 
 |-  B = ( Base ` G )
2 fsuppind.z 
 |-  .0. = ( 0g ` G )
3 fsuppind.p 
 |-  .+ = ( +g ` G )
4 fsuppind.g 
 |-  ( ph -> G e. Grp )
5 fsuppind.v 
 |-  ( ph -> I e. V )
6 fsuppind.0 
 |-  ( ph -> ( I X. { .0. } ) e. H )
7 fsuppind.1 
 |-  ( ( ph /\ ( a e. I /\ b e. B ) ) -> ( x e. I |-> if ( x = a , b , .0. ) ) e. H )
8 fsuppind.2 
 |-  ( ( ph /\ ( x e. H /\ y e. H ) ) -> ( x oF .+ y ) e. H )
9 1 fvexi 
 |-  B e. _V
10 9 a1i 
 |-  ( ph -> B e. _V )
11 10 5 elmapd 
 |-  ( ph -> ( X e. ( B ^m I ) <-> X : I --> B ) )
12 11 adantr 
 |-  ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) -> ( X e. ( B ^m I ) <-> X : I --> B ) )
13 eqeq1 
 |-  ( i = 1 -> ( i = ( # ` ( h supp .0. ) ) <-> 1 = ( # ` ( h supp .0. ) ) ) )
14 13 imbi1d 
 |-  ( i = 1 -> ( ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> ( 1 = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
15 14 ralbidv 
 |-  ( i = 1 -> ( A. h e. ( B ^m I ) ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> A. h e. ( B ^m I ) ( 1 = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
16 eqeq1 
 |-  ( i = j -> ( i = ( # ` ( h supp .0. ) ) <-> j = ( # ` ( h supp .0. ) ) ) )
17 16 imbi1d 
 |-  ( i = j -> ( ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
18 17 ralbidv 
 |-  ( i = j -> ( A. h e. ( B ^m I ) ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
19 eqeq1 
 |-  ( i = ( j + 1 ) -> ( i = ( # ` ( h supp .0. ) ) <-> ( j + 1 ) = ( # ` ( h supp .0. ) ) ) )
20 19 imbi1d 
 |-  ( i = ( j + 1 ) -> ( ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> ( ( j + 1 ) = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
21 20 ralbidv 
 |-  ( i = ( j + 1 ) -> ( A. h e. ( B ^m I ) ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> A. h e. ( B ^m I ) ( ( j + 1 ) = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
22 eqeq1 
 |-  ( i = n -> ( i = ( # ` ( h supp .0. ) ) <-> n = ( # ` ( h supp .0. ) ) ) )
23 22 imbi1d 
 |-  ( i = n -> ( ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> ( n = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
24 23 ralbidv 
 |-  ( i = n -> ( A. h e. ( B ^m I ) ( i = ( # ` ( h supp .0. ) ) -> h e. H ) <-> A. h e. ( B ^m I ) ( n = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
25 eqcom 
 |-  ( 1 = ( # ` ( h supp .0. ) ) <-> ( # ` ( h supp .0. ) ) = 1 )
26 ovex 
 |-  ( h supp .0. ) e. _V
27 euhash1 
 |-  ( ( h supp .0. ) e. _V -> ( ( # ` ( h supp .0. ) ) = 1 <-> E! c c e. ( h supp .0. ) ) )
28 26 27 ax-mp 
 |-  ( ( # ` ( h supp .0. ) ) = 1 <-> E! c c e. ( h supp .0. ) )
29 25 28 bitri 
 |-  ( 1 = ( # ` ( h supp .0. ) ) <-> E! c c e. ( h supp .0. ) )
30 elmapfn 
 |-  ( h e. ( B ^m I ) -> h Fn I )
31 30 adantl 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> h Fn I )
32 5 adantr 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> I e. V )
33 2 fvexi 
 |-  .0. e. _V
34 33 a1i 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> .0. e. _V )
35 elsuppfn 
 |-  ( ( h Fn I /\ I e. V /\ .0. e. _V ) -> ( c e. ( h supp .0. ) <-> ( c e. I /\ ( h ` c ) =/= .0. ) ) )
36 31 32 34 35 syl3anc 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> ( c e. ( h supp .0. ) <-> ( c e. I /\ ( h ` c ) =/= .0. ) ) )
37 36 eubidv 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> ( E! c c e. ( h supp .0. ) <-> E! c ( c e. I /\ ( h ` c ) =/= .0. ) ) )
38 df-reu 
 |-  ( E! c e. I ( h ` c ) =/= .0. <-> E! c ( c e. I /\ ( h ` c ) =/= .0. ) )
39 37 38 bitr4di 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> ( E! c c e. ( h supp .0. ) <-> E! c e. I ( h ` c ) =/= .0. ) )
40 30 ad2antlr 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> h Fn I )
41 fvex 
 |-  ( h ` x ) e. _V
42 41 33 ifex 
 |-  if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) e. _V
43 eqid 
 |-  ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) = ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) )
44 42 43 fnmpti 
 |-  ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) Fn I
45 44 a1i 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) Fn I )
46 eqeq1 
 |-  ( x = v -> ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) <-> v = ( iota_ c e. I ( h ` c ) =/= .0. ) ) )
47 fveq2 
 |-  ( x = v -> ( h ` x ) = ( h ` v ) )
48 46 47 ifbieq1d 
 |-  ( x = v -> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) = if ( v = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` v ) , .0. ) )
49 48 43 42 fvmpt3i 
 |-  ( v e. I -> ( ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) ` v ) = if ( v = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` v ) , .0. ) )
50 49 adantl 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> ( ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) ` v ) = if ( v = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` v ) , .0. ) )
51 eqidd 
 |-  ( ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) /\ v = ( iota_ c e. I ( h ` c ) =/= .0. ) ) -> ( h ` v ) = ( h ` v ) )
52 simpr 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> v e. I )
53 simplr 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> E! c e. I ( h ` c ) =/= .0. )
54 fveq2 
 |-  ( c = v -> ( h ` c ) = ( h ` v ) )
55 54 neeq1d 
 |-  ( c = v -> ( ( h ` c ) =/= .0. <-> ( h ` v ) =/= .0. ) )
56 55 riota2 
 |-  ( ( v e. I /\ E! c e. I ( h ` c ) =/= .0. ) -> ( ( h ` v ) =/= .0. <-> ( iota_ c e. I ( h ` c ) =/= .0. ) = v ) )
57 52 53 56 syl2anc 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> ( ( h ` v ) =/= .0. <-> ( iota_ c e. I ( h ` c ) =/= .0. ) = v ) )
58 necom 
 |-  ( .0. =/= ( h ` v ) <-> ( h ` v ) =/= .0. )
59 eqcom 
 |-  ( v = ( iota_ c e. I ( h ` c ) =/= .0. ) <-> ( iota_ c e. I ( h ` c ) =/= .0. ) = v )
60 57 58 59 3bitr4g 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> ( .0. =/= ( h ` v ) <-> v = ( iota_ c e. I ( h ` c ) =/= .0. ) ) )
61 60 biimpd 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> ( .0. =/= ( h ` v ) -> v = ( iota_ c e. I ( h ` c ) =/= .0. ) ) )
62 61 necon1bd 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> ( -. v = ( iota_ c e. I ( h ` c ) =/= .0. ) -> .0. = ( h ` v ) ) )
63 62 imp 
 |-  ( ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) /\ -. v = ( iota_ c e. I ( h ` c ) =/= .0. ) ) -> .0. = ( h ` v ) )
64 51 63 ifeqda 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> if ( v = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` v ) , .0. ) = ( h ` v ) )
65 50 64 eqtr2d 
 |-  ( ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) /\ v e. I ) -> ( h ` v ) = ( ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) ` v ) )
66 40 45 65 eqfnfvd 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> h = ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) )
67 riotacl 
 |-  ( E! c e. I ( h ` c ) =/= .0. -> ( iota_ c e. I ( h ` c ) =/= .0. ) e. I )
68 67 adantl 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> ( iota_ c e. I ( h ` c ) =/= .0. ) e. I )
69 elmapi 
 |-  ( h e. ( B ^m I ) -> h : I --> B )
70 69 ad2antlr 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> h : I --> B )
71 70 68 ffvelrnd 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) e. B )
72 7 ralrimivva 
 |-  ( ph -> A. a e. I A. b e. B ( x e. I |-> if ( x = a , b , .0. ) ) e. H )
73 72 ad2antrr 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> A. a e. I A. b e. B ( x e. I |-> if ( x = a , b , .0. ) ) e. H )
74 eqeq2 
 |-  ( a = ( iota_ c e. I ( h ` c ) =/= .0. ) -> ( x = a <-> x = ( iota_ c e. I ( h ` c ) =/= .0. ) ) )
75 74 ifbid 
 |-  ( a = ( iota_ c e. I ( h ` c ) =/= .0. ) -> if ( x = a , b , .0. ) = if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , b , .0. ) )
76 75 mpteq2dv 
 |-  ( a = ( iota_ c e. I ( h ` c ) =/= .0. ) -> ( x e. I |-> if ( x = a , b , .0. ) ) = ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , b , .0. ) ) )
77 76 eleq1d 
 |-  ( a = ( iota_ c e. I ( h ` c ) =/= .0. ) -> ( ( x e. I |-> if ( x = a , b , .0. ) ) e. H <-> ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , b , .0. ) ) e. H ) )
78 fveq2 
 |-  ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) -> ( h ` x ) = ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) )
79 78 eqeq2d 
 |-  ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) -> ( b = ( h ` x ) <-> b = ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) ) )
80 79 biimparc 
 |-  ( ( b = ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) /\ x = ( iota_ c e. I ( h ` c ) =/= .0. ) ) -> b = ( h ` x ) )
81 80 ifeq1da 
 |-  ( b = ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) -> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , b , .0. ) = if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) )
82 81 mpteq2dv 
 |-  ( b = ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) -> ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , b , .0. ) ) = ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) )
83 82 eleq1d 
 |-  ( b = ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) -> ( ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , b , .0. ) ) e. H <-> ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) e. H ) )
84 77 83 rspc2va 
 |-  ( ( ( ( iota_ c e. I ( h ` c ) =/= .0. ) e. I /\ ( h ` ( iota_ c e. I ( h ` c ) =/= .0. ) ) e. B ) /\ A. a e. I A. b e. B ( x e. I |-> if ( x = a , b , .0. ) ) e. H ) -> ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) e. H )
85 68 71 73 84 syl21anc 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> ( x e. I |-> if ( x = ( iota_ c e. I ( h ` c ) =/= .0. ) , ( h ` x ) , .0. ) ) e. H )
86 66 85 eqeltrd 
 |-  ( ( ( ph /\ h e. ( B ^m I ) ) /\ E! c e. I ( h ` c ) =/= .0. ) -> h e. H )
87 86 ex 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> ( E! c e. I ( h ` c ) =/= .0. -> h e. H ) )
88 39 87 sylbid 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> ( E! c c e. ( h supp .0. ) -> h e. H ) )
89 29 88 syl5bi 
 |-  ( ( ph /\ h e. ( B ^m I ) ) -> ( 1 = ( # ` ( h supp .0. ) ) -> h e. H ) )
90 89 ralrimiva 
 |-  ( ph -> A. h e. ( B ^m I ) ( 1 = ( # ` ( h supp .0. ) ) -> h e. H ) )
91 1 2 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
92 4 91 syl 
 |-  ( ph -> .0. e. B )
93 92 ad5antr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ x e. I ) -> .0. e. B )
94 eqid 
 |-  ( B ^m I ) = ( B ^m I )
95 simprl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> l e. ( B ^m I ) )
96 95 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ x e. I ) -> l e. ( B ^m I ) )
97 simpr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ x e. I ) -> x e. I )
98 94 96 97 mapfvd 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ x e. I ) -> ( l ` x ) e. B )
99 93 98 ifcld 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ x e. I ) -> if ( x = z , .0. , ( l ` x ) ) e. B )
100 99 fmpttd 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) : I --> B )
101 9 a1i 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> B e. _V )
102 5 ad4antr 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> I e. V )
103 101 102 elmapd 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) e. ( B ^m I ) <-> ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) : I --> B ) )
104 100 103 mpbird 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) e. ( B ^m I ) )
105 104 adantrl 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) e. ( B ^m I ) )
106 fvoveq1 
 |-  ( m = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) -> ( # ` ( m supp .0. ) ) = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) )
107 106 eqeq2d 
 |-  ( m = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) -> ( j = ( # ` ( m supp .0. ) ) <-> j = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) ) )
108 oveq1 
 |-  ( m = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) -> ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) )
109 108 eqeq2d 
 |-  ( m = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) -> ( l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) <-> l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
110 107 109 anbi12d 
 |-  ( m = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) -> ( ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) <-> ( j = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) /\ l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) )
111 110 adantl 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) /\ m = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ) -> ( ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) <-> ( j = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) /\ l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) )
112 ovexd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( l supp .0. ) e. _V )
113 simprl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> z e. I )
114 simprr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( l ` z ) =/= .0. )
115 elmapfn 
 |-  ( l e. ( B ^m I ) -> l Fn I )
116 115 ad2antrl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> l Fn I )
117 116 adantr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> l Fn I )
118 5 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> I e. V )
119 33 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> .0. e. _V )
120 elsuppfn 
 |-  ( ( l Fn I /\ I e. V /\ .0. e. _V ) -> ( z e. ( l supp .0. ) <-> ( z e. I /\ ( l ` z ) =/= .0. ) ) )
121 117 118 119 120 syl3anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( z e. ( l supp .0. ) <-> ( z e. I /\ ( l ` z ) =/= .0. ) ) )
122 113 114 121 mpbir2and 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> z e. ( l supp .0. ) )
123 simpllr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> j e. NN )
124 123 nnnn0d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> j e. NN0 )
125 simplrr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( j + 1 ) = ( # ` ( l supp .0. ) ) )
126 125 eqcomd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( # ` ( l supp .0. ) ) = ( j + 1 ) )
127 hashdifsnp1 
 |-  ( ( ( l supp .0. ) e. _V /\ z e. ( l supp .0. ) /\ j e. NN0 ) -> ( ( # ` ( l supp .0. ) ) = ( j + 1 ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = j ) )
128 127 imp 
 |-  ( ( ( ( l supp .0. ) e. _V /\ z e. ( l supp .0. ) /\ j e. NN0 ) /\ ( # ` ( l supp .0. ) ) = ( j + 1 ) ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = j )
129 112 122 124 126 128 syl31anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = j )
130 eldifsn 
 |-  ( v e. ( ( l supp .0. ) \ { z } ) <-> ( v e. ( l supp .0. ) /\ v =/= z ) )
131 fvex 
 |-  ( l ` x ) e. _V
132 33 131 ifex 
 |-  if ( x = z , .0. , ( l ` x ) ) e. _V
133 eqid 
 |-  ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) )
134 132 133 fnmpti 
 |-  ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) Fn I
135 134 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) Fn I )
136 5 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> I e. V )
137 33 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> .0. e. _V )
138 elsuppfn 
 |-  ( ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) Fn I /\ I e. V /\ .0. e. _V ) -> ( v e. ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) <-> ( v e. I /\ ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) =/= .0. ) ) )
139 135 136 137 138 syl3anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( v e. ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) <-> ( v e. I /\ ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) =/= .0. ) ) )
140 iftrue 
 |-  ( v = z -> if ( v = z , .0. , ( l ` v ) ) = .0. )
141 olc 
 |-  ( v = z -> ( ( l ` v ) = .0. \/ v = z ) )
142 140 141 2thd 
 |-  ( v = z -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
143 iffalse 
 |-  ( -. v = z -> if ( v = z , .0. , ( l ` v ) ) = ( l ` v ) )
144 143 eqeq1d 
 |-  ( -. v = z -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( l ` v ) = .0. ) )
145 biorf 
 |-  ( -. v = z -> ( ( l ` v ) = .0. <-> ( v = z \/ ( l ` v ) = .0. ) ) )
146 orcom 
 |-  ( ( ( l ` v ) = .0. \/ v = z ) <-> ( v = z \/ ( l ` v ) = .0. ) )
147 145 146 bitr4di 
 |-  ( -. v = z -> ( ( l ` v ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
148 144 147 bitrd 
 |-  ( -. v = z -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
149 142 148 pm2.61i 
 |-  ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) )
150 149 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
151 150 necon3abid 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( if ( v = z , .0. , ( l ` v ) ) =/= .0. <-> -. ( ( l ` v ) = .0. \/ v = z ) ) )
152 neanior 
 |-  ( ( ( l ` v ) =/= .0. /\ v =/= z ) <-> -. ( ( l ` v ) = .0. \/ v = z ) )
153 151 152 bitr4di 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( if ( v = z , .0. , ( l ` v ) ) =/= .0. <-> ( ( l ` v ) =/= .0. /\ v =/= z ) ) )
154 153 anbi2d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( v e. I /\ if ( v = z , .0. , ( l ` v ) ) =/= .0. ) <-> ( v e. I /\ ( ( l ` v ) =/= .0. /\ v =/= z ) ) ) )
155 anass 
 |-  ( ( ( v e. I /\ ( l ` v ) =/= .0. ) /\ v =/= z ) <-> ( v e. I /\ ( ( l ` v ) =/= .0. /\ v =/= z ) ) )
156 154 155 bitr4di 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( v e. I /\ if ( v = z , .0. , ( l ` v ) ) =/= .0. ) <-> ( ( v e. I /\ ( l ` v ) =/= .0. ) /\ v =/= z ) ) )
157 equequ1 
 |-  ( x = v -> ( x = z <-> v = z ) )
158 fveq2 
 |-  ( x = v -> ( l ` x ) = ( l ` v ) )
159 157 158 ifbieq2d 
 |-  ( x = v -> if ( x = z , .0. , ( l ` x ) ) = if ( v = z , .0. , ( l ` v ) ) )
160 159 133 132 fvmpt3i 
 |-  ( v e. I -> ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) = if ( v = z , .0. , ( l ` v ) ) )
161 160 adantl 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) = if ( v = z , .0. , ( l ` v ) ) )
162 161 neeq1d 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) =/= .0. <-> if ( v = z , .0. , ( l ` v ) ) =/= .0. ) )
163 162 pm5.32da 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( v e. I /\ ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) =/= .0. ) <-> ( v e. I /\ if ( v = z , .0. , ( l ` v ) ) =/= .0. ) ) )
164 116 adantr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> l Fn I )
165 elsuppfn 
 |-  ( ( l Fn I /\ I e. V /\ .0. e. _V ) -> ( v e. ( l supp .0. ) <-> ( v e. I /\ ( l ` v ) =/= .0. ) ) )
166 164 136 137 165 syl3anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( v e. ( l supp .0. ) <-> ( v e. I /\ ( l ` v ) =/= .0. ) ) )
167 166 anbi1d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( v e. ( l supp .0. ) /\ v =/= z ) <-> ( ( v e. I /\ ( l ` v ) =/= .0. ) /\ v =/= z ) ) )
168 156 163 167 3bitr4d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( v e. I /\ ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) =/= .0. ) <-> ( v e. ( l supp .0. ) /\ v =/= z ) ) )
169 139 168 bitr2d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( v e. ( l supp .0. ) /\ v =/= z ) <-> v e. ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) )
170 130 169 syl5bb 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( v e. ( ( l supp .0. ) \ { z } ) <-> v e. ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) )
171 170 eqrdv 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( l supp .0. ) \ { z } ) = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) )
172 171 fveq2d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) )
173 172 adantrl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) )
174 129 173 eqtr3d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> j = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) )
175 131 33 ifex 
 |-  if ( x = z , ( l ` x ) , .0. ) e. _V
176 eqid 
 |-  ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) = ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) )
177 175 176 fnmpti 
 |-  ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) Fn I
178 177 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) Fn I )
179 inidm 
 |-  ( I i^i I ) = I
180 135 178 136 136 179 offn 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) Fn I )
181 157 158 ifbieq1d 
 |-  ( x = v -> if ( x = z , ( l ` x ) , .0. ) = if ( v = z , ( l ` v ) , .0. ) )
182 181 176 175 fvmpt3i 
 |-  ( v e. I -> ( ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ` v ) = if ( v = z , ( l ` v ) , .0. ) )
183 182 adantl 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ` v ) = if ( v = z , ( l ` v ) , .0. ) )
184 135 178 136 136 179 161 183 ofval 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ` v ) = ( if ( v = z , .0. , ( l ` v ) ) .+ if ( v = z , ( l ` v ) , .0. ) ) )
185 4 ad4antr 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> G e. Grp )
186 simplrl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( ( l ` z ) =/= .0. /\ v e. I ) ) -> l e. ( B ^m I ) )
187 186 anassrs 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> l e. ( B ^m I ) )
188 simpr 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> v e. I )
189 94 187 188 mapfvd 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( l ` v ) e. B )
190 1 3 2 grplid 
 |-  ( ( G e. Grp /\ ( l ` v ) e. B ) -> ( .0. .+ ( l ` v ) ) = ( l ` v ) )
191 1 3 2 grprid 
 |-  ( ( G e. Grp /\ ( l ` v ) e. B ) -> ( ( l ` v ) .+ .0. ) = ( l ` v ) )
192 190 191 ifeq12d 
 |-  ( ( G e. Grp /\ ( l ` v ) e. B ) -> if ( v = z , ( .0. .+ ( l ` v ) ) , ( ( l ` v ) .+ .0. ) ) = if ( v = z , ( l ` v ) , ( l ` v ) ) )
193 185 189 192 syl2anc 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> if ( v = z , ( .0. .+ ( l ` v ) ) , ( ( l ` v ) .+ .0. ) ) = if ( v = z , ( l ` v ) , ( l ` v ) ) )
194 ovif12 
 |-  ( if ( v = z , .0. , ( l ` v ) ) .+ if ( v = z , ( l ` v ) , .0. ) ) = if ( v = z , ( .0. .+ ( l ` v ) ) , ( ( l ` v ) .+ .0. ) )
195 ifid 
 |-  if ( v = z , ( l ` v ) , ( l ` v ) ) = ( l ` v )
196 195 eqcomi 
 |-  ( l ` v ) = if ( v = z , ( l ` v ) , ( l ` v ) )
197 193 194 196 3eqtr4g 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( if ( v = z , .0. , ( l ` v ) ) .+ if ( v = z , ( l ` v ) , .0. ) ) = ( l ` v ) )
198 184 197 eqtr2d 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> ( l ` v ) = ( ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ` v ) )
199 164 180 198 eqfnfvd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) )
200 199 adantrl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) )
201 174 200 jca 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( j = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) /\ l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
202 201 adantllr 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( j = ( # ` ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) supp .0. ) ) /\ l = ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
203 105 111 202 rspcedvd 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> E. m e. ( B ^m I ) ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
204 115 ad2antrl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> l Fn I )
205 5 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> I e. V )
206 33 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> .0. e. _V )
207 suppvalfn 
 |-  ( ( l Fn I /\ I e. V /\ .0. e. _V ) -> ( l supp .0. ) = { z e. I | ( l ` z ) =/= .0. } )
208 204 205 206 207 syl3anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( l supp .0. ) = { z e. I | ( l ` z ) =/= .0. } )
209 simprr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( j + 1 ) = ( # ` ( l supp .0. ) ) )
210 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
211 210 ad3antlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( j + 1 ) e. NN )
212 211 nnne0d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( j + 1 ) =/= 0 )
213 209 212 eqnetrrd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( # ` ( l supp .0. ) ) =/= 0 )
214 ovex 
 |-  ( l supp .0. ) e. _V
215 hasheq0 
 |-  ( ( l supp .0. ) e. _V -> ( ( # ` ( l supp .0. ) ) = 0 <-> ( l supp .0. ) = (/) ) )
216 215 necon3bid 
 |-  ( ( l supp .0. ) e. _V -> ( ( # ` ( l supp .0. ) ) =/= 0 <-> ( l supp .0. ) =/= (/) ) )
217 214 216 mp1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( ( # ` ( l supp .0. ) ) =/= 0 <-> ( l supp .0. ) =/= (/) ) )
218 213 217 mpbid 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( l supp .0. ) =/= (/) )
219 208 218 eqnetrrd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> { z e. I | ( l ` z ) =/= .0. } =/= (/) )
220 rabn0 
 |-  ( { z e. I | ( l ` z ) =/= .0. } =/= (/) <-> E. z e. I ( l ` z ) =/= .0. )
221 219 220 sylib 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> E. z e. I ( l ` z ) =/= .0. )
222 203 221 reximddv 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> E. z e. I E. m e. ( B ^m I ) ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
223 rexcom 
 |-  ( E. z e. I E. m e. ( B ^m I ) ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) <-> E. m e. ( B ^m I ) E. z e. I ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
224 222 223 sylib 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> E. m e. ( B ^m I ) E. z e. I ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) )
225 simprr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) )
226 fvoveq1 
 |-  ( h = m -> ( # ` ( h supp .0. ) ) = ( # ` ( m supp .0. ) ) )
227 226 eqeq2d 
 |-  ( h = m -> ( j = ( # ` ( h supp .0. ) ) <-> j = ( # ` ( m supp .0. ) ) ) )
228 eleq1w 
 |-  ( h = m -> ( h e. H <-> m e. H ) )
229 227 228 imbi12d 
 |-  ( h = m -> ( ( j = ( # ` ( h supp .0. ) ) -> h e. H ) <-> ( j = ( # ` ( m supp .0. ) ) -> m e. H ) ) )
230 229 rspccva 
 |-  ( ( A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) /\ m e. ( B ^m I ) ) -> ( j = ( # ` ( m supp .0. ) ) -> m e. H ) )
231 230 adantll 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ m e. ( B ^m I ) ) -> ( j = ( # ` ( m supp .0. ) ) -> m e. H ) )
232 231 imp 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ m e. ( B ^m I ) ) /\ j = ( # ` ( m supp .0. ) ) ) -> m e. H )
233 232 adantllr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ m e. ( B ^m I ) ) /\ j = ( # ` ( m supp .0. ) ) ) -> m e. H )
234 233 adantlrr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ j = ( # ` ( m supp .0. ) ) ) -> m e. H )
235 234 adantrr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> m e. H )
236 simplrr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> z e. I )
237 95 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> l e. ( B ^m I ) )
238 94 237 236 mapfvd 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> ( l ` z ) e. B )
239 72 ad5antr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> A. a e. I A. b e. B ( x e. I |-> if ( x = a , b , .0. ) ) e. H )
240 equequ2 
 |-  ( a = z -> ( x = a <-> x = z ) )
241 240 ifbid 
 |-  ( a = z -> if ( x = a , b , .0. ) = if ( x = z , b , .0. ) )
242 241 mpteq2dv 
 |-  ( a = z -> ( x e. I |-> if ( x = a , b , .0. ) ) = ( x e. I |-> if ( x = z , b , .0. ) ) )
243 242 eleq1d 
 |-  ( a = z -> ( ( x e. I |-> if ( x = a , b , .0. ) ) e. H <-> ( x e. I |-> if ( x = z , b , .0. ) ) e. H ) )
244 fveq2 
 |-  ( x = z -> ( l ` x ) = ( l ` z ) )
245 244 eqeq2d 
 |-  ( x = z -> ( b = ( l ` x ) <-> b = ( l ` z ) ) )
246 245 biimparc 
 |-  ( ( b = ( l ` z ) /\ x = z ) -> b = ( l ` x ) )
247 246 ifeq1da 
 |-  ( b = ( l ` z ) -> if ( x = z , b , .0. ) = if ( x = z , ( l ` x ) , .0. ) )
248 247 mpteq2dv 
 |-  ( b = ( l ` z ) -> ( x e. I |-> if ( x = z , b , .0. ) ) = ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) )
249 248 eleq1d 
 |-  ( b = ( l ` z ) -> ( ( x e. I |-> if ( x = z , b , .0. ) ) e. H <-> ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) e. H ) )
250 243 249 rspc2va 
 |-  ( ( ( z e. I /\ ( l ` z ) e. B ) /\ A. a e. I A. b e. B ( x e. I |-> if ( x = a , b , .0. ) ) e. H ) -> ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) e. H )
251 236 238 239 250 syl21anc 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) e. H )
252 8 ralrimivva 
 |-  ( ph -> A. x e. H A. y e. H ( x oF .+ y ) e. H )
253 252 ad5antr 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> A. x e. H A. y e. H ( x oF .+ y ) e. H )
254 ovrspc2v 
 |-  ( ( ( m e. H /\ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) e. H ) /\ A. x e. H A. y e. H ( x oF .+ y ) e. H ) -> ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) e. H )
255 235 251 253 254 syl21anc 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) e. H )
256 225 255 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) /\ ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) ) -> l e. H )
257 256 ex 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( m e. ( B ^m I ) /\ z e. I ) ) -> ( ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) -> l e. H ) )
258 257 rexlimdvva 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> ( E. m e. ( B ^m I ) E. z e. I ( j = ( # ` ( m supp .0. ) ) /\ l = ( m oF .+ ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ) ) -> l e. H ) )
259 224 258 mpd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> l e. H )
260 259 exp32 
 |-  ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) -> ( l e. ( B ^m I ) -> ( ( j + 1 ) = ( # ` ( l supp .0. ) ) -> l e. H ) ) )
261 260 ralrimiv 
 |-  ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) -> A. l e. ( B ^m I ) ( ( j + 1 ) = ( # ` ( l supp .0. ) ) -> l e. H ) )
262 fvoveq1 
 |-  ( l = h -> ( # ` ( l supp .0. ) ) = ( # ` ( h supp .0. ) ) )
263 262 eqeq2d 
 |-  ( l = h -> ( ( j + 1 ) = ( # ` ( l supp .0. ) ) <-> ( j + 1 ) = ( # ` ( h supp .0. ) ) ) )
264 eleq1w 
 |-  ( l = h -> ( l e. H <-> h e. H ) )
265 263 264 imbi12d 
 |-  ( l = h -> ( ( ( j + 1 ) = ( # ` ( l supp .0. ) ) -> l e. H ) <-> ( ( j + 1 ) = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
266 265 cbvralvw 
 |-  ( A. l e. ( B ^m I ) ( ( j + 1 ) = ( # ` ( l supp .0. ) ) -> l e. H ) <-> A. h e. ( B ^m I ) ( ( j + 1 ) = ( # ` ( h supp .0. ) ) -> h e. H ) )
267 261 266 sylib 
 |-  ( ( ( ph /\ j e. NN ) /\ A. h e. ( B ^m I ) ( j = ( # ` ( h supp .0. ) ) -> h e. H ) ) -> A. h e. ( B ^m I ) ( ( j + 1 ) = ( # ` ( h supp .0. ) ) -> h e. H ) )
268 15 18 21 24 90 267 nnindd 
 |-  ( ( ph /\ n e. NN ) -> A. h e. ( B ^m I ) ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
269 268 ralrimiva 
 |-  ( ph -> A. n e. NN A. h e. ( B ^m I ) ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
270 ralcom 
 |-  ( A. n e. NN A. h e. ( B ^m I ) ( n = ( # ` ( h supp .0. ) ) -> h e. H ) <-> A. h e. ( B ^m I ) A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
271 269 270 sylib 
 |-  ( ph -> A. h e. ( B ^m I ) A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
272 biidd 
 |-  ( n = ( # ` ( h supp .0. ) ) -> ( h e. H <-> h e. H ) )
273 272 ceqsralv 
 |-  ( ( # ` ( h supp .0. ) ) e. NN -> ( A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) <-> h e. H ) )
274 273 biimpcd 
 |-  ( A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) -> ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) )
275 274 ralimi 
 |-  ( A. h e. ( B ^m I ) A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) -> A. h e. ( B ^m I ) ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) )
276 271 275 syl 
 |-  ( ph -> A. h e. ( B ^m I ) ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) )
277 fvoveq1 
 |-  ( h = X -> ( # ` ( h supp .0. ) ) = ( # ` ( X supp .0. ) ) )
278 277 eleq1d 
 |-  ( h = X -> ( ( # ` ( h supp .0. ) ) e. NN <-> ( # ` ( X supp .0. ) ) e. NN ) )
279 eleq1 
 |-  ( h = X -> ( h e. H <-> X e. H ) )
280 278 279 imbi12d 
 |-  ( h = X -> ( ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) <-> ( ( # ` ( X supp .0. ) ) e. NN -> X e. H ) ) )
281 280 rspcv 
 |-  ( X e. ( B ^m I ) -> ( A. h e. ( B ^m I ) ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) -> ( ( # ` ( X supp .0. ) ) e. NN -> X e. H ) ) )
282 276 281 syl5com 
 |-  ( ph -> ( X e. ( B ^m I ) -> ( ( # ` ( X supp .0. ) ) e. NN -> X e. H ) ) )
283 282 com23 
 |-  ( ph -> ( ( # ` ( X supp .0. ) ) e. NN -> ( X e. ( B ^m I ) -> X e. H ) ) )
284 283 imp 
 |-  ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) -> ( X e. ( B ^m I ) -> X e. H ) )
285 12 284 sylbird 
 |-  ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) -> ( X : I --> B -> X e. H ) )
286 285 imp 
 |-  ( ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) /\ X : I --> B ) -> X e. H )
287 286 an32s 
 |-  ( ( ( ph /\ X : I --> B ) /\ ( # ` ( X supp .0. ) ) e. NN ) -> X e. H )
288 287 adantlr 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( # ` ( X supp .0. ) ) e. NN ) -> X e. H )
289 ovex 
 |-  ( X supp .0. ) e. _V
290 hasheq0 
 |-  ( ( X supp .0. ) e. _V -> ( ( # ` ( X supp .0. ) ) = 0 <-> ( X supp .0. ) = (/) ) )
291 289 290 ax-mp 
 |-  ( ( # ` ( X supp .0. ) ) = 0 <-> ( X supp .0. ) = (/) )
292 ffn 
 |-  ( X : I --> B -> X Fn I )
293 292 ad2antlr 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> X Fn I )
294 5 ad2antrr 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> I e. V )
295 33 a1i 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> .0. e. _V )
296 fnsuppeq0 
 |-  ( ( X Fn I /\ I e. V /\ .0. e. _V ) -> ( ( X supp .0. ) = (/) <-> X = ( I X. { .0. } ) ) )
297 293 294 295 296 syl3anc 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( ( X supp .0. ) = (/) <-> X = ( I X. { .0. } ) ) )
298 297 biimpa 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( X supp .0. ) = (/) ) -> X = ( I X. { .0. } ) )
299 6 ad3antrrr 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( X supp .0. ) = (/) ) -> ( I X. { .0. } ) e. H )
300 298 299 eqeltrd 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( X supp .0. ) = (/) ) -> X e. H )
301 291 300 sylan2b 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( # ` ( X supp .0. ) ) = 0 ) -> X e. H )
302 simpr 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> X finSupp .0. )
303 302 fsuppimpd 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( X supp .0. ) e. Fin )
304 hashcl 
 |-  ( ( X supp .0. ) e. Fin -> ( # ` ( X supp .0. ) ) e. NN0 )
305 303 304 syl 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( # ` ( X supp .0. ) ) e. NN0 )
306 elnn0 
 |-  ( ( # ` ( X supp .0. ) ) e. NN0 <-> ( ( # ` ( X supp .0. ) ) e. NN \/ ( # ` ( X supp .0. ) ) = 0 ) )
307 305 306 sylib 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( ( # ` ( X supp .0. ) ) e. NN \/ ( # ` ( X supp .0. ) ) = 0 ) )
308 288 301 307 mpjaodan 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> X e. H )
309 308 anasss 
 |-  ( ( ph /\ ( X : I --> B /\ X finSupp .0. ) ) -> X e. H )