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 ˙ = 0 G
fsuppind.p ⊢ + ˙ = + G
fsuppind.g ⊢ φ → G ∈ Grp
fsuppind.v ⊢ φ → I ∈ V
fsuppind.0 ⊢ φ → I × 0 ˙ ∈ H
fsuppind.1 ⊢ φ ∧ a ∈ I ∧ b ∈ B → x ∈ I ⟼ if x = a b 0 ˙ ∈ H
fsuppind.2 ⊢ φ ∧ x ∈ H ∧ y ∈ H → x + ˙ f y ∈ H
Assertion fsuppind ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X ∈ H

Proof

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