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

Theorem fsuppind 41112
Description: Induction on functions 𝐹:𝐴𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21295 and frlmplusgval 21303). This theorem is structurally general for polynomial proof usage (see mplelbas 21532 and mpladd 21550). Note that hypothesis 0 is redundant when 𝐼 is nonempty. (Contributed by SN, 18-May-2024.)
Hypotheses
Ref Expression
fsuppind.b 𝐵 = (Base‘𝐺)
fsuppind.z 0 = (0g𝐺)
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.
StepHypRef Expression
1 fsuppind.b . . . . . . . . . . 11 𝐵 = (Base‘𝐺)
21fvexi 6902 . . . . . . . . . 10 𝐵 ∈ V
32a1i 11 . . . . . . . . 9 (𝜑𝐵 ∈ V)
4 fsuppind.v . . . . . . . . 9 (𝜑𝐼𝑉)
53, 4elmapd 8830 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
65adantr 482 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
7 eqeq1 2737 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝑖 = (♯‘( supp 0 )) ↔ 1 = (♯‘( supp 0 ))))
87imbi1d 342 . . . . . . . . . . . . . . 15 (𝑖 = 1 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (1 = (♯‘( supp 0 )) → 𝐻)))
98ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = 1 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻)))
10 eqeq1 2737 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘( supp 0 ))))
1110imbi1d 342 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘( supp 0 )) → 𝐻)))
1211ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)))
13 eqeq1 2737 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘( supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
1413imbi1d 342 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
1514ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 + 1) → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
16 eqeq1 2737 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑛 = (♯‘( supp 0 ))))
1716imbi1d 342 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑛 = (♯‘( supp 0 )) → 𝐻)))
1817ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻)))
19 eqcom 2740 . . . . . . . . . . . . . . . . 17 (1 = (♯‘( supp 0 )) ↔ (♯‘( supp 0 )) = 1)
20 ovex 7437 . . . . . . . . . . . . . . . . . 18 ( supp 0 ) ∈ V
21 euhash1 14376 . . . . . . . . . . . . . . . . . 18 (( supp 0 ) ∈ V → ((♯‘( supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ ( supp 0 )))
2220, 21ax-mp 5 . . . . . . . . . . . . . . . . 17 ((♯‘( supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ ( supp 0 ))
2319, 22bitri 275 . . . . . . . . . . . . . . . 16 (1 = (♯‘( supp 0 )) ↔ ∃!𝑐 𝑐 ∈ ( supp 0 ))
24 elmapfn 8855 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (𝐵m 𝐼) → Fn 𝐼)
2524adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → Fn 𝐼)
264adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 𝐼𝑉)
27 fsuppind.z . . . . . . . . . . . . . . . . . . . . . 22 0 = (0g𝐺)
2827fvexi 6902 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
2928a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 0 ∈ V)
30 elsuppfn 8151 . . . . . . . . . . . . . . . . . . . 20 (( Fn 𝐼𝐼𝑉0 ∈ V) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3125, 26, 29, 30syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∈ (𝐵m 𝐼)) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3231eubidv 2581 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 )))
33 df-reu 3378 . . . . . . . . . . . . . . . . . 18 (∃!𝑐𝐼 (𝑐) ≠ 0 ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 ))
3432, 33bitr4di 289 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐𝐼 (𝑐) ≠ 0 ))
3524ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → Fn 𝐼)
36 fvex 6901 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥) ∈ V
3736, 28ifex 4577 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) ∈ V
38 eqid 2733 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
3937, 38fnmpti 6690 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼
4039a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼)
41 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
42 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥) = (𝑣))
4341, 42ifbieq1d 4551 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑣 → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4443, 38, 37fvmpt3i 6999 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4544adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
46 eqidd 2734 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → (𝑣) = (𝑣))
47 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
48 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ∃!𝑐𝐼 (𝑐) ≠ 0 )
49 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑣 → (𝑐) = (𝑣))
5049neeq1d 3001 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑣 → ((𝑐) ≠ 0 ↔ (𝑣) ≠ 0 ))
5150riota2 7386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣𝐼 ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
5247, 48, 51syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
53 necom 2995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( 0 ≠ (𝑣) ↔ (𝑣) ≠ 0 )
54 eqcom 2740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣)
5552, 53, 543bitr4g 314 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5655biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) → 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5756necon1bd 2959 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) → 0 = (𝑣)))
5857imp 408 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ ¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → 0 = (𝑣))
5946, 58ifeqda 4563 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ) = (𝑣))
6045, 59eqtr2d 2774 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (𝑣) = ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣))
6135, 40, 60eqfnfvd 7031 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
62 riotacl 7378 . . . . . . . . . . . . . . . . . . . . 21 (∃!𝑐𝐼 (𝑐) ≠ 0 → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
6362adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
64 elmapi 8839 . . . . . . . . . . . . . . . . . . . . . 22 ( ∈ (𝐵m 𝐼) → :𝐼𝐵)
6564ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → :𝐼𝐵)
6665, 63ffvelcdmd 7083 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵)
67 fsuppind.1 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎𝐼𝑏𝐵)) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6867ralrimivva 3201 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6968ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70 eqeq2 2745 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥 = 𝑎𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )))
7170ifbid 4550 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ))
7271mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )))
7372eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥) = (‘(𝑐𝐼 (𝑐) ≠ 0 )))
7574eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑏 = (𝑥) ↔ 𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 ))))
7675biimparc 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∧ 𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )) → 𝑏 = (𝑥))
7776ifeq1da 4558 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
7877mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
7978eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻))
8073, 79rspc2va 3622 . . . . . . . . . . . . . . . . . . . 20 ((((𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼 ∧ (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8163, 66, 69, 80syl21anc 837 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8261, 81eqeltrd 2834 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → 𝐻)
8382ex 414 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐𝐼 (𝑐) ≠ 0𝐻))
8434, 83sylbid 239 . . . . . . . . . . . . . . . 16 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) → 𝐻))
8523, 84biimtrid 241 . . . . . . . . . . . . . . 15 ((𝜑 ∈ (𝐵m 𝐼)) → (1 = (♯‘( supp 0 )) → 𝐻))
8685ralrimiva 3147 . . . . . . . . . . . . . 14 (𝜑 → ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻))
87 fsuppind.g . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺 ∈ Grp)
881, 27grpidcl 18846 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ Grp → 0𝐵)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑0𝐵)
9089ad5antr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 0𝐵)
91 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵m 𝐼) = (𝐵m 𝐼)
92 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵m 𝐼))
9392ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑙 ∈ (𝐵m 𝐼))
94 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑥𝐼)
9591, 93, 94mapfvd 8869 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → (𝑙𝑥) ∈ 𝐵)
9690, 95ifcld 4573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ 𝐵)
9796fmpttd 7110 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵)
982a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐵 ∈ V)
994ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
10098, 99elmapd 8830 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼) ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵))
10197, 100mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
102101adantrl 715 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
103 fvoveq1 7427 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
104103eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))))
105 oveq1 7411 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
106105eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ↔ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
107104, 106anbi12d 632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))))
108107adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) ∧ 𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))))
109 ovexd 7439 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
110 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧𝐼)
111 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙𝑧) ≠ 0 )
112 elmapfn 8855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (𝐵m 𝐼) → 𝑙 Fn 𝐼)
113112ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
114113adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
1154ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝐼𝑉)
11628a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 0 ∈ V)
117 elsuppfn 8151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
118114, 115, 116, 117syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
119110, 111, 118mpbir2and 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
120 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
121120nnnn0d 12528 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ0)
122 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
123122eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
124 hashdifsnp1 14453 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) → ((♯‘(𝑙 supp 0 )) = (𝑗 + 1) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗))
125124imp 408 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) ∧ (♯‘(𝑙 supp 0 )) = (𝑗 + 1)) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126109, 119, 121, 123, 125syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
127 eldifsn 4789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧))
128 fvex 6901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙𝑥) ∈ V
12928, 128ifex 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ V
130 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))
131129, 130fnmpti 6690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼
132131a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼)
1334ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
13428a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 0 ∈ V)
135 elsuppfn 8151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
136132, 133, 134, 135syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
137 iftrue 4533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 )
138 olc 867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → ((𝑙𝑣) = 0𝑣 = 𝑧))
139137, 1382thd 265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
140 iffalse 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = (𝑙𝑣))
141140eqeq1d 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ (𝑙𝑣) = 0 ))
142 biorf 936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 )))
143 orcom 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑙𝑣) = 0𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 ))
144142, 143bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
145141, 144bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
146139, 145pm2.61i 182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧))
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
148147necon3abid 2978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧)))
149 neanior 3036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑙𝑣) ≠ 0𝑣𝑧) ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧))
150148, 149bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ((𝑙𝑣) ≠ 0𝑣𝑧)))
151150anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧))))
152 anass 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧)))
153151, 152bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
154 equequ1 2029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑥 = 𝑧𝑣 = 𝑧))
155 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑙𝑥) = (𝑙𝑣))
156154, 155ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
157156, 130, 129fvmpt3i 6999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
158157adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
159158neeq1d 3001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ))
160159pm5.32da 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 )))
161113adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 Fn 𝐼)
162 elsuppfn 8151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
163161, 133, 134, 162syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
164163anbi1d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
165153, 160, 1643bitr4d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧)))
166136, 165bitr2d 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧) ↔ 𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
167127, 166bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
168167eqrdv 2731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))
169168fveq2d 6892 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
170169adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
171126, 170eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
172128, 28ifex 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑥 = 𝑧, (𝑙𝑥), 0 ) ∈ V
173 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
174172, 173fnmpti 6690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼
175174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼)
176 inidm 4217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐼𝐼) = 𝐼
177132, 175, 133, 133, 176offn 7678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) Fn 𝐼)
178154, 155ifbieq1d 4551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
179178, 173, 172fvmpt3i 6999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
180179adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
181132, 175, 133, 133, 176, 158, 180ofval 7676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )))
18287ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝐺 ∈ Grp)
183 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙𝑧) ≠ 0𝑣𝐼)) → 𝑙 ∈ (𝐵m 𝐼))
184183anassrs 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑙 ∈ (𝐵m 𝐼))
185 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
18691, 184, 185mapfvd 8869 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) ∈ 𝐵)
187 fsuppind.p . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 + = (+g𝐺)
1881, 187, 27grplid 18848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ( 0 + (𝑙𝑣)) = (𝑙𝑣))
1891, 187, 27grprid 18849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ((𝑙𝑣) + 0 ) = (𝑙𝑣))
190188, 189ifeq12d 4548 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
191182, 186, 190syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
192 ovif12 7503 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 ))
193 ifid 4567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)) = (𝑙𝑣)
194193eqcomi 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣))
195191, 192, 1943eqtr4g 2798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = (𝑙𝑣))
196181, 195eqtr2d 2774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) = (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣))
197161, 177, 196eqfnfvd 7031 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
198197adantrl 715 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
199171, 198jca 513 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
200199adantllr 718 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
201102, 108, 200rspcedvd 3614 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
202112ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
2034ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼𝑉)
20428a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
205 suppvalfn 8149 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
206202, 203, 204, 205syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
207 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
208 peano2nn 12220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
209208ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
210209nnne0d 12258 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
211207, 210eqnetrrd 3010 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
212 ovex 7437 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 supp 0 ) ∈ V
213 hasheq0 14319 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
214213necon3bid 2986 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
215212, 214mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
216211, 215mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) ≠ ∅)
217206, 216eqnetrrd 3010 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 } ≠ ∅)
218 rabn0 4384 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 } ≠ ∅ ↔ ∃𝑧𝐼 (𝑙𝑧) ≠ 0 )
219217, 218sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼 (𝑙𝑧) ≠ 0 )
220201, 219reximddv 3172 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
221 rexcom 3288 . . . . . . . . . . . . . . . . . . 19 (∃𝑧𝐼𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ ∃𝑚 ∈ (𝐵m 𝐼)∃𝑧𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
222220, 221sylib 217 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑚 ∈ (𝐵m 𝐼)∃𝑧𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
223 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
224 fvoveq1 7427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ( = 𝑚 → (♯‘( supp 0 )) = (♯‘(𝑚 supp 0 )))
225224eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝑗 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
226 eleq1w 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝐻𝑚𝐻))
227225, 226imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( = 𝑚 → ((𝑗 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻)))
228227rspccva 3611 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
229228adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
230229imp 408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
231230adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
232231adantlrr 720 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
233232adantrr 716 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑚𝐻)
234 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑧𝐼)
23592ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 ∈ (𝐵m 𝐼))
23691, 235, 234mapfvd 8869 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑙𝑧) ∈ 𝐵)
23768ad5antr 733 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
238 equequ2 2030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑧 → (𝑥 = 𝑎𝑥 = 𝑧))
239238ifbid 4550 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
240239mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
241240eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑧 → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
242 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑧 → (𝑙𝑥) = (𝑙𝑧))
243242eqeq2d 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → (𝑏 = (𝑙𝑥) ↔ 𝑏 = (𝑙𝑧)))
244243biimparc 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 = (𝑙𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙𝑥))
245244ifeq1da 4558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = (𝑙𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
246245mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = (𝑙𝑧) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))
247246eleq1d 2819 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (𝑙𝑧) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻))
248241, 247rspc2va 3622 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧𝐼 ∧ (𝑙𝑧) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
249234, 236, 237, 248syl21anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
250 fsuppind.2 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑥𝐻𝑦𝐻)) → (𝑥f + 𝑦) ∈ 𝐻)
251250ralrimivva 3201 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
252251ad5antr 733 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
253 ovrspc2v 7430 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑚𝐻 ∧ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
254233, 249, 252, 253syl21anc 837 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
255223, 254eqeltrd 2834 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙𝐻)
256255ex 414 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) → 𝑙𝐻))
257256rexlimdvva 3212 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (∃𝑚 ∈ (𝐵m 𝐼)∃𝑧𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) → 𝑙𝐻))
258222, 257mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙𝐻)
259258exp32 422 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → (𝑙 ∈ (𝐵m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻)))
260259ralrimiv 3146 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → ∀𝑙 ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻))
261 fvoveq1 7427 . . . . . . . . . . . . . . . . . 18 (𝑙 = → (♯‘(𝑙 supp 0 )) = (♯‘( supp 0 )))
262261eqeq2d 2744 . . . . . . . . . . . . . . . . 17 (𝑙 = → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
263 eleq1w 2817 . . . . . . . . . . . . . . . . 17 (𝑙 = → (𝑙𝐻𝐻))
264262, 263imbi12d 345 . . . . . . . . . . . . . . . 16 (𝑙 = → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
265264cbvralvw 3235 . . . . . . . . . . . . . . 15 (∀𝑙 ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻) ↔ ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻))
266260, 265sylib 217 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻))
2679, 12, 15, 18, 86, 266nnindd 12228 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
268267ralrimiva 3147 . . . . . . . . . . . 12 (𝜑 → ∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
269 ralcom 3287 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
270268, 269sylib 217 . . . . . . . . . . 11 (𝜑 → ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
271 biidd 262 . . . . . . . . . . . . . 14 (𝑛 = (♯‘( supp 0 )) → (𝐻𝐻))
272271ceqsralv 3513 . . . . . . . . . . . . 13 ((♯‘( supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ 𝐻))
273272biimpcd 248 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ((♯‘( supp 0 )) ∈ ℕ → 𝐻))
274273ralimi 3084 . . . . . . . . . . 11 (∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
275270, 274syl 17 . . . . . . . . . 10 (𝜑 → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
276 fvoveq1 7427 . . . . . . . . . . . . 13 ( = 𝑋 → (♯‘( supp 0 )) = (♯‘(𝑋 supp 0 )))
277276eleq1d 2819 . . . . . . . . . . . 12 ( = 𝑋 → ((♯‘( supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
278 eleq1 2822 . . . . . . . . . . . 12 ( = 𝑋 → (𝐻𝑋𝐻))
279277, 278imbi12d 345 . . . . . . . . . . 11 ( = 𝑋 → (((♯‘( supp 0 )) ∈ ℕ → 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
280279rspcv 3608 . . . . . . . . . 10 (𝑋 ∈ (𝐵m 𝐼) → (∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
281275, 280syl5com 31 . . . . . . . . 9 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
282281com23 86 . . . . . . . 8 (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻)))
283282imp 408 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻))
2846, 283sylbird 260 . . . . . 6 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋:𝐼𝐵𝑋𝐻))
285284imp 408 . . . . 5 (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧ 𝑋:𝐼𝐵) → 𝑋𝐻)
286285an32s 651 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
287286adantlr 714 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
288 ovex 7437 . . . . 5 (𝑋 supp 0 ) ∈ V
289 hasheq0 14319 . . . . 5 ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
290288, 289ax-mp 5 . . . 4 ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
291 ffn 6714 . . . . . . . 8 (𝑋:𝐼𝐵𝑋 Fn 𝐼)
292291ad2antlr 726 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
2934ad2antrr 725 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼𝑉)
29428a1i 11 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
295 fnsuppeq0 8172 . . . . . . 7 ((𝑋 Fn 𝐼𝐼𝑉0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296292, 293, 294, 295syl3anc 1372 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
297296biimpa 478 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
298 fsuppind.0 . . . . . 6 (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
299298ad3antrrr 729 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
300297, 299eqeltrd 2834 . . . 4 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋𝐻)
301290, 300sylan2b 595 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋𝐻)
302 simpr 486 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
303302fsuppimpd 9365 . . . . 5 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
304 hashcl 14312 . . . . 5 ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
305303, 304syl 17 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
306 elnn0 12470 . . . 4 ((♯‘(𝑋 supp 0 )) ∈ ℕ0 ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
307305, 306sylib 217 . . 3 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
308287, 301, 307mpjaodan 958 . 2 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋𝐻)
309308anasss 468 1 ((𝜑 ∧ (𝑋:𝐼𝐵𝑋 finSupp 0 )) → 𝑋𝐻)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3a 1088   = wceq 1542  wcel 2107  ∃!weu 2563  wne 2941  wral 3062  wrex 3071  ∃!wreu 3375  {crab 3433  Vcvv 3475  cdif 3944  c0 4321  ifcif 4527  {csn 4627   class class class wbr 5147  cmpt 5230   × cxp 5673   Fn wfn 6535  wf 6536  cfv 6540  crio 7359  (class class class)co 7404  f cof 7663   supp csupp 8141  m cmap 8816  Fincfn 8935   finSupp cfsupp 9357  0cc0 11106  1c1 11107   + caddc 11109  cn 12208  0cn0 12468  chash 14286  Basecbs 17140  +gcplusg 17193  0gc0g 17381  Grpcgrp 18815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-hash 14287  df-0g 17383  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818
This theorem is referenced by:  fsuppssind  41115
  Copyright terms: Public domain W3C validator