fsuppind - Mathbox for Steven Nguyen

	Mathbox for Steven Nguyen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fsuppind		Structured version Visualization version GIF version

Theorem fsuppind 40286

Description: Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 20972 and frlmplusgval 20980). This theorem is structurally general for polynomial proof usage (see mplelbas 21208 and mpladd 21222). Note that hypothesis 0 is redundant when 𝐼 is nonempty. (Contributed by SN, 18-May-2024.)

**Hypotheses**
Ref	Expression
fsuppind.b	⊢ 𝐵 = (Base‘𝐺)
fsuppind.z	⊢ 0 = (0_g‘𝐺)
fsuppind.p	⊢ + = (+_g‘𝐺)
fsuppind.g	⊢ (𝜑 → 𝐺 ∈ Grp)
fsuppind.v	⊢ (𝜑 → 𝐼 ∈ 𝑉)
fsuppind.0	⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
fsuppind.1	⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
fsuppind.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘_f + 𝑦) ∈ 𝐻)

**Assertion**
Ref	Expression
fsuppind	⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻)

Distinct variable groups: 𝑥, + ,𝑦 0 ,𝑎,𝑏,𝑥 𝑦, 0 𝐼,𝑎,𝑏,𝑥 𝑦,𝐼 𝐻,𝑏 𝑦,𝐻,𝑥 𝐻,𝑎 𝜑,𝑥,𝑦 𝜑,𝑎,𝑏 𝐵,𝑎,𝑏,𝑥 Allowed substitution hints: 𝐵(𝑦) + (𝑎,𝑏) 𝐺(𝑥,𝑦,𝑎,𝑏) 𝑉(𝑥,𝑦,𝑎,𝑏) 𝑋(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem fsuppind Dummy variables 𝑧 𝑐 ℎ 𝑚 𝑣 𝑖 𝑗 𝑛 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fsuppind.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐺)
2	1	fvexi 6797	. . . . . . . . . 10 ⊢ 𝐵 ∈ V
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ V)
4		fsuppind.v	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
5	3, 4	elmapd 8638	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑_m 𝐼) ↔ 𝑋:𝐼⟶𝐵))
6	5	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵 ↑_m 𝐼) ↔ 𝑋:𝐼⟶𝐵))
7		eqeq1 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 1 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 1 = (♯‘(ℎ supp 0 ))))
8	7	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
9	8	ralbidv 3113	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
10		eqeq1 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(ℎ supp 0 ))))
11	10	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
12	11	ralbidv 3113	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
13		eqeq1 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘(ℎ supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 ))))
14	13	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
15	14	ralbidv 3113	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 + 1) → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
16		eqeq1 2743	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑛 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑛 = (♯‘(ℎ supp 0 ))))
17	16	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑛 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
18	17	ralbidv 3113	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑛 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
19		eqcom 2746	. . . . . . . . . . . . . . . . 17 ⊢ (1 = (♯‘(ℎ supp 0 )) ↔ (♯‘(ℎ supp 0 )) = 1)
20		ovex 7317	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ supp 0 ) ∈ V
21		euhash1 14144	. . . . . . . . . . . . . . . . . 18 ⊢ ((ℎ supp 0 ) ∈ V → ((♯‘(ℎ supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 )))
22	20, 21	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘(ℎ supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 ))
23	19, 22	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (1 = (♯‘(ℎ supp 0 )) ↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 ))
24		elmapfn 8662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∈ (𝐵 ↑_m 𝐼) → ℎ Fn 𝐼)
25	24	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → ℎ Fn 𝐼)
26	4	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → 𝐼 ∈ 𝑉)
27		fsuppind.z	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 = (0_g‘𝐺)
28	27	fvexi 6797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → 0 ∈ V)
30		elsuppfn 7996	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
31	25, 26, 29, 30	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
32	31	eubidv 2587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
33		df-reu 3073	. . . . . . . . . . . . . . . . . 18 ⊢ (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))
34	32, 33	bitr4di 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))
35	24	ad2antlr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ Fn 𝐼)
36		fvex 6796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ‘𝑥) ∈ V
37	36, 28	ifex 4510	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) ∈ V
38		eqid 2739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))
39	37, 38	fnmpti 6585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼
40	39	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼)
41		eqeq1 2743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑣 → (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
42		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑣 → (ℎ‘𝑥) = (ℎ‘𝑣))
43	41, 42	ifbieq1d 4484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑣 → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
44	43, 38, 37	fvmpt3i 6889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
45	44	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
46		eqidd 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (ℎ‘𝑣) = (ℎ‘𝑣))
47		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
48		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )
49		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑣 → (ℎ‘𝑐) = (ℎ‘𝑣))
50	49	neeq1d 3004	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = 𝑣 → ((ℎ‘𝑐) ≠ 0 ↔ (ℎ‘𝑣) ≠ 0 ))
51	50	riota2 7267	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑣 ∈ 𝐼 ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((ℎ‘𝑣) ≠ 0 ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣))
52	47, 48, 51	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((ℎ‘𝑣) ≠ 0 ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣))
53		necom 2998	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( 0 ≠ (ℎ‘𝑣) ↔ (ℎ‘𝑣) ≠ 0 )
54		eqcom 2746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣)
55	52, 53, 54	3bitr4g 314	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
56	55	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) → 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
57	56	necon1bd 2962	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → 0 = (ℎ‘𝑣)))
58	57	imp 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ ¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 0 = (ℎ‘𝑣))
59	46, 58	ifeqda 4496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ) = (ℎ‘𝑣))
60	45, 59	eqtr2d 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (ℎ‘𝑣) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣))
61	35, 40, 60	eqfnfvd 6921	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )))
62		riotacl 7259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼)
63	62	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼)
64		elmapi 8646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ∈ (𝐵 ↑_m 𝐼) → ℎ:𝐼⟶𝐵)
65	64	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ:𝐼⟶𝐵)
66	65, 63	ffvelrnd 6971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵)
67		fsuppind.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
68	67	ralrimivva 3124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
69	68	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70		eqeq2 2751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 = 𝑎 ↔ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
71	70	ifbid 4483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ))
72	71	mpteq2dv 5177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )))
73	72	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘𝑥) = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
75	74	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑏 = (ℎ‘𝑥) ↔ 𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))))
76	75	biimparc 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∧ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 𝑏 = (ℎ‘𝑥))
77	76	ifeq1da 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))
78	77	mpteq2dv 5177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )))
79	78	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻))
80	73, 79	rspc2va 3572	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼 ∧ (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)
81	63, 66, 69, 80	syl21anc 835	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)
82	61, 81	eqeltrd 2840	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ ∈ 𝐻)
83	82	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → ℎ ∈ 𝐻))
84	34, 83	sylbid 239	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) → ℎ ∈ 𝐻))
85	23, 84	syl5bi 241	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
86	85	ralrimiva 3104	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
87		fsuppind.g	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐺 ∈ Grp)
88	1, 27	grpidcl 18616	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ 𝐵)
90	89	ad5antr 731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 0 ∈ 𝐵)
91		eqid 2739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ↑_m 𝐼) = (𝐵 ↑_m 𝐼)
92		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
93	92	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
94		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
95	91, 93, 94	mapfvd 8676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑙‘𝑥) ∈ 𝐵)
96	90, 95	ifcld 4506	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ 𝐵)
97	96	fmpttd 6998	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵)
98	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐵 ∈ V)
99	4	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉)
100	98, 99	elmapd 8638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼) ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵))
101	97, 100	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼))
102	101	adantrl 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼))
103		fvoveq1 7307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
104	103	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))))
105		oveq1 7291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
106	105	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ↔ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
107	104, 106	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))))
108	107	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) ∧ 𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))))
109		ovexd 7319	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
110		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ 𝐼)
111		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙‘𝑧) ≠ 0 )
112		elmapfn 8662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑙 ∈ (𝐵 ↑_m 𝐼) → 𝑙 Fn 𝐼)
113	112	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
114	113	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
115	4	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝐼 ∈ 𝑉)
116	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 0 ∈ V)
117		elsuppfn 7996	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )))
118	114, 115, 116, 117	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )))
119	110, 111, 118	mpbir2and 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
120		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
121	120	nnnn0d 12302	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈ ℕ₀)
122		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
123	122	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
124		hashdifsnp1 14219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ₀) → ((♯‘(𝑙 supp 0 )) = (𝑗 + 1) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗))
125	124	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ₀) ∧ (♯‘(𝑙 supp 0 )) = (𝑗 + 1)) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126	109, 119, 121, 123, 125	syl31anc 1372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
127		eldifsn 4721	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧))
128		fvex 6796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑙‘𝑥) ∈ V
129	28, 128	ifex 4510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ V
130		eqid 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))
131	129, 130	fnmpti 6585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼
132	131	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼)
133	4	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉)
134	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 0 ∈ V)
135		elsuppfn 7996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 )))
136	132, 133, 134, 135	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 )))
137		iftrue 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 )
138		olc 865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
139	137, 138	2thd 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
140		iffalse 4469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (¬ 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = (𝑙‘𝑣))
141	140	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (¬ 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ (𝑙‘𝑣) = 0 ))
142		biorf 934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (¬ 𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 )))
143		orcom 867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 ))
144	142, 143	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (¬ 𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
145	141, 144	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (¬ 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
146	139, 145	pm2.61i 182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
148	147	necon3abid 2981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
149		neanior 3038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧) ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
150	148, 149	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))
151	150	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧))))
152		anass 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))
153	151, 152	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧)))
154		equequ1 2029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑣 → (𝑥 = 𝑧 ↔ 𝑣 = 𝑧))
155		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑣 → (𝑙‘𝑥) = (𝑙‘𝑣))
156	154, 155	ifbieq2d 4486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
157	156, 130, 129	fvmpt3i 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
158	157	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
159	158	neeq1d 3004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ))
160	159	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 )))
161	113	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 Fn 𝐼)
162		elsuppfn 7996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 )))
163	161, 133, 134, 162	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 )))
164	163	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧)))
165	153, 160, 164	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧)))
166	136, 165	bitr2d 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
167	127, 166	syl5bb 283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
168	167	eqrdv 2737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))
169	168	fveq2d 6787	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
170	169	adantrl 713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
171	126, 170	eqtr3d 2781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
172	128, 28	ifex 4510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) ∈ V
173		eqid 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))
174	172, 173	fnmpti 6585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼
175	174	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼)
176		inidm 4153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐼 ∩ 𝐼) = 𝐼
177	132, 175, 133, 133, 176	offn 7555	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) Fn 𝐼)
178	154, 155	ifbieq1d 4484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
179	178, 173, 172	fvmpt3i 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
180	179	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
181	132, 175, 133, 133, 176, 158, 180	ofval 7553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )))
182	87	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝐺 ∈ Grp)
183		simplrl 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙‘𝑧) ≠ 0 ∧ 𝑣 ∈ 𝐼)) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
184	183	anassrs 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
185		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
186	91, 184, 185	mapfvd 8676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) ∈ 𝐵)
187		fsuppind.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ + = (+_g‘𝐺)
188	1, 187, 27	grplid 18618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ( 0 + (𝑙‘𝑣)) = (𝑙‘𝑣))
189	1, 187, 27	grprid 18619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ((𝑙‘𝑣) + 0 ) = (𝑙‘𝑣))
190	188, 189	ifeq12d 4481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)))
191	182, 186, 190	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)))
192		ovif12 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 ))
193		ifid 4500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) = (𝑙‘𝑣)
194	193	eqcomi 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑙‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣))
195	191, 192, 194	3eqtr4g 2804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = (𝑙‘𝑣))
196	181, 195	eqtr2d 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) = (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣))
197	161, 177, 196	eqfnfvd 6921	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
198	197	adantrl 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
199	171, 198	jca 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
200	199	adantllr 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
201	102, 108, 200	rspcedvd 3564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
202	112	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
203	4	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼 ∈ 𝑉)
204	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
205		suppvalfn 7994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 })
206	202, 203, 204, 205	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 })
207		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
208		peano2nn 11994	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
209	208	ad3antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
210	209	nnne0d 12032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
211	207, 210	eqnetrrd 3013	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
212		ovex 7317	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 supp 0 ) ∈ V
213		hasheq0 14087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
214	213	necon3bid 2989	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
215	212, 214	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
216	211, 215	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) ≠ ∅)
217	206, 216	eqnetrrd 3013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅)
218		rabn0 4320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅ ↔ ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 )
219	217, 218	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 )
220	201, 219	reximddv 3205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
221		rexcom 3235	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ 𝐼 ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ ∃𝑚 ∈ (𝐵 ↑_m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
222	220, 221	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑚 ∈ (𝐵 ↑_m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
223		simprr 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
224		fvoveq1 7307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ = 𝑚 → (♯‘(ℎ supp 0 )) = (♯‘(𝑚 supp 0 )))
225	224	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = 𝑚 → (𝑗 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
226		eleq1w 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = 𝑚 → (ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻))
227	225, 226	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = 𝑚 → ((𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)))
228	227	rspccva 3561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))
229	228	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))
230	229	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
231	230	adantllr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
232	231	adantlrr 718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
233	232	adantrr 714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑚 ∈ 𝐻)
234		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑧 ∈ 𝐼)
235	92	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
236	91, 235, 234	mapfvd 8676	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑙‘𝑧) ∈ 𝐵)
237	68	ad5antr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
238		equequ2 2030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑧 → (𝑥 = 𝑎 ↔ 𝑥 = 𝑧))
239	238	ifbid 4483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
240	239	mpteq2dv 5177	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑧 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
241	240	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑧 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
242		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑧 → (𝑙‘𝑥) = (𝑙‘𝑧))
243	242	eqeq2d 2750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑏 = (𝑙‘𝑥) ↔ 𝑏 = (𝑙‘𝑧)))
244	243	biimparc 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 = (𝑙‘𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙‘𝑥))
245	244	ifeq1da 4491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = (𝑙‘𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))
246	245	mpteq2dv 5177	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = (𝑙‘𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))
247	246	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = (𝑙‘𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻))
248	241, 247	rspc2va 3572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)
249	234, 236, 237, 248	syl21anc 835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)
250		fsuppind.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘_f + 𝑦) ∈ 𝐻)
251	250	ralrimivva 3124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻)
252	251	ad5antr 731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻)
253		ovrspc2v 7310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 ∈ 𝐻 ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻)
254	233, 249, 252, 253	syl21anc 835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻)
255	223, 254	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ 𝐻)
256	255	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻))
257	256	rexlimdvva 3224	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (∃𝑚 ∈ (𝐵 ↑_m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻))
258	222, 257	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ 𝐻)
259	258	exp32 421	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → (𝑙 ∈ (𝐵 ↑_m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻)))
260	259	ralrimiv 3103	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀𝑙 ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻))
261		fvoveq1 7307	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (♯‘(𝑙 supp 0 )) = (♯‘(ℎ supp 0 )))
262	261	eqeq2d 2750	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 ))))
263		eleq1w 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → (𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻))
264	262, 263	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = ℎ → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
265	264	cbvralvw 3384	. . . . . . . . . . . . . . 15 ⊢ (∀𝑙 ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
266	260, 265	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
267	9, 12, 15, 18, 86, 266	nnindd 12002	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
268	267	ralrimiva 3104	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
269		ralcom 3167	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
270	268, 269	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
271		biidd 261	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (♯‘(ℎ supp 0 )) → (ℎ ∈ 𝐻 ↔ ℎ ∈ 𝐻))
272	271	ceqsralv 3470	. . . . . . . . . . . . 13 ⊢ ((♯‘(ℎ supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ℎ ∈ 𝐻))
273	272	biimpcd 248	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
274	273	ralimi 3088	. . . . . . . . . . 11 ⊢ (∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
275	270, 274	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
276		fvoveq1 7307	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑋 → (♯‘(ℎ supp 0 )) = (♯‘(𝑋 supp 0 )))
277	276	eleq1d 2824	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑋 → ((♯‘(ℎ supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
278		eleq1 2827	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑋 → (ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻))
279	277, 278	imbi12d 345	. . . . . . . . . . 11 ⊢ (ℎ = 𝑋 → (((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
280	279	rspcv 3558	. . . . . . . . . 10 ⊢ (𝑋 ∈ (𝐵 ↑_m 𝐼) → (∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
281	275, 280	syl5com 31	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑_m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
282	281	com23 86	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ → (𝑋 ∈ (𝐵 ↑_m 𝐼) → 𝑋 ∈ 𝐻)))
283	282	imp 407	. . . . . . 7 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵 ↑_m 𝐼) → 𝑋 ∈ 𝐻))
284	6, 283	sylbird 259	. . . . . 6 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋:𝐼⟶𝐵 → 𝑋 ∈ 𝐻))
285	284	imp 407	. . . . 5 ⊢ (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧ 𝑋:𝐼⟶𝐵) → 𝑋 ∈ 𝐻)
286	285	an32s 649	. . . 4 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋 ∈ 𝐻)
287	286	adantlr 712	. . 3 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋 ∈ 𝐻)
288		ovex 7317	. . . . 5 ⊢ (𝑋 supp 0 ) ∈ V
289		hasheq0 14087	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
290	288, 289	ax-mp 5	. . . 4 ⊢ ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
291		ffn 6609	. . . . . . . 8 ⊢ (𝑋:𝐼⟶𝐵 → 𝑋 Fn 𝐼)
292	291	ad2antlr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
293	4	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉)
294	28	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
295		fnsuppeq0 8017	. . . . . . 7 ⊢ ((𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296	292, 293, 294, 295	syl3anc 1370	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
297	296	biimpa 477	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
298		fsuppind.0	. . . . . 6 ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
299	298	ad3antrrr 727	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
300	297, 299	eqeltrd 2840	. . . 4 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 ∈ 𝐻)
301	290, 300	sylan2b 594	. . 3 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋 ∈ 𝐻)
302		simpr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
303	302	fsuppimpd 9144	. . . . 5 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
304		hashcl 14080	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ₀)
305	303, 304	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ₀)
306		elnn0 12244	. . . 4 ⊢ ((♯‘(𝑋 supp 0 )) ∈ ℕ₀ ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
307	305, 306	sylib 217	. . 3 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
308	287, 301, 307	mpjaodan 956	. 2 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 ∈ 𝐻)
309	308	anasss 467	1 ⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ∃!weu 2569 ≠ wne 2944 ∀wral 3065 ∃wrex 3066 ∃!wreu 3067 {crab 3069 Vcvv 3433 ∖ cdif 3885 ∅c0 4257 ifcif 4460 {csn 4562 class class class wbr 5075 ↦ cmpt 5158 × cxp 5588 Fn wfn 6432 ⟶wf 6433 ‘cfv 6437 ℩crio 7240 (class class class)co 7284 ∘_f cof 7540 supp csupp 7986 ↑_m cmap 8624 Fincfn 8742 finSupp cfsupp 9137 0cc0 10880 1c1 10881 + caddc 10883 ℕcn 11982 ℕ₀cn0 12242 ♯chash 14053 Basecbs 16921 +_gcplusg 16971 0_gc0g 17159 Grpcgrp 18586

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-of 7542 df-om 7722 df-1st 7840 df-2nd 7841 df-supp 7987 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-oadd 8310 df-er 8507 df-map 8626 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-fsupp 9138 df-dju 9668 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-n0 12243 df-z 12329 df-uz 12592 df-fz 13249 df-hash 14054 df-0g 17161 df-mgm 18335 df-sgrp 18384 df-mnd 18395 df-grp 18589

This theorem is referenced by: fsuppssind 40289

W3C validator