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 42711

Description: Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21697 and frlmplusgval 21705). This theorem is structurally general for polynomial proof usage (see mplelbas 21931 and mpladd 21949). 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 6844	. . . . . . . . . 10 ⊢ 𝐵 ∈ V
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ V)
4		fsuppind.v	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
5	3, 4	elmapd 8772	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑_m 𝐼) ↔ 𝑋:𝐼⟶𝐵))
6	5	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵 ↑_m 𝐼) ↔ 𝑋:𝐼⟶𝐵))
7		eqeq1 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 1 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 1 = (♯‘(ℎ supp 0 ))))
8	7	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
9	8	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
10		eqeq1 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(ℎ supp 0 ))))
11	10	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
12	11	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
13		eqeq1 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘(ℎ supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 ))))
14	13	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
15	14	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 + 1) → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
16		eqeq1 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑛 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑛 = (♯‘(ℎ supp 0 ))))
17	16	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑛 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
18	17	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑛 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
19		eqcom 2740	. . . . . . . . . . . . . . . . 17 ⊢ (1 = (♯‘(ℎ supp 0 )) ↔ (♯‘(ℎ supp 0 )) = 1)
20		ovex 7387	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ supp 0 ) ∈ V
21		euhash1 14331	. . . . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . . . 16 ⊢ (1 = (♯‘(ℎ supp 0 )) ↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 ))
24		elmapfn 8797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ∈ (𝐵 ↑_m 𝐼) → ℎ Fn 𝐼)
25	24	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → ℎ Fn 𝐼)
26	4	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → 𝐼 ∈ 𝑉)
27		fsuppind.z	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 = (0_g‘𝐺)
28	27	fvexi 6844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → 0 ∈ V)
30		elsuppfn 8108	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
31	25, 26, 29, 30	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
32	31	eubidv 2583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
33		df-reu 3348	. . . . . . . . . . . . . . . . . 18 ⊢ (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))
34	32, 33	bitr4di 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))
35	24	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ Fn 𝐼)
36		fvex 6843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ‘𝑥) ∈ V
37	36, 28	ifex 4527	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) ∈ V
38		eqid 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))
39	37, 38	fnmpti 6631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼
40	39	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼)
41		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑣 → (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
42		fveq2 6830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑣 → (ℎ‘𝑥) = (ℎ‘𝑣))
43	41, 42	ifbieq1d 4501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑣 → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
44	43, 38, 37	fvmpt3i 6942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
45	44	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
46		eqidd 2734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (ℎ‘𝑣) = (ℎ‘𝑣))
47		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
48		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )
49		fveq2 6830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑣 → (ℎ‘𝑐) = (ℎ‘𝑣))
50	49	neeq1d 2988	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = 𝑣 → ((ℎ‘𝑐) ≠ 0 ↔ (ℎ‘𝑣) ≠ 0 ))
51	50	riota2 7336	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑣 ∈ 𝐼 ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((ℎ‘𝑣) ≠ 0 ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣))
52	47, 48, 51	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((ℎ‘𝑣) ≠ 0 ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣))
53		necom 2982	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( 0 ≠ (ℎ‘𝑣) ↔ (ℎ‘𝑣) ≠ 0 )
54		eqcom 2740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣)
55	52, 53, 54	3bitr4g 314	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
56	55	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) → 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
57	56	necon1bd 2947	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → 0 = (ℎ‘𝑣)))
58	57	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ ¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 0 = (ℎ‘𝑣))
59	46, 58	ifeqda 4513	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ) = (ℎ‘𝑣))
60	45, 59	eqtr2d 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (ℎ‘𝑣) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣))
61	35, 40, 60	eqfnfvd 6975	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )))
62		riotacl 7328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼)
63	62	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼)
64		elmapi 8781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ∈ (𝐵 ↑_m 𝐼) → ℎ:𝐼⟶𝐵)
65	64	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ:𝐼⟶𝐵)
66	65, 63	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵)
67		fsuppind.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
68	67	ralrimivva 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
69	68	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70		eqeq2 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 = 𝑎 ↔ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
71	70	ifbid 4500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ))
72	71	mpteq2dv 5189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )))
73	72	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74		fveq2 6830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘𝑥) = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
75	74	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑏 = (ℎ‘𝑥) ↔ 𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))))
76	75	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∧ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 𝑏 = (ℎ‘𝑥))
77	76	ifeq1da 4508	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))
78	77	mpteq2dv 5189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )))
79	78	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻))
80	73, 79	rspc2va 3585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼 ∧ (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)
81	63, 66, 69, 80	syl21anc 837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)
82	61, 81	eqeltrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ ∈ 𝐻)
83	82	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → ℎ ∈ 𝐻))
84	34, 83	sylbid 240	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) → ℎ ∈ 𝐻))
85	23, 84	biimtrid 242	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
86	85	ralrimiva 3125	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
87		fvoveq1 7377	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
88	87	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))))
89		oveq1 7361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
90	89	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ↔ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
91	88, 90	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))))
92		fsuppind.g	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐺 ∈ Grp)
93	1, 27	grpidcl 18882	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ 𝐵)
95	94	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 0 ∈ 𝐵)
96		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ↑_m 𝐼) = (𝐵 ↑_m 𝐼)
97		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
98	97	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
99		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
100	96, 98, 99	mapfvd 8811	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑙‘𝑥) ∈ 𝐵)
101	95, 100	ifcld 4523	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ 𝐵)
102	101	fmpttd 7056	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵)
103	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐵 ∈ V)
104	4	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉)
105	103, 104	elmapd 8772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼) ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵))
106	102, 105	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼))
107	106	adantrl 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼))
108		ovexd 7389	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
109		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ 𝐼)
110		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙‘𝑧) ≠ 0 )
111		elmapfn 8797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑙 ∈ (𝐵 ↑_m 𝐼) → 𝑙 Fn 𝐼)
112	111	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
113	112	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
114	4	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝐼 ∈ 𝑉)
115	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 0 ∈ V)
116		elsuppfn 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )))
117	113, 114, 115, 116	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )))
118	109, 110, 117	mpbir2and 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
119		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
120	119	nnnn0d 12451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈ ℕ₀)
121		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
122	121	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
123		hashdifsnp1 14417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ₀) → ((♯‘(𝑙 supp 0 )) = (𝑗 + 1) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗))
124	123	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ₀) ∧ (♯‘(𝑙 supp 0 )) = (𝑗 + 1)) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
125	108, 118, 120, 122, 124	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126		eldifsn 4739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧))
127		fvex 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑙‘𝑥) ∈ V
128	28, 127	ifex 4527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ V
129		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))
130	128, 129	fnmpti 6631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼)
132	4	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉)
133	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 0 ∈ V)
134		elsuppfn 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 )))
135	131, 132, 133, 134	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 )))
136		iftrue 4482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 )
137		olc 868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
138	136, 137	2thd 265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
139		iffalse 4485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (¬ 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = (𝑙‘𝑣))
140	139	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (¬ 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ (𝑙‘𝑣) = 0 ))
141		biorf 936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (¬ 𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 )))
142		orcom 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 ))
143	141, 142	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (¬ 𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
144	140, 143	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (¬ 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
145	138, 144	pm2.61i 182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
146	145	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
147	146	necon3abid 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
148		neanior 3022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧) ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
149	147, 148	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))
150	149	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧))))
151		anass 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))
152	150, 151	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧)))
153		equequ1 2026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑣 → (𝑥 = 𝑧 ↔ 𝑣 = 𝑧))
154		fveq2 6830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑣 → (𝑙‘𝑥) = (𝑙‘𝑣))
155	153, 154	ifbieq2d 4503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
156	155, 129, 128	fvmpt3i 6942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
157	156	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
158	157	neeq1d 2988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ))
159	158	pm5.32da 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 )))
160	112	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 Fn 𝐼)
161		elsuppfn 8108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 )))
162	160, 132, 133, 161	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 )))
163	162	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧)))
164	152, 159, 163	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧)))
165	135, 164	bitr2d 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
166	126, 165	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
167	166	eqrdv 2731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))
168	167	fveq2d 6834	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
169	168	adantrl 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
170	125, 169	eqtr3d 2770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
171	127, 28	ifex 4527	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) ∈ V
172		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))
173	171, 172	fnmpti 6631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼)
175		inidm 4176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐼 ∩ 𝐼) = 𝐼
176	131, 174, 132, 132, 175	offn 7631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) Fn 𝐼)
177	153, 154	ifbieq1d 4501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
178	177, 172, 171	fvmpt3i 6942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
179	178	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
180	131, 174, 132, 132, 175, 157, 179	ofval 7629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )))
181	92	ad4antr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝐺 ∈ Grp)
182		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙‘𝑧) ≠ 0 ∧ 𝑣 ∈ 𝐼)) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
183	182	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
184		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
185	96, 183, 184	mapfvd 8811	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) ∈ 𝐵)
186		fsuppind.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ + = (+_g‘𝐺)
187	1, 186, 27	grplid 18884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ( 0 + (𝑙‘𝑣)) = (𝑙‘𝑣))
188	1, 186, 27	grprid 18885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ((𝑙‘𝑣) + 0 ) = (𝑙‘𝑣))
189	187, 188	ifeq12d 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)))
190	181, 185, 189	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)))
191		ovif12 7454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 ))
192		ifid 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) = (𝑙‘𝑣)
193	192	eqcomi 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑙‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣))
194	190, 191, 193	3eqtr4g 2793	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = (𝑙‘𝑣))
195	180, 194	eqtr2d 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) = (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣))
196	160, 176, 195	eqfnfvd 6975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
197	196	adantrl 716	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
198	170, 197	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
199	198	adantllr 719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
200	91, 107, 199	rspcedvdw 3576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
201	111	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
202	4	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼 ∈ 𝑉)
203	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
204		suppvalfn 8106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 })
205	201, 202, 203, 204	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 })
206		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
207		peano2nn 12146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
208	207	ad3antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
209	208	nnne0d 12184	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
210	206, 209	eqnetrrd 2997	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
211		ovex 7387	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 supp 0 ) ∈ V
212		hasheq0 14274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
213	212	necon3bid 2973	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
214	211, 213	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
215	210, 214	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) ≠ ∅)
216	205, 215	eqnetrrd 2997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅)
217		rabn0 4338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅ ↔ ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 )
218	216, 217	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 )
219	200, 218	reximddv 3149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
220		rexcom 3262	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧 ∈ 𝐼 ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ ∃𝑚 ∈ (𝐵 ↑_m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
221	219, 220	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑚 ∈ (𝐵 ↑_m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
222		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
223		fvoveq1 7377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ = 𝑚 → (♯‘(ℎ supp 0 )) = (♯‘(𝑚 supp 0 )))
224	223	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = 𝑚 → (𝑗 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
225		eleq1w 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = 𝑚 → (ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻))
226	224, 225	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = 𝑚 → ((𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)))
227	226	rspccva 3572	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))
228	227	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))
229	228	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
230	229	adantllr 719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
231	230	adantlrr 721	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
232	231	adantrr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑚 ∈ 𝐻)
233		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑧 ∈ 𝐼)
234	97	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
235	96, 234, 233	mapfvd 8811	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑙‘𝑧) ∈ 𝐵)
236	68	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
237		equequ2 2027	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑧 → (𝑥 = 𝑎 ↔ 𝑥 = 𝑧))
238	237	ifbid 4500	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
239	238	mpteq2dv 5189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑧 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
240	239	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑧 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
241		fveq2 6830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑧 → (𝑙‘𝑥) = (𝑙‘𝑧))
242	241	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑏 = (𝑙‘𝑥) ↔ 𝑏 = (𝑙‘𝑧)))
243	242	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 = (𝑙‘𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙‘𝑥))
244	243	ifeq1da 4508	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = (𝑙‘𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))
245	244	mpteq2dv 5189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = (𝑙‘𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))
246	245	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = (𝑙‘𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻))
247	240, 246	rspc2va 3585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)
248	233, 235, 236, 247	syl21anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)
249		fsuppind.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘_f + 𝑦) ∈ 𝐻)
250	249	ralrimivva 3176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻)
251	250	ad5antr 734	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻)
252		ovrspc2v 7380	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 ∈ 𝐻 ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻)
253	232, 248, 251, 252	syl21anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻)
254	222, 253	eqeltrd 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ 𝐻)
255	254	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻))
256	255	rexlimdvva 3190	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (∃𝑚 ∈ (𝐵 ↑_m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻))
257	221, 256	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ 𝐻)
258	257	exp32 420	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → (𝑙 ∈ (𝐵 ↑_m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻)))
259	258	ralrimiv 3124	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀𝑙 ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻))
260		fvoveq1 7377	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (♯‘(𝑙 supp 0 )) = (♯‘(ℎ supp 0 )))
261	260	eqeq2d 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 ))))
262		eleq1w 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → (𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻))
263	261, 262	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = ℎ → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
264	263	cbvralvw 3211	. . . . . . . . . . . . . . 15 ⊢ (∀𝑙 ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
265	259, 264	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
266	9, 12, 15, 18, 86, 265	nnindd 12154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
267	266	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
268		ralcom 3261	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
269	267, 268	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
270		biidd 262	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (♯‘(ℎ supp 0 )) → (ℎ ∈ 𝐻 ↔ ℎ ∈ 𝐻))
271	270	ceqsralv 3478	. . . . . . . . . . . . 13 ⊢ ((♯‘(ℎ supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ℎ ∈ 𝐻))
272	271	biimpcd 249	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
273	272	ralimi 3070	. . . . . . . . . . 11 ⊢ (∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
274	269, 273	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
275		fvoveq1 7377	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑋 → (♯‘(ℎ supp 0 )) = (♯‘(𝑋 supp 0 )))
276	275	eleq1d 2818	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑋 → ((♯‘(ℎ supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
277		eleq1 2821	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑋 → (ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻))
278	276, 277	imbi12d 344	. . . . . . . . . . 11 ⊢ (ℎ = 𝑋 → (((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
279	278	rspcv 3569	. . . . . . . . . 10 ⊢ (𝑋 ∈ (𝐵 ↑_m 𝐼) → (∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
280	274, 279	syl5com 31	. . . . . . . . 9 ⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑_m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
281	280	com23 86	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ → (𝑋 ∈ (𝐵 ↑_m 𝐼) → 𝑋 ∈ 𝐻)))
282	281	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵 ↑_m 𝐼) → 𝑋 ∈ 𝐻))
283	6, 282	sylbird 260	. . . . . 6 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋:𝐼⟶𝐵 → 𝑋 ∈ 𝐻))
284	283	imp 406	. . . . 5 ⊢ (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧ 𝑋:𝐼⟶𝐵) → 𝑋 ∈ 𝐻)
285	284	an32s 652	. . . 4 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋 ∈ 𝐻)
286	285	adantlr 715	. . 3 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋 ∈ 𝐻)
287		ovex 7387	. . . . 5 ⊢ (𝑋 supp 0 ) ∈ V
288		hasheq0 14274	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
289	287, 288	ax-mp 5	. . . 4 ⊢ ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
290		ffn 6658	. . . . . . . 8 ⊢ (𝑋:𝐼⟶𝐵 → 𝑋 Fn 𝐼)
291	290	ad2antlr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
292	4	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉)
293	28	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
294		fnsuppeq0 8130	. . . . . . 7 ⊢ ((𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
295	291, 292, 293, 294	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296	295	biimpa 476	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
297		fsuppind.0	. . . . . 6 ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
298	297	ad3antrrr 730	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
299	296, 298	eqeltrd 2833	. . . 4 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 ∈ 𝐻)
300	289, 299	sylan2b 594	. . 3 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋 ∈ 𝐻)
301		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
302	301	fsuppimpd 9262	. . . . 5 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
303		hashcl 14267	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ₀)
304	302, 303	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ₀)
305		elnn0 12392	. . . 4 ⊢ ((♯‘(𝑋 supp 0 )) ∈ ℕ₀ ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
306	304, 305	sylib 218	. . 3 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
307	286, 300, 306	mpjaodan 960	. 2 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 ∈ 𝐻)
308	307	anasss 466	1 ⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∃!weu 2565 ≠ wne 2929 ∀wral 3048 ∃wrex 3057 ∃!wreu 3345 {crab 3396 Vcvv 3437 ∖ cdif 3895 ∅c0 4282 ifcif 4476 {csn 4577 class class class wbr 5095 ↦ cmpt 5176 × cxp 5619 Fn wfn 6483 ⟶wf 6484 ‘cfv 6488 ℩crio 7310 (class class class)co 7354 ∘_f cof 7616 supp csupp 8098 ↑_m cmap 8758 Fincfn 8877 finSupp cfsupp 9254 0cc0 11015 1c1 11016 + caddc 11018 ℕcn 12134 ℕ₀cn0 12390 ♯chash 14241 Basecbs 17124 +_gcplusg 17165 0_gc0g 17347 Grpcgrp 18850

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-riota 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-of 7618 df-om 7805 df-1st 7929 df-2nd 7930 df-supp 8099 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-oadd 8397 df-er 8630 df-map 8760 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-fsupp 9255 df-dju 9803 df-card 9841 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-nn 12135 df-n0 12391 df-z 12478 df-uz 12741 df-fz 13412 df-hash 14242 df-0g 17349 df-mgm 18552 df-sgrp 18631 df-mnd 18647 df-grp 18853

This theorem is referenced by: fsuppssind 42714

W3C validator