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

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 ffvelcdmd 
 |-  ( ( ( 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 biimtrid 
 |-  ( ( 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 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. ) ) )
92 91 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. ) ) ) )
93 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. ) ) ) )
94 93 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. ) ) ) ) )
95 92 94 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. ) ) ) ) ) )
96 1 2 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
97 4 96 syl 
 |-  ( ph -> .0. e. B )
98 97 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 )
99 eqid 
 |-  ( B ^m I ) = ( B ^m I )
100 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 ) )
101 100 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 ) )
102 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 )
103 99 101 102 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 )
104 98 103 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 )
105 104 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 )
106 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 )
107 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 )
108 106 107 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 ) )
109 105 108 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 ) )
110 109 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 ) )
111 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 )
112 simprl 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> z e. I )
113 simprr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> ( l ` z ) =/= .0. )
114 elmapfn 
 |-  ( l e. ( B ^m I ) -> l Fn I )
115 114 ad2antrl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) -> l Fn I )
116 115 adantr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> l Fn I )
117 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 )
118 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 )
119 elsuppfn 
 |-  ( ( l Fn I /\ I e. V /\ .0. e. _V ) -> ( z e. ( l supp .0. ) <-> ( z e. I /\ ( l ` z ) =/= .0. ) ) )
120 116 117 118 119 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. ) ) )
121 112 113 120 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. ) )
122 simpllr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> j e. NN )
123 122 nnnn0d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( z e. I /\ ( l ` z ) =/= .0. ) ) -> j e. NN0 )
124 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. ) ) )
125 124 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 ) )
126 hashdifsnp1 
 |-  ( ( ( l supp .0. ) e. _V /\ z e. ( l supp .0. ) /\ j e. NN0 ) -> ( ( # ` ( l supp .0. ) ) = ( j + 1 ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = j ) )
127 126 imp 
 |-  ( ( ( ( l supp .0. ) e. _V /\ z e. ( l supp .0. ) /\ j e. NN0 ) /\ ( # ` ( l supp .0. ) ) = ( j + 1 ) ) -> ( # ` ( ( l supp .0. ) \ { z } ) ) = j )
128 111 121 123 125 127 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 )
129 eldifsn 
 |-  ( v e. ( ( l supp .0. ) \ { z } ) <-> ( v e. ( l supp .0. ) /\ v =/= z ) )
130 fvex 
 |-  ( l ` x ) e. _V
131 33 130 ifex 
 |-  if ( x = z , .0. , ( l ` x ) ) e. _V
132 eqid 
 |-  ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) = ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) )
133 131 132 fnmpti 
 |-  ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) Fn I
134 133 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 )
135 5 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> I e. V )
136 33 a1i 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> .0. e. _V )
137 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. ) ) )
138 134 135 136 137 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. ) ) )
139 iftrue 
 |-  ( v = z -> if ( v = z , .0. , ( l ` v ) ) = .0. )
140 olc 
 |-  ( v = z -> ( ( l ` v ) = .0. \/ v = z ) )
141 139 140 2thd 
 |-  ( v = z -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
142 iffalse 
 |-  ( -. v = z -> if ( v = z , .0. , ( l ` v ) ) = ( l ` v ) )
143 142 eqeq1d 
 |-  ( -. v = z -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( l ` v ) = .0. ) )
144 biorf 
 |-  ( -. v = z -> ( ( l ` v ) = .0. <-> ( v = z \/ ( l ` v ) = .0. ) ) )
145 orcom 
 |-  ( ( ( l ` v ) = .0. \/ v = z ) <-> ( v = z \/ ( l ` v ) = .0. ) )
146 144 145 bitr4di 
 |-  ( -. v = z -> ( ( l ` v ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
147 143 146 bitrd 
 |-  ( -. v = z -> ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) ) )
148 141 147 pm2.61i 
 |-  ( if ( v = z , .0. , ( l ` v ) ) = .0. <-> ( ( l ` v ) = .0. \/ v = z ) )
149 148 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 ) ) )
150 149 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 ) ) )
151 neanior 
 |-  ( ( ( l ` v ) =/= .0. /\ v =/= z ) <-> -. ( ( l ` v ) = .0. \/ v = z ) )
152 150 151 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 ) ) )
153 152 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 ) ) ) )
154 anass 
 |-  ( ( ( v e. I /\ ( l ` v ) =/= .0. ) /\ v =/= z ) <-> ( v e. I /\ ( ( l ` v ) =/= .0. /\ v =/= z ) ) )
155 153 154 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 ) ) )
156 equequ1 
 |-  ( x = v -> ( x = z <-> v = z ) )
157 fveq2 
 |-  ( x = v -> ( l ` x ) = ( l ` v ) )
158 156 157 ifbieq2d 
 |-  ( x = v -> if ( x = z , .0. , ( l ` x ) ) = if ( v = z , .0. , ( l ` v ) ) )
159 158 132 131 fvmpt3i 
 |-  ( v e. I -> ( ( x e. I |-> if ( x = z , .0. , ( l ` x ) ) ) ` v ) = if ( v = z , .0. , ( l ` v ) ) )
160 159 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 ) ) )
161 160 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. ) )
162 161 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. ) ) )
163 115 adantr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) -> l Fn I )
164 elsuppfn 
 |-  ( ( l Fn I /\ I e. V /\ .0. e. _V ) -> ( v e. ( l supp .0. ) <-> ( v e. I /\ ( l ` v ) =/= .0. ) ) )
165 163 135 136 164 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. ) ) )
166 165 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 ) ) )
167 155 162 166 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 ) ) )
168 138 167 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. ) ) )
169 129 168 bitrid 
 |-  ( ( ( ( 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. ) ) )
170 169 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. ) )
171 170 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. ) ) )
172 171 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. ) ) )
173 128 172 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. ) ) )
174 130 33 ifex 
 |-  if ( x = z , ( l ` x ) , .0. ) e. _V
175 eqid 
 |-  ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) = ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) )
176 174 175 fnmpti 
 |-  ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) Fn I
177 176 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 )
178 inidm 
 |-  ( I i^i I ) = I
179 134 177 135 135 178 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 )
180 156 157 ifbieq1d 
 |-  ( x = v -> if ( x = z , ( l ` x ) , .0. ) = if ( v = z , ( l ` v ) , .0. ) )
181 180 175 174 fvmpt3i 
 |-  ( v e. I -> ( ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) ` v ) = if ( v = z , ( l ` v ) , .0. ) )
182 181 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. ) )
183 134 177 135 135 178 160 182 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. ) ) )
184 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 )
185 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 ) )
186 185 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 ) )
187 simpr 
 |-  ( ( ( ( ( ph /\ j e. NN ) /\ ( l e. ( B ^m I ) /\ ( j + 1 ) = ( # ` ( l supp .0. ) ) ) ) /\ ( l ` z ) =/= .0. ) /\ v e. I ) -> v e. I )
188 99 186 187 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 )
189 1 3 2 grplid 
 |-  ( ( G e. Grp /\ ( l ` v ) e. B ) -> ( .0. .+ ( l ` v ) ) = ( l ` v ) )
190 1 3 2 grprid 
 |-  ( ( G e. Grp /\ ( l ` v ) e. B ) -> ( ( l ` v ) .+ .0. ) = ( l ` v ) )
191 189 190 ifeq12d 
 |-  ( ( G e. Grp /\ ( l ` v ) e. B ) -> if ( v = z , ( .0. .+ ( l ` v ) ) , ( ( l ` v ) .+ .0. ) ) = if ( v = z , ( l ` v ) , ( l ` v ) ) )
192 184 188 191 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 ) ) )
193 ovif12 
 |-  ( if ( v = z , .0. , ( l ` v ) ) .+ if ( v = z , ( l ` v ) , .0. ) ) = if ( v = z , ( .0. .+ ( l ` v ) ) , ( ( l ` v ) .+ .0. ) )
194 ifid 
 |-  if ( v = z , ( l ` v ) , ( l ` v ) ) = ( l ` v )
195 194 eqcomi 
 |-  ( l ` v ) = if ( v = z , ( l ` v ) , ( l ` v ) )
196 192 193 195 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 ) )
197 183 196 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 ) )
198 163 179 197 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. ) ) ) )
199 198 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. ) ) ) )
200 173 199 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. ) ) ) ) )
201 200 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. ) ) ) ) )
202 95 110 201 rspcedvdw 
 |-  ( ( ( ( ( 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. ) ) ) ) )
203 114 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 )
204 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 )
205 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 )
206 suppvalfn 
 |-  ( ( l Fn I /\ I e. V /\ .0. e. _V ) -> ( l supp .0. ) = { z e. I | ( l ` z ) =/= .0. } )
207 203 204 205 206 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. } )
208 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. ) ) )
209 peano2nn 
 |-  ( j e. NN -> ( j + 1 ) e. NN )
210 209 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 )
211 210 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 )
212 208 211 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 )
213 ovex 
 |-  ( l supp .0. ) e. _V
214 hasheq0 
 |-  ( ( l supp .0. ) e. _V -> ( ( # ` ( l supp .0. ) ) = 0 <-> ( l supp .0. ) = (/) ) )
215 214 necon3bid 
 |-  ( ( l supp .0. ) e. _V -> ( ( # ` ( l supp .0. ) ) =/= 0 <-> ( l supp .0. ) =/= (/) ) )
216 213 215 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. ) =/= (/) ) )
217 212 216 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. ) =/= (/) )
218 207 217 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. } =/= (/) )
219 rabn0 
 |-  ( { z e. I | ( l ` z ) =/= .0. } =/= (/) <-> E. z e. I ( l ` z ) =/= .0. )
220 218 219 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. )
221 202 220 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. ) ) ) ) )
222 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. ) ) ) ) )
223 221 222 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. ) ) ) ) )
224 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. ) ) ) )
225 fvoveq1 
 |-  ( h = m -> ( # ` ( h supp .0. ) ) = ( # ` ( m supp .0. ) ) )
226 225 eqeq2d 
 |-  ( h = m -> ( j = ( # ` ( h supp .0. ) ) <-> j = ( # ` ( m supp .0. ) ) ) )
227 eleq1w 
 |-  ( h = m -> ( h e. H <-> m e. H ) )
228 226 227 imbi12d 
 |-  ( h = m -> ( ( j = ( # ` ( h supp .0. ) ) -> h e. H ) <-> ( j = ( # ` ( m supp .0. ) ) -> m e. H ) ) )
229 228 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 ) )
230 229 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 ) )
231 230 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 )
232 231 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 )
233 232 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 )
234 233 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 )
235 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 )
236 100 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 ) )
237 99 236 235 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 )
238 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 )
239 equequ2 
 |-  ( a = z -> ( x = a <-> x = z ) )
240 239 ifbid 
 |-  ( a = z -> if ( x = a , b , .0. ) = if ( x = z , b , .0. ) )
241 240 mpteq2dv 
 |-  ( a = z -> ( x e. I |-> if ( x = a , b , .0. ) ) = ( x e. I |-> if ( x = z , b , .0. ) ) )
242 241 eleq1d 
 |-  ( a = z -> ( ( x e. I |-> if ( x = a , b , .0. ) ) e. H <-> ( x e. I |-> if ( x = z , b , .0. ) ) e. H ) )
243 fveq2 
 |-  ( x = z -> ( l ` x ) = ( l ` z ) )
244 243 eqeq2d 
 |-  ( x = z -> ( b = ( l ` x ) <-> b = ( l ` z ) ) )
245 244 biimparc 
 |-  ( ( b = ( l ` z ) /\ x = z ) -> b = ( l ` x ) )
246 245 ifeq1da 
 |-  ( b = ( l ` z ) -> if ( x = z , b , .0. ) = if ( x = z , ( l ` x ) , .0. ) )
247 246 mpteq2dv 
 |-  ( b = ( l ` z ) -> ( x e. I |-> if ( x = z , b , .0. ) ) = ( x e. I |-> if ( x = z , ( l ` x ) , .0. ) ) )
248 247 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 ) )
249 242 248 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 )
250 235 237 238 249 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 )
251 8 ralrimivva 
 |-  ( ph -> A. x e. H A. y e. H ( x oF .+ y ) e. H )
252 251 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 )
253 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 )
254 234 250 252 253 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 )
255 224 254 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 )
256 255 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 ) )
257 256 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 ) )
258 223 257 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 )
259 258 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 ) ) )
260 259 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 ) )
261 fvoveq1 
 |-  ( l = h -> ( # ` ( l supp .0. ) ) = ( # ` ( h supp .0. ) ) )
262 261 eqeq2d 
 |-  ( l = h -> ( ( j + 1 ) = ( # ` ( l supp .0. ) ) <-> ( j + 1 ) = ( # ` ( h supp .0. ) ) ) )
263 eleq1w 
 |-  ( l = h -> ( l e. H <-> h e. H ) )
264 262 263 imbi12d 
 |-  ( l = h -> ( ( ( j + 1 ) = ( # ` ( l supp .0. ) ) -> l e. H ) <-> ( ( j + 1 ) = ( # ` ( h supp .0. ) ) -> h e. H ) ) )
265 264 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 ) )
266 260 265 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 ) )
267 15 18 21 24 90 266 nnindd 
 |-  ( ( ph /\ n e. NN ) -> A. h e. ( B ^m I ) ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
268 267 ralrimiva 
 |-  ( ph -> A. n e. NN A. h e. ( B ^m I ) ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
269 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 ) )
270 268 269 sylib 
 |-  ( ph -> A. h e. ( B ^m I ) A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) )
271 biidd 
 |-  ( n = ( # ` ( h supp .0. ) ) -> ( h e. H <-> h e. H ) )
272 271 ceqsralv 
 |-  ( ( # ` ( h supp .0. ) ) e. NN -> ( A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) <-> h e. H ) )
273 272 biimpcd 
 |-  ( A. n e. NN ( n = ( # ` ( h supp .0. ) ) -> h e. H ) -> ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) )
274 273 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 ) )
275 270 274 syl 
 |-  ( ph -> A. h e. ( B ^m I ) ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) )
276 fvoveq1 
 |-  ( h = X -> ( # ` ( h supp .0. ) ) = ( # ` ( X supp .0. ) ) )
277 276 eleq1d 
 |-  ( h = X -> ( ( # ` ( h supp .0. ) ) e. NN <-> ( # ` ( X supp .0. ) ) e. NN ) )
278 eleq1 
 |-  ( h = X -> ( h e. H <-> X e. H ) )
279 277 278 imbi12d 
 |-  ( h = X -> ( ( ( # ` ( h supp .0. ) ) e. NN -> h e. H ) <-> ( ( # ` ( X supp .0. ) ) e. NN -> X e. H ) ) )
280 279 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 ) ) )
281 275 280 syl5com 
 |-  ( ph -> ( X e. ( B ^m I ) -> ( ( # ` ( X supp .0. ) ) e. NN -> X e. H ) ) )
282 281 com23 
 |-  ( ph -> ( ( # ` ( X supp .0. ) ) e. NN -> ( X e. ( B ^m I ) -> X e. H ) ) )
283 282 imp 
 |-  ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) -> ( X e. ( B ^m I ) -> X e. H ) )
284 12 283 sylbird 
 |-  ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) -> ( X : I --> B -> X e. H ) )
285 284 imp 
 |-  ( ( ( ph /\ ( # ` ( X supp .0. ) ) e. NN ) /\ X : I --> B ) -> X e. H )
286 285 an32s 
 |-  ( ( ( ph /\ X : I --> B ) /\ ( # ` ( X supp .0. ) ) e. NN ) -> X e. H )
287 286 adantlr 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( # ` ( X supp .0. ) ) e. NN ) -> X e. H )
288 ovex 
 |-  ( X supp .0. ) e. _V
289 hasheq0 
 |-  ( ( X supp .0. ) e. _V -> ( ( # ` ( X supp .0. ) ) = 0 <-> ( X supp .0. ) = (/) ) )
290 288 289 ax-mp 
 |-  ( ( # ` ( X supp .0. ) ) = 0 <-> ( X supp .0. ) = (/) )
291 ffn 
 |-  ( X : I --> B -> X Fn I )
292 291 ad2antlr 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> X Fn I )
293 5 ad2antrr 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> I e. V )
294 33 a1i 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> .0. e. _V )
295 fnsuppeq0 
 |-  ( ( X Fn I /\ I e. V /\ .0. e. _V ) -> ( ( X supp .0. ) = (/) <-> X = ( I X. { .0. } ) ) )
296 292 293 294 295 syl3anc 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( ( X supp .0. ) = (/) <-> X = ( I X. { .0. } ) ) )
297 296 biimpa 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( X supp .0. ) = (/) ) -> X = ( I X. { .0. } ) )
298 6 ad3antrrr 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( X supp .0. ) = (/) ) -> ( I X. { .0. } ) e. H )
299 297 298 eqeltrd 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( X supp .0. ) = (/) ) -> X e. H )
300 290 299 sylan2b 
 |-  ( ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) /\ ( # ` ( X supp .0. ) ) = 0 ) -> X e. H )
301 simpr 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> X finSupp .0. )
302 301 fsuppimpd 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( X supp .0. ) e. Fin )
303 hashcl 
 |-  ( ( X supp .0. ) e. Fin -> ( # ` ( X supp .0. ) ) e. NN0 )
304 302 303 syl 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( # ` ( X supp .0. ) ) e. NN0 )
305 elnn0 
 |-  ( ( # ` ( X supp .0. ) ) e. NN0 <-> ( ( # ` ( X supp .0. ) ) e. NN \/ ( # ` ( X supp .0. ) ) = 0 ) )
306 304 305 sylib 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> ( ( # ` ( X supp .0. ) ) e. NN \/ ( # ` ( X supp .0. ) ) = 0 ) )
307 287 300 306 mpjaodan 
 |-  ( ( ( ph /\ X : I --> B ) /\ X finSupp .0. ) -> X e. H )
308 307 anasss 
 |-  ( ( ph /\ ( X : I --> B /\ X finSupp .0. ) ) -> X e. H )