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 ffvelrnd ⊢ φ ∧ 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 syl5bi ⊢ φ ∧ h ∈ B I → 1 = h supp 0 ˙ → h ∈ H
90 89 ralrimiva ⊢ φ → ∀ h ∈ B I 1 = h supp 0 ˙ → h ∈ H
91 1 2 grpidcl ⊢ G ∈ Grp → 0 ˙ ∈ B
92 4 91 syl ⊢ φ → 0 ˙ ∈ B
93 92 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
94 eqid ⊢ B I = B I
95 simprl ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → l ∈ B I
96 95 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
97 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
98 94 96 97 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
99 93 98 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
100 99 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
101 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
102 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
103 101 102 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
104 100 103 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
105 104 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
106 fvoveq1 ⊢ m = x ∈ I ⟼ if x = z 0 ˙ l ⁡ x → m supp 0 ˙ = x ∈ I ⟼ if x = z 0 ˙ l ⁡ x supp 0 ˙
107 106 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 ˙
108 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 ˙
109 108 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 ˙
110 107 109 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 ˙
111 110 adantl ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ ∧ 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 ˙
112 ovexd ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → l supp 0 ˙ ∈ V
113 simprl ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → z ∈ I
114 simprr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → l ⁡ z ≠ 0 ˙
115 elmapfn ⊢ l ∈ B I → l Fn I
116 115 ad2antrl ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → l Fn I
117 116 adantr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → l Fn I
118 5 ad3antrrr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → I ∈ V
119 33 a1i ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → 0 ˙ ∈ V
120 elsuppfn ⊢ l Fn I ∧ I ∈ V ∧ 0 ˙ ∈ V → z ∈ supp 0 ˙⁡ l ↔ z ∈ I ∧ l ⁡ z ≠ 0 ˙
121 117 118 119 120 syl3anc ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → z ∈ supp 0 ˙⁡ l ↔ z ∈ I ∧ l ⁡ z ≠ 0 ˙
122 113 114 121 mpbir2and ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → z ∈ supp 0 ˙⁡ l
123 simpllr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → j ∈ ℕ
124 123 nnnn0d ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → j ∈ ℕ 0
125 simplrr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → j + 1 = l supp 0 ˙
126 125 eqcomd ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → l supp 0 ˙ = j + 1
127 hashdifsnp1 ⊢ l supp 0 ˙ ∈ V ∧ z ∈ supp 0 ˙⁡ l ∧ j ∈ ℕ 0 → l supp 0 ˙ = j + 1 → supp 0 ˙⁡ l ∖ z = j
128 127 imp ⊢ l supp 0 ˙ ∈ V ∧ z ∈ supp 0 ˙⁡ l ∧ j ∈ ℕ 0 ∧ l supp 0 ˙ = j + 1 → supp 0 ˙⁡ l ∖ z = j
129 112 122 124 126 128 syl31anc ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ z ∈ I ∧ l ⁡ z ≠ 0 ˙ → supp 0 ˙⁡ l ∖ z = j
130 eldifsn ⊢ v ∈ supp 0 ˙⁡ l ∖ z ↔ v ∈ supp 0 ˙⁡ l ∧ v ≠ z
131 fvex ⊢ l ⁡ x ∈ V
132 33 131 ifex ⊢ if x = z 0 ˙ l ⁡ x ∈ V
133 eqid ⊢ x ∈ I ⟼ if x = z 0 ˙ l ⁡ x = x ∈ I ⟼ if x = z 0 ˙ l ⁡ x
134 132 133 fnmpti ⊢ x ∈ I ⟼ if x = z 0 ˙ l ⁡ x Fn I
135 134 a1i ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ → x ∈ I ⟼ if x = z 0 ˙ l ⁡ x Fn I
136 5 ad3antrrr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ → I ∈ V
137 33 a1i ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ → 0 ˙ ∈ V
138 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 ˙
139 135 136 137 138 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 ˙
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 ⊢ φ ∧ 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 150 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
152 neanior ⊢ l ⁡ v ≠ 0 ˙ ∧ v ≠ z ↔ ¬ l ⁡ v = 0 ˙ ∨ v = z
153 151 152 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
154 153 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
155 anass ⊢ v ∈ I ∧ l ⁡ v ≠ 0 ˙ ∧ v ≠ z ↔ v ∈ I ∧ l ⁡ v ≠ 0 ˙ ∧ v ≠ z
156 154 155 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
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 ∈ I → x ∈ I ⟼ if x = z 0 ˙ l ⁡ x ⁡ v = if v = z 0 ˙ l ⁡ v
161 160 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
162 161 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 ˙
163 162 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 ˙
164 116 adantr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ → l Fn I
165 elsuppfn ⊢ l Fn I ∧ I ∈ V ∧ 0 ˙ ∈ V → v ∈ supp 0 ˙⁡ l ↔ v ∈ I ∧ l ⁡ v ≠ 0 ˙
166 164 136 137 165 syl3anc ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ → v ∈ supp 0 ˙⁡ l ↔ v ∈ I ∧ l ⁡ v ≠ 0 ˙
167 166 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
168 156 163 167 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
169 139 168 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
170 130 169 syl5bb ⊢ φ ∧ 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
171 170 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 ˙
172 171 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 ˙
173 172 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 ˙
174 129 173 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 ˙
175 131 33 ifex ⊢ if x = z l ⁡ x 0 ˙ ∈ V
176 eqid ⊢ x ∈ I ⟼ if x = z l ⁡ x 0 ˙ = x ∈ I ⟼ if x = z l ⁡ x 0 ˙
177 175 176 fnmpti ⊢ x ∈ I ⟼ if x = z l ⁡ x 0 ˙ Fn I
178 177 a1i ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ → x ∈ I ⟼ if x = z l ⁡ x 0 ˙ Fn I
179 inidm ⊢ I ∩ I = I
180 135 178 136 136 179 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
181 157 158 ifbieq1d ⊢ x = v → if x = z l ⁡ x 0 ˙ = if v = z l ⁡ v 0 ˙
182 181 176 175 fvmpt3i ⊢ v ∈ I → x ∈ I ⟼ if x = z l ⁡ x 0 ˙ ⁡ v = if v = z l ⁡ v 0 ˙
183 182 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 ˙
184 135 178 136 136 179 161 183 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 ˙
185 4 ad4antr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ ∧ v ∈ I → G ∈ Grp
186 simplrl ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ ∧ v ∈ I → l ∈ B I
187 186 anassrs ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ ∧ v ∈ I → l ∈ B I
188 simpr ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ ∧ v ∈ I → v ∈ I
189 94 187 188 mapfvd ⊢ φ ∧ j ∈ ℕ ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ ∧ l ⁡ z ≠ 0 ˙ ∧ v ∈ I → l ⁡ v ∈ B
190 1 3 2 grplid ⊢ G ∈ Grp ∧ l ⁡ v ∈ B → 0 ˙ + ˙ l ⁡ v = l ⁡ v
191 1 3 2 grprid ⊢ G ∈ Grp ∧ l ⁡ v ∈ B → l ⁡ v + ˙ 0 ˙ = l ⁡ v
192 190 191 ifeq12d ⊢ G ∈ Grp ∧ l ⁡ v ∈ B → if v = z 0 ˙ + ˙ l ⁡ v l ⁡ v + ˙ 0 ˙ = if v = z l ⁡ v l ⁡ v
193 185 189 192 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
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 ⊢ φ ∧ 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
198 184 197 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
199 164 180 198 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 ˙
200 199 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 ˙
201 174 200 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 ˙
202 201 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 ˙
203 105 111 202 rspcedvd ⊢ φ ∧ 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 ˙
204 115 ad2antrl ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → l Fn I
205 5 ad3antrrr ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → I ∈ V
206 33 a1i ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → 0 ˙ ∈ V
207 suppvalfn ⊢ l Fn I ∧ I ∈ V ∧ 0 ˙ ∈ V → l supp 0 ˙ = z ∈ I | l ⁡ z ≠ 0 ˙
208 204 205 206 207 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 ˙
209 simprr ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → j + 1 = l supp 0 ˙
210 peano2nn ⊢ j ∈ ℕ → j + 1 ∈ ℕ
211 210 ad3antlr ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → j + 1 ∈ ℕ
212 211 nnne0d ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → j + 1 ≠ 0
213 209 212 eqnetrrd ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → l supp 0 ˙ ≠ 0
214 ovex ⊢ l supp 0 ˙ ∈ V
215 hasheq0 ⊢ l supp 0 ˙ ∈ V → l supp 0 ˙ = 0 ↔ l supp 0 ˙ = ∅
216 215 necon3bid ⊢ l supp 0 ˙ ∈ V → l supp 0 ˙ ≠ 0 ↔ l supp 0 ˙ ≠ ∅
217 214 216 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 ˙ ≠ ∅
218 213 217 mpbid ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → l supp 0 ˙ ≠ ∅
219 208 218 eqnetrrd ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → z ∈ I | l ⁡ z ≠ 0 ˙ ≠ ∅
220 rabn0 ⊢ z ∈ I | l ⁡ z ≠ 0 ˙ ≠ ∅ ↔ ∃ z ∈ I l ⁡ z ≠ 0 ˙
221 219 220 sylib ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → ∃ z ∈ I l ⁡ z ≠ 0 ˙
222 203 221 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 ˙
223 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 ˙
224 222 223 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 ˙
225 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 ˙
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 ∈ H ↔ m ∈ H
229 227 228 imbi12d ⊢ h = m → j = h supp 0 ˙ → h ∈ H ↔ j = m supp 0 ˙ → m ∈ H
230 229 rspccva ⊢ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ m ∈ B I → j = m supp 0 ˙ → m ∈ H
231 230 adantll ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ m ∈ B I → j = m supp 0 ˙ → m ∈ H
232 231 imp ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ m ∈ B I ∧ j = m supp 0 ˙ → m ∈ H
233 232 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
234 233 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
235 234 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
236 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
237 95 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
238 94 237 236 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
239 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
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 ∈ I ⟼ if x = a b 0 ˙ = x ∈ I ⟼ if x = z b 0 ˙
243 242 eleq1d ⊢ a = z → x ∈ I ⟼ if x = a b 0 ˙ ∈ H ↔ x ∈ I ⟼ if x = z b 0 ˙ ∈ 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 ∈ I ⟼ if x = z b 0 ˙ = x ∈ I ⟼ if x = z l ⁡ x 0 ˙
249 248 eleq1d ⊢ b = l ⁡ z → x ∈ I ⟼ if x = z b 0 ˙ ∈ H ↔ x ∈ I ⟼ if x = z l ⁡ x 0 ˙ ∈ H
250 243 249 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
251 236 238 239 250 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
252 8 ralrimivva ⊢ φ → ∀ x ∈ H ∀ y ∈ H x + ˙ f y ∈ H
253 252 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
254 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
255 235 251 253 254 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
256 225 255 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
257 256 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
258 257 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
259 224 258 mpd ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H ∧ l ∈ B I ∧ j + 1 = l supp 0 ˙ → l ∈ H
260 259 exp32 ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H → l ∈ B I → j + 1 = l supp 0 ˙ → l ∈ H
261 260 ralrimiv ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H → ∀ l ∈ B I j + 1 = l supp 0 ˙ → l ∈ 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 ∈ H ↔ h ∈ H
265 263 264 imbi12d ⊢ l = h → j + 1 = l supp 0 ˙ → l ∈ H ↔ j + 1 = h supp 0 ˙ → h ∈ H
266 265 cbvralvw ⊢ ∀ l ∈ B I j + 1 = l supp 0 ˙ → l ∈ H ↔ ∀ h ∈ B I j + 1 = h supp 0 ˙ → h ∈ H
267 261 266 sylib ⊢ φ ∧ j ∈ ℕ ∧ ∀ h ∈ B I j = h supp 0 ˙ → h ∈ H → ∀ h ∈ B I j + 1 = h supp 0 ˙ → h ∈ H
268 15 18 21 24 90 267 nnindd ⊢ φ ∧ n ∈ ℕ → ∀ h ∈ B I n = h supp 0 ˙ → h ∈ H
269 268 ralrimiva ⊢ φ → ∀ n ∈ ℕ ∀ h ∈ B I n = h supp 0 ˙ → h ∈ H
270 ralcom ⊢ ∀ n ∈ ℕ ∀ h ∈ B I n = h supp 0 ˙ → h ∈ H ↔ ∀ h ∈ B I ∀ n ∈ ℕ n = h supp 0 ˙ → h ∈ H
271 269 270 sylib ⊢ φ → ∀ h ∈ B I ∀ n ∈ ℕ n = h supp 0 ˙ → h ∈ H
272 biidd ⊢ n = h supp 0 ˙ → h ∈ H ↔ h ∈ H
273 272 ceqsralv ⊢ h supp 0 ˙ ∈ ℕ → ∀ n ∈ ℕ n = h supp 0 ˙ → h ∈ H ↔ h ∈ H
274 273 biimpcd ⊢ ∀ n ∈ ℕ n = h supp 0 ˙ → h ∈ H → h supp 0 ˙ ∈ ℕ → h ∈ H
275 274 ralimi ⊢ ∀ h ∈ B I ∀ n ∈ ℕ n = h supp 0 ˙ → h ∈ H → ∀ h ∈ B I h supp 0 ˙ ∈ ℕ → h ∈ H
276 271 275 syl ⊢ φ → ∀ h ∈ B I h supp 0 ˙ ∈ ℕ → h ∈ H
277 fvoveq1 ⊢ h = X → h supp 0 ˙ = X supp 0 ˙
278 277 eleq1d ⊢ h = X → h supp 0 ˙ ∈ ℕ ↔ X supp 0 ˙ ∈ ℕ
279 eleq1 ⊢ h = X → h ∈ H ↔ X ∈ H
280 278 279 imbi12d ⊢ h = X → h supp 0 ˙ ∈ ℕ → h ∈ H ↔ X supp 0 ˙ ∈ ℕ → X ∈ H
281 280 rspcv ⊢ X ∈ B I → ∀ h ∈ B I h supp 0 ˙ ∈ ℕ → h ∈ H → X supp 0 ˙ ∈ ℕ → X ∈ H
282 276 281 syl5com ⊢ φ → X ∈ B I → X supp 0 ˙ ∈ ℕ → X ∈ H
283 282 com23 ⊢ φ → X supp 0 ˙ ∈ ℕ → X ∈ B I → X ∈ H
284 283 imp ⊢ φ ∧ X supp 0 ˙ ∈ ℕ → X ∈ B I → X ∈ H
285 12 284 sylbird ⊢ φ ∧ X supp 0 ˙ ∈ ℕ → X : I ⟶ B → X ∈ H
286 285 imp ⊢ φ ∧ X supp 0 ˙ ∈ ℕ ∧ X : I ⟶ B → X ∈ H
287 286 an32s ⊢ φ ∧ X : I ⟶ B ∧ X supp 0 ˙ ∈ ℕ → X ∈ H
288 287 adantlr ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X ∧ X supp 0 ˙ ∈ ℕ → X ∈ H
289 ovex ⊢ X supp 0 ˙ ∈ V
290 hasheq0 ⊢ X supp 0 ˙ ∈ 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 ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X Fn I
294 5 ad2antrr ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → I ∈ V
295 33 a1i ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → 0 ˙ ∈ V
296 fnsuppeq0 ⊢ X Fn I ∧ I ∈ V ∧ 0 ˙ ∈ V → X supp 0 ˙ = ∅ ↔ X = I × 0 ˙
297 293 294 295 296 syl3anc ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X supp 0 ˙ = ∅ ↔ X = I × 0 ˙
298 297 biimpa ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X ∧ X supp 0 ˙ = ∅ → X = I × 0 ˙
299 6 ad3antrrr ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X ∧ X supp 0 ˙ = ∅ → I × 0 ˙ ∈ H
300 298 299 eqeltrd ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X ∧ X supp 0 ˙ = ∅ → X ∈ H
301 291 300 sylan2b ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X ∧ X supp 0 ˙ = 0 → X ∈ H
302 simpr ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → finSupp 0 ˙⁡ X
303 302 fsuppimpd ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X supp 0 ˙ ∈ Fin
304 hashcl ⊢ X supp 0 ˙ ∈ Fin → X supp 0 ˙ ∈ ℕ 0
305 303 304 syl ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X supp 0 ˙ ∈ ℕ 0
306 elnn0 ⊢ X supp 0 ˙ ∈ ℕ 0 ↔ X supp 0 ˙ ∈ ℕ ∨ X supp 0 ˙ = 0
307 305 306 sylib ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X supp 0 ˙ ∈ ℕ ∨ X supp 0 ˙ = 0
308 288 301 307 mpjaodan ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X ∈ H
309 308 anasss ⊢ φ ∧ X : I ⟶ B ∧ finSupp 0 ˙⁡ X → X ∈ H