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 43022

Description: Induction on functions 𝐹:𝐴⟶𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21713 and frlmplusgval 21721). This theorem is structurally general for polynomial proof usage (see mplelbas 21947 and mpladd 21965). 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 6846	. . . . . . . . . 10 ⊢ 𝐵 ∈ V
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ V)
4		fsuppind.v	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
5	3, 4	elmapd 8778	. . . . . . . 8 ⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑_m 𝐼) ↔ 𝑋:𝐼⟶𝐵))
6	5	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵 ↑_m 𝐼) ↔ 𝑋:𝐼⟶𝐵))
7		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 1 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 1 = (♯‘(ℎ supp 0 ))))
8	7	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 1 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
9	8	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 1 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
10		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(ℎ supp 0 ))))
11	10	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
12	11	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
13		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘(ℎ supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 ))))
14	13	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
15	14	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑗 + 1) → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
16		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑛 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑛 = (♯‘(ℎ supp 0 ))))
17	16	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑛 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
18	17	ralbidv 3161	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑛 → (∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
19		eqcom 2744	. . . . . . . . . . . . . . . . 17 ⊢ (1 = (♯‘(ℎ supp 0 )) ↔ (♯‘(ℎ supp 0 )) = 1)
20		ovex 7391	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ supp 0 ) ∈ V
21		euhash1 14344	. . . . . . . . . . . . . . . . . 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 8803	. . . . . . . . . . . . . . . . . . . . 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 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → 0 ∈ V)
30		elsuppfn 8111	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
31	25, 26, 29, 30	syl3anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
32	31	eubidv 2587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )))
33		df-reu 3344	. . . . . . . . . . . . . . . . . 18 ⊢ (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))
34	32, 33	bitr4di 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))
35	24	ad2antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ Fn 𝐼)
36		fvex 6845	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ‘𝑥) ∈ V
37	36, 28	ifex 4518	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) ∈ V
38		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))
39	37, 38	fnmpti 6633	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼
40	39	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼)
41		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑣 → (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
42		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑣 → (ℎ‘𝑥) = (ℎ‘𝑣))
43	41, 42	ifbieq1d 4492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑣 → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
44	43, 38, 37	fvmpt3i 6945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
45	44	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ))
46		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (ℎ‘𝑣) = (ℎ‘𝑣))
47		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼)
48		simplr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )
49		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑣 → (ℎ‘𝑐) = (ℎ‘𝑣))
50	49	neeq1d 2992	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = 𝑣 → ((ℎ‘𝑐) ≠ 0 ↔ (ℎ‘𝑣) ≠ 0 ))
51	50	riota2 7340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑣 ∈ 𝐼 ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((ℎ‘𝑣) ≠ 0 ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣))
52	47, 48, 51	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((ℎ‘𝑣) ≠ 0 ↔ (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣))
53		necom 2986	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ( 0 ≠ (ℎ‘𝑣) ↔ (ℎ‘𝑣) ≠ 0 )
54		eqcom 2744	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → 0 = (ℎ‘𝑣)))
58	57	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ ¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 0 = (ℎ‘𝑣))
59	46, 58	ifeqda 4504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ) = (ℎ‘𝑣))
60	45, 59	eqtr2d 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (ℎ‘𝑣) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣))
61	35, 40, 60	eqfnfvd 6978	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )))
62		riotacl 7332	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼)
63	62	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼)
64		elmapi 8787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ∈ (𝐵 ↑_m 𝐼) → ℎ:𝐼⟶𝐵)
65	64	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ:𝐼⟶𝐵)
66	65, 63	ffvelcdmd 7029	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵)
67		fsuppind.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
68	67	ralrimivva 3181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
69	68	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70		eqeq2 2749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 = 𝑎 ↔ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
71	70	ifbid 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ))
72	71	mpteq2dv 5180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )))
73	72	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘𝑥) = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))
75	74	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑏 = (ℎ‘𝑥) ↔ 𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))))
76	75	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∧ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 𝑏 = (ℎ‘𝑥))
77	76	ifeq1da 4499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))
78	77	mpteq2dv 5180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )))
79	78	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻))
80	73, 79	rspc2va 3577	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼 ∧ (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)
81	63, 66, 69, 80	syl21anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑_m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)
82	61, 81	eqeltrd 2837	. . . . . . . . . . . . . . . . . 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 3130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
87		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
88	87	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))))
89		oveq1 7365	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
90	89	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ↔ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
91	88, 90	anbi12d 633	. . . . . . . . . . . . . . . . . . . . 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 18899	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ 𝐵)
95	94	ad5antr 735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 0 ∈ 𝐵)
96		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐵 ↑_m 𝐼) = (𝐵 ↑_m 𝐼)
97		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
98	97	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 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 8818	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑙‘𝑥) ∈ 𝐵)
101	95, 100	ifcld 4514	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ 𝐵)
102	101	fmpttd 7059	. . . . . . . . . . . . . . . . . . . . . . 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 733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉)
105	103, 104	elmapd 8778	. . . . . . . . . . . . . . . . . . . . . . 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 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑_m 𝐼))
108		ovexd 7393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
109		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ 𝐼)
110		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙‘𝑧) ≠ 0 )
111		elmapfn 8803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑙 ∈ (𝐵 ↑_m 𝐼) → 𝑙 Fn 𝐼)
112	111	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
113	112	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
114	4	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝐼 ∈ 𝑉)
115	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 0 ∈ V)
116		elsuppfn 8111	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )))
117	113, 114, 115, 116	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )))
118	109, 110, 117	mpbir2and 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
119		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
120	119	nnnn0d 12463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈ ℕ₀)
121		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
122	121	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
123		hashdifsnp1 14430	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1376	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126		eldifsn 4730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧))
127		fvex 6845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑙‘𝑥) ∈ V
128	28, 127	ifex 4518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ V
129		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))
130	128, 129	fnmpti 6633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼)
132	4	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉)
133	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 0 ∈ V)
134		elsuppfn 8111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 )))
135	131, 132, 133, 134	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 )))
136		iftrue 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 )
137		olc 869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
138	136, 137	2thd 265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
139		iffalse 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (¬ 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = (𝑙‘𝑣))
140	139	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (¬ 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ (𝑙‘𝑣) = 0 ))
141		biorf 937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (¬ 𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 )))
142		orcom 871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)))
148		neanior 3026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧) ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))
149	147, 148	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))
150	149	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑣 → (𝑥 = 𝑧 ↔ 𝑣 = 𝑧))
154		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑥 = 𝑣 → (𝑙‘𝑥) = (𝑙‘𝑣))
155	153, 154	ifbieq2d 4494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
156	155, 129, 128	fvmpt3i 6945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
157	156	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)))
158	157	neeq1d 2992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 )))
162	160, 132, 133, 161	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 )))
163	162	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))
168	167	fveq2d 6836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
169	168	adantrl 717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
170	125, 169	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))
171	127, 28	ifex 4518	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) ∈ V
172		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))
173	171, 172	fnmpti 6633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼)
175		inidm 4168	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐼 ∩ 𝐼) = 𝐼
176	131, 174, 132, 132, 175	offn 7635	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) Fn 𝐼)
177	153, 154	ifbieq1d 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))
178	177, 172, 171	fvmpt3i 6945	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7633	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )))
181	92	ad4antr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝐺 ∈ Grp)
182		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8818	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) ∈ 𝐵)
186		fsuppind.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ + = (+_g‘𝐺)
187	1, 186, 27	grplid 18901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ( 0 + (𝑙‘𝑣)) = (𝑙‘𝑣))
188	1, 186, 27	grprid 18902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ((𝑙‘𝑣) + 0 ) = (𝑙‘𝑣))
189	187, 188	ifeq12d 4489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)))
190	181, 185, 189	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)))
191		ovif12 7458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 ))
192		ifid 4508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) = (𝑙‘𝑣)
193	192	eqcomi 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑙‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣))
194	190, 191, 193	3eqtr4g 2797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = (𝑙‘𝑣))
195	180, 194	eqtr2d 2773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) = (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣))
196	160, 176, 195	eqfnfvd 6978	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
197	196	adantrl 717	. . . . . . . . . . . . . . . . . . . . . . 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 720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
200	91, 107, 199	rspcedvdw 3568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
201	111	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
202	4	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼 ∈ 𝑉)
203	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
204		suppvalfn 8109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 })
205	201, 202, 203, 204	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 })
206		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
207		peano2nn 12158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
208	207	ad3antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
209	208	nnne0d 12196	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
210	206, 209	eqnetrrd 3001	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
211		ovex 7391	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑙 supp 0 ) ∈ V
212		hasheq0 14287	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
213	212	necon3bid 2977	. . . . . . . . . . . . . . . . . . . . . . . 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 3001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅)
217		rabn0 4330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅ ↔ ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 )
218	216, 217	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 )
219	200, 218	reximddv 3154	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 ∃𝑚 ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))
220		rexcom 3267	. . . . . . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))
223		fvoveq1 7381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ℎ = 𝑚 → (♯‘(ℎ supp 0 )) = (♯‘(𝑚 supp 0 )))
224	223	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = 𝑚 → (𝑗 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
225		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ℎ = 𝑚 → (ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻))
226	224, 225	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (ℎ = 𝑚 → ((𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)))
227	226	rspccva 3564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))
228	227	adantll 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))
229	228	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
230	229	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵 ↑_m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
231	230	adantlrr 722	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻)
232	231	adantrr 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑚 ∈ 𝐻)
233		simplrr 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑧 ∈ 𝐼)
234	97	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ (𝐵 ↑_m 𝐼))
235	96, 234, 233	mapfvd 8818	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑙‘𝑧) ∈ 𝐵)
236	68	ad5antr 735	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
237		equequ2 2028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑧 → (𝑥 = 𝑎 ↔ 𝑥 = 𝑧))
238	237	ifbid 4491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
239	238	mpteq2dv 5180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑧 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
240	239	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = 𝑧 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
241		fveq2 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑧 → (𝑙‘𝑥) = (𝑙‘𝑧))
242	241	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝑧 → (𝑏 = (𝑙‘𝑥) ↔ 𝑏 = (𝑙‘𝑧)))
243	242	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑏 = (𝑙‘𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙‘𝑥))
244	243	ifeq1da 4499	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = (𝑙‘𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))
245	244	mpteq2dv 5180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = (𝑙‘𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))
246	245	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = (𝑙‘𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻))
247	240, 246	rspc2va 3577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)
248	233, 235, 236, 247	syl21anc 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)
249		fsuppind.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘_f + 𝑦) ∈ 𝐻)
250	249	ralrimivva 3181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻)
251	250	ad5antr 735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻)
252		ovrspc2v 7384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 ∈ 𝐻 ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘_f + 𝑦) ∈ 𝐻) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻)
253	232, 248, 251, 252	syl21anc 838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑_m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑_m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑚 ∘_f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻)
254	222, 253	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . 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 3195	. . . . . . . . . . . . . . . . . 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 3129	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀𝑙 ∈ (𝐵 ↑_m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻))
260		fvoveq1 7381	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = ℎ → (♯‘(𝑙 supp 0 )) = (♯‘(ℎ supp 0 )))
261	260	eqeq2d 2748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 ))))
262		eleq1w 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = ℎ → (𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻))
263	261, 262	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = ℎ → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)))
264	263	cbvralvw 3216	. . . . . . . . . . . . . . 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 12166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
267	266	ralrimiva 3130	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑_m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))
268		ralcom 3266	. . . . . . . . . . . 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 3471	. . . . . . . . . . . . 13 ⊢ ((♯‘(ℎ supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ℎ ∈ 𝐻))
272	271	biimpcd 249	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
273	272	ralimi 3075	. . . . . . . . . . 11 ⊢ (∀ℎ ∈ (𝐵 ↑_m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
274	269, 273	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑_m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻))
275		fvoveq1 7381	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑋 → (♯‘(ℎ supp 0 )) = (♯‘(𝑋 supp 0 )))
276	275	eleq1d 2822	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑋 → ((♯‘(ℎ supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
277		eleq1 2825	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑋 → (ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻))
278	276, 277	imbi12d 344	. . . . . . . . . . 11 ⊢ (ℎ = 𝑋 → (((♯‘(ℎ supp 0 )) ∈ ℕ → ℎ ∈ 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋 ∈ 𝐻)))
279	278	rspcv 3561	. . . . . . . . . 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 653	. . . 4 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋 ∈ 𝐻)
286	285	adantlr 716	. . 3 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋 ∈ 𝐻)
287		ovex 7391	. . . . 5 ⊢ (𝑋 supp 0 ) ∈ V
288		hasheq0 14287	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
289	287, 288	ax-mp 5	. . . 4 ⊢ ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
290		ffn 6660	. . . . . . . 8 ⊢ (𝑋:𝐼⟶𝐵 → 𝑋 Fn 𝐼)
291	290	ad2antlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
292	4	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉)
293	28	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
294		fnsuppeq0 8133	. . . . . . 7 ⊢ ((𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
295	291, 292, 293, 294	syl3anc 1374	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296	295	biimpa 476	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
297		fsuppind.0	. . . . . 6 ⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
298	297	ad3antrrr 731	. . . . 5 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
299	296, 298	eqeltrd 2837	. . . 4 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 ∈ 𝐻)
300	289, 299	sylan2b 595	. . 3 ⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋 ∈ 𝐻)
301		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
302	301	fsuppimpd 9273	. . . . 5 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
303		hashcl 14280	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ₀)
304	302, 303	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ₀)
305		elnn0 12404	. . . 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 961	. 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 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃!weu 2569 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∃!wreu 3341 {crab 3390 Vcvv 3430 ∖ cdif 3887 ∅c0 4274 ifcif 4467 {csn 4568 class class class wbr 5086 ↦ cmpt 5167 × cxp 5620 Fn wfn 6485 ⟶wf 6486 ‘cfv 6490 ℩crio 7314 (class class class)co 7358 ∘_f cof 7620 supp csupp 8101 ↑_m cmap 8764 Fincfn 8884 finSupp cfsupp 9265 0cc0 11027 1c1 11028 + caddc 11030 ℕcn 12146 ℕ₀cn0 12402 ♯chash 14254 Basecbs 17137 +_gcplusg 17178 0_gc0g 17360 Grpcgrp 18867

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8102 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-oadd 8400 df-er 8634 df-map 8766 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-dju 9814 df-card 9852 df-pnf 11169 df-mnf 11170 df-xr 11171 df-ltxr 11172 df-le 11173 df-sub 11367 df-neg 11368 df-nn 12147 df-n0 12403 df-z 12490 df-uz 12753 df-fz 13425 df-hash 14255 df-0g 17362 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-grp 18870

This theorem is referenced by: fsuppssind 43025

W3C validator