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 40751
Description: Induction on functions 𝐹:𝐴𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21162 and frlmplusgval 21170). This theorem is structurally general for polynomial proof usage (see mplelbas 21399 and mpladd 21413). 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 6856 . . . . . . . . . 10 𝐵 ∈ V
32a1i 11 . . . . . . . . 9 (𝜑𝐵 ∈ V)
4 fsuppind.v . . . . . . . . 9 (𝜑𝐼𝑉)
53, 4elmapd 8779 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
65adantr 481 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
7 eqeq1 2740 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝑖 = (♯‘( supp 0 )) ↔ 1 = (♯‘( supp 0 ))))
87imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = 1 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (1 = (♯‘( supp 0 )) → 𝐻)))
98ralbidv 3174 . . . . . . . . . . . . . 14 (𝑖 = 1 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻)))
10 eqeq1 2740 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘( supp 0 ))))
1110imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘( supp 0 )) → 𝐻)))
1211ralbidv 3174 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)))
13 eqeq1 2740 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘( supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
1413imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
1514ralbidv 3174 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 + 1) → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
16 eqeq1 2740 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑛 = (♯‘( supp 0 ))))
1716imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑛 = (♯‘( supp 0 )) → 𝐻)))
1817ralbidv 3174 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻)))
19 eqcom 2743 . . . . . . . . . . . . . . . . 17 (1 = (♯‘( supp 0 )) ↔ (♯‘( supp 0 )) = 1)
20 ovex 7390 . . . . . . . . . . . . . . . . . 18 ( supp 0 ) ∈ V
21 euhash1 14320 . . . . . . . . . . . . . . . . . 18 (( supp 0 ) ∈ V → ((♯‘( supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ ( supp 0 )))
2220, 21ax-mp 5 . . . . . . . . . . . . . . . . 17 ((♯‘( supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ ( supp 0 ))
2319, 22bitri 274 . . . . . . . . . . . . . . . 16 (1 = (♯‘( supp 0 )) ↔ ∃!𝑐 𝑐 ∈ ( supp 0 ))
24 elmapfn 8803 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (𝐵m 𝐼) → Fn 𝐼)
2524adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → Fn 𝐼)
264adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 𝐼𝑉)
27 fsuppind.z . . . . . . . . . . . . . . . . . . . . . 22 0 = (0g𝐺)
2827fvexi 6856 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
2928a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 0 ∈ V)
30 elsuppfn 8102 . . . . . . . . . . . . . . . . . . . 20 (( Fn 𝐼𝐼𝑉0 ∈ V) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3125, 26, 29, 30syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∈ (𝐵m 𝐼)) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3231eubidv 2584 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 )))
33 df-reu 3354 . . . . . . . . . . . . . . . . . 18 (∃!𝑐𝐼 (𝑐) ≠ 0 ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 ))
3432, 33bitr4di 288 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐𝐼 (𝑐) ≠ 0 ))
3524ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → Fn 𝐼)
36 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥) ∈ V
3736, 28ifex 4536 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) ∈ V
38 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
3937, 38fnmpti 6644 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼
4039a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼)
41 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
42 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥) = (𝑣))
4341, 42ifbieq1d 4510 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑣 → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4443, 38, 37fvmpt3i 6953 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4544adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
46 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → (𝑣) = (𝑣))
47 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
48 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ∃!𝑐𝐼 (𝑐) ≠ 0 )
49 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑣 → (𝑐) = (𝑣))
5049neeq1d 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑣 → ((𝑐) ≠ 0 ↔ (𝑣) ≠ 0 ))
5150riota2 7339 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣𝐼 ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
5247, 48, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
53 necom 2997 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( 0 ≠ (𝑣) ↔ (𝑣) ≠ 0 )
54 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣)
5552, 53, 543bitr4g 313 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5655biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) → 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5756necon1bd 2961 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) → 0 = (𝑣)))
5857imp 407 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ ¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → 0 = (𝑣))
5946, 58ifeqda 4522 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ) = (𝑣))
6045, 59eqtr2d 2777 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (𝑣) = ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣))
6135, 40, 60eqfnfvd 6985 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
62 riotacl 7331 . . . . . . . . . . . . . . . . . . . . 21 (∃!𝑐𝐼 (𝑐) ≠ 0 → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
6362adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
64 elmapi 8787 . . . . . . . . . . . . . . . . . . . . . 22 ( ∈ (𝐵m 𝐼) → :𝐼𝐵)
6564ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → :𝐼𝐵)
6665, 63ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵)
67 fsuppind.1 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎𝐼𝑏𝐵)) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6867ralrimivva 3197 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6968ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥 = 𝑎𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )))
7170ifbid 4509 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ))
7271mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )))
7372eleq1d 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥) = (‘(𝑐𝐼 (𝑐) ≠ 0 )))
7574eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑏 = (𝑥) ↔ 𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 ))))
7675biimparc 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∧ 𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )) → 𝑏 = (𝑥))
7776ifeq1da 4517 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
7877mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
7978eleq1d 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻))
8073, 79rspc2va 3591 . . . . . . . . . . . . . . . . . . . 20 ((((𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼 ∧ (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8163, 66, 69, 80syl21anc 836 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8261, 81eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → 𝐻)
8382ex 413 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐𝐼 (𝑐) ≠ 0𝐻))
8434, 83sylbid 239 . . . . . . . . . . . . . . . 16 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) → 𝐻))
8523, 84biimtrid 241 . . . . . . . . . . . . . . 15 ((𝜑 ∈ (𝐵m 𝐼)) → (1 = (♯‘( supp 0 )) → 𝐻))
8685ralrimiva 3143 . . . . . . . . . . . . . 14 (𝜑 → ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻))
87 fsuppind.g . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺 ∈ Grp)
881, 27grpidcl 18778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ Grp → 0𝐵)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑0𝐵)
9089ad5antr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 0𝐵)
91 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵m 𝐼) = (𝐵m 𝐼)
92 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵m 𝐼))
9392ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑙 ∈ (𝐵m 𝐼))
94 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑥𝐼)
9591, 93, 94mapfvd 8817 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → (𝑙𝑥) ∈ 𝐵)
9690, 95ifcld 4532 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ 𝐵)
9796fmpttd 7063 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵)
982a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐵 ∈ V)
994ad4antr 730 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
10098, 99elmapd 8779 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼) ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵))
10197, 100mpbird 256 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
102101adantrl 714 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
103 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
104103eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))))
105 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
106105eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ↔ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
107104, 106anbi12d 631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))))
108107adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) ∧ 𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))))
109 ovexd 7392 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
110 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧𝐼)
111 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙𝑧) ≠ 0 )
112 elmapfn 8803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (𝐵m 𝐼) → 𝑙 Fn 𝐼)
113112ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
114113adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
1154ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝐼𝑉)
11628a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 0 ∈ V)
117 elsuppfn 8102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
118114, 115, 116, 117syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
119110, 111, 118mpbir2and 711 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
120 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
121120nnnn0d 12473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ0)
122 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
123122eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
124 hashdifsnp1 14395 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) → ((♯‘(𝑙 supp 0 )) = (𝑗 + 1) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗))
125124imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) ∧ (♯‘(𝑙 supp 0 )) = (𝑗 + 1)) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126109, 119, 121, 123, 125syl31anc 1373 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
127 eldifsn 4747 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧))
128 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙𝑥) ∈ V
12928, 128ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ V
130 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))
131129, 130fnmpti 6644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼
132131a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼)
1334ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
13428a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 0 ∈ V)
135 elsuppfn 8102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
136132, 133, 134, 135syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
137 iftrue 4492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 )
138 olc 866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → ((𝑙𝑣) = 0𝑣 = 𝑧))
139137, 1382thd 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
140 iffalse 4495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = (𝑙𝑣))
141140eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ (𝑙𝑣) = 0 ))
142 biorf 935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 )))
143 orcom 868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑙𝑣) = 0𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 ))
144142, 143bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
145141, 144bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧)))
149 neanior 3037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑙𝑣) ≠ 0𝑣𝑧) ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧))
150148, 149bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ((𝑙𝑣) ≠ 0𝑣𝑧)))
151150anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧))))
152 anass 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧)))
153151, 152bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
154 equequ1 2028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑥 = 𝑧𝑣 = 𝑧))
155 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑙𝑥) = (𝑙𝑣))
156154, 155ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
157156, 130, 129fvmpt3i 6953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
158157adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
159158neeq1d 3003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ))
160159pm5.32da 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 )))
161113adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 Fn 𝐼)
162 elsuppfn 8102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
163161, 133, 134, 162syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
164163anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
165153, 160, 1643bitr4d 310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧)))
166136, 165bitr2d 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧) ↔ 𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
167127, 166bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
168167eqrdv 2734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))
169168fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
170169adantrl 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
171126, 170eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
172128, 28ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑥 = 𝑧, (𝑙𝑥), 0 ) ∈ V
173 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
174172, 173fnmpti 6644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼
175174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼)
176 inidm 4178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐼𝐼) = 𝐼
177132, 175, 133, 133, 176offn 7630 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) Fn 𝐼)
178154, 155ifbieq1d 4510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
179178, 173, 172fvmpt3i 6953 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
180179adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
181132, 175, 133, 133, 176, 158, 180ofval 7628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )))
18287ad4antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝐺 ∈ Grp)
183 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙𝑧) ≠ 0𝑣𝐼)) → 𝑙 ∈ (𝐵m 𝐼))
184183anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑙 ∈ (𝐵m 𝐼))
185 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
18691, 184, 185mapfvd 8817 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) ∈ 𝐵)
187 fsuppind.p . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 + = (+g𝐺)
1881, 187, 27grplid 18780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ( 0 + (𝑙𝑣)) = (𝑙𝑣))
1891, 187, 27grprid 18781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ((𝑙𝑣) + 0 ) = (𝑙𝑣))
190188, 189ifeq12d 4507 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
191182, 186, 190syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
192 ovif12 7456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 ))
193 ifid 4526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)) = (𝑙𝑣)
194193eqcomi 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣))
195191, 192, 1943eqtr4g 2801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = (𝑙𝑣))
196181, 195eqtr2d 2777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) = (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣))
197161, 177, 196eqfnfvd 6985 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
198197adantrl 714 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
199171, 198jca 512 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
200199adantllr 717 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
201102, 108, 200rspcedvd 3583 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
202112ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
2034ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼𝑉)
20428a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
205 suppvalfn 8100 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
206202, 203, 204, 205syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
207 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
208 peano2nn 12165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
209208ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
210209nnne0d 12203 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
211207, 210eqnetrrd 3012 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
212 ovex 7390 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 supp 0 ) ∈ V
213 hasheq0 14263 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
214213necon3bid 2988 . . . . . . . . . . . . . . . . . . . . . . . 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 3012 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 } ≠ ∅)
218 rabn0 4345 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 } ≠ ∅ ↔ ∃𝑧𝐼 (𝑙𝑧) ≠ 0 )
219217, 218sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼 (𝑙𝑧) ≠ 0 )
220201, 219reximddv 3168 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
221 rexcom 3273 . . . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
224 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ( = 𝑚 → (♯‘( supp 0 )) = (♯‘(𝑚 supp 0 )))
225224eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝑗 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
226 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝐻𝑚𝐻))
227225, 226imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( = 𝑚 → ((𝑗 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻)))
228227rspccva 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
229228adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
230229imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
231230adantllr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
232231adantlrr 719 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
233232adantrr 715 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑚𝐻)
234 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑧𝐼)
23592ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 ∈ (𝐵m 𝐼))
23691, 235, 234mapfvd 8817 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑙𝑧) ∈ 𝐵)
23768ad5antr 732 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
238 equequ2 2029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑧 → (𝑥 = 𝑎𝑥 = 𝑧))
239238ifbid 4509 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
240239mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
241240eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑧 → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
242 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑧 → (𝑙𝑥) = (𝑙𝑧))
243242eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → (𝑏 = (𝑙𝑥) ↔ 𝑏 = (𝑙𝑧)))
244243biimparc 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 = (𝑙𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙𝑥))
245244ifeq1da 4517 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = (𝑙𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
246245mpteq2dv 5207 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = (𝑙𝑧) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))
247246eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (𝑙𝑧) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻))
248241, 247rspc2va 3591 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧𝐼 ∧ (𝑙𝑧) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
249234, 236, 237, 248syl21anc 836 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
250 fsuppind.2 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑥𝐻𝑦𝐻)) → (𝑥f + 𝑦) ∈ 𝐻)
251250ralrimivva 3197 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
252251ad5antr 732 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
253 ovrspc2v 7383 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑚𝐻 ∧ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
254233, 249, 252, 253syl21anc 836 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
255223, 254eqeltrd 2838 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙𝐻)
256255ex 413 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) → 𝑙𝐻))
257256rexlimdvva 3205 . . . . . . . . . . . . . . . . . 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 421 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → (𝑙 ∈ (𝐵m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻)))
260259ralrimiv 3142 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → ∀𝑙 ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻))
261 fvoveq1 7380 . . . . . . . . . . . . . . . . . 18 (𝑙 = → (♯‘(𝑙 supp 0 )) = (♯‘( supp 0 )))
262261eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑙 = → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
263 eleq1w 2820 . . . . . . . . . . . . . . . . 17 (𝑙 = → (𝑙𝐻𝐻))
264262, 263imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑙 = → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
265264cbvralvw 3225 . . . . . . . . . . . . . . 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 12173 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
268267ralrimiva 3143 . . . . . . . . . . . 12 (𝜑 → ∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
269 ralcom 3272 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
270268, 269sylib 217 . . . . . . . . . . 11 (𝜑 → ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
271 biidd 261 . . . . . . . . . . . . . 14 (𝑛 = (♯‘( supp 0 )) → (𝐻𝐻))
272271ceqsralv 3483 . . . . . . . . . . . . 13 ((♯‘( supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ 𝐻))
273272biimpcd 248 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ((♯‘( supp 0 )) ∈ ℕ → 𝐻))
274273ralimi 3086 . . . . . . . . . . 11 (∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
275270, 274syl 17 . . . . . . . . . 10 (𝜑 → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
276 fvoveq1 7380 . . . . . . . . . . . . 13 ( = 𝑋 → (♯‘( supp 0 )) = (♯‘(𝑋 supp 0 )))
277276eleq1d 2822 . . . . . . . . . . . 12 ( = 𝑋 → ((♯‘( supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
278 eleq1 2825 . . . . . . . . . . . 12 ( = 𝑋 → (𝐻𝑋𝐻))
279277, 278imbi12d 344 . . . . . . . . . . 11 ( = 𝑋 → (((♯‘( supp 0 )) ∈ ℕ → 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
280279rspcv 3577 . . . . . . . . . 10 (𝑋 ∈ (𝐵m 𝐼) → (∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
281275, 280syl5com 31 . . . . . . . . 9 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
282281com23 86 . . . . . . . 8 (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻)))
283282imp 407 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻))
2846, 283sylbird 259 . . . . . 6 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋:𝐼𝐵𝑋𝐻))
285284imp 407 . . . . 5 (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧ 𝑋:𝐼𝐵) → 𝑋𝐻)
286285an32s 650 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
287286adantlr 713 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
288 ovex 7390 . . . . 5 (𝑋 supp 0 ) ∈ V
289 hasheq0 14263 . . . . 5 ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
290288, 289ax-mp 5 . . . 4 ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
291 ffn 6668 . . . . . . . 8 (𝑋:𝐼𝐵𝑋 Fn 𝐼)
292291ad2antlr 725 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
2934ad2antrr 724 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼𝑉)
29428a1i 11 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
295 fnsuppeq0 8123 . . . . . . 7 ((𝑋 Fn 𝐼𝐼𝑉0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296292, 293, 294, 295syl3anc 1371 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
297296biimpa 477 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
298 fsuppind.0 . . . . . 6 (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
299298ad3antrrr 728 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
300297, 299eqeltrd 2838 . . . 4 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋𝐻)
301290, 300sylan2b 594 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋𝐻)
302 simpr 485 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
303302fsuppimpd 9312 . . . . 5 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
304 hashcl 14256 . . . . 5 ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
305303, 304syl 17 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
306 elnn0 12415 . . . 4 ((♯‘(𝑋 supp 0 )) ∈ ℕ0 ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
307305, 306sylib 217 . . 3 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
308287, 301, 307mpjaodan 957 . 2 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋𝐻)
309308anasss 467 1 ((𝜑 ∧ (𝑋:𝐼𝐵𝑋 finSupp 0 )) → 𝑋𝐻)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  ∃!weu 2566  wne 2943  wral 3064  wrex 3073  ∃!wreu 3351  {crab 3407  Vcvv 3445  cdif 3907  c0 4282  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631   Fn wfn 6491  wf 6492  cfv 6496  crio 7312  (class class class)co 7357  f cof 7615   supp csupp 8092  m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  0cc0 11051  1c1 11052   + caddc 11054  cn 12153  0cn0 12413  chash 14230  Basecbs 17083  +gcplusg 17133  0gc0g 17321  Grpcgrp 18748
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-hash 14231  df-0g 17323  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-grp 18751
This theorem is referenced by:  fsuppssind  40754
  Copyright terms: Public domain W3C validator