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 41464
Description: Induction on functions 𝐹:𝐴𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21530 and frlmplusgval 21538). This theorem is structurally general for polynomial proof usage (see mplelbas 21769 and mpladd 21787). 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 6904 . . . . . . . . . 10 𝐵 ∈ V
32a1i 11 . . . . . . . . 9 (𝜑𝐵 ∈ V)
4 fsuppind.v . . . . . . . . 9 (𝜑𝐼𝑉)
53, 4elmapd 8836 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
65adantr 479 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
7 eqeq1 2734 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝑖 = (♯‘( supp 0 )) ↔ 1 = (♯‘( supp 0 ))))
87imbi1d 340 . . . . . . . . . . . . . . 15 (𝑖 = 1 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (1 = (♯‘( supp 0 )) → 𝐻)))
98ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = 1 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻)))
10 eqeq1 2734 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘( supp 0 ))))
1110imbi1d 340 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘( supp 0 )) → 𝐻)))
1211ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)))
13 eqeq1 2734 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘( supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
1413imbi1d 340 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
1514ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 + 1) → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
16 eqeq1 2734 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑛 = (♯‘( supp 0 ))))
1716imbi1d 340 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑛 = (♯‘( supp 0 )) → 𝐻)))
1817ralbidv 3175 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻)))
19 eqcom 2737 . . . . . . . . . . . . . . . . 17 (1 = (♯‘( supp 0 )) ↔ (♯‘( supp 0 )) = 1)
20 ovex 7444 . . . . . . . . . . . . . . . . . 18 ( supp 0 ) ∈ V
21 euhash1 14384 . . . . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (𝐵m 𝐼) → Fn 𝐼)
2524adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → Fn 𝐼)
264adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 𝐼𝑉)
27 fsuppind.z . . . . . . . . . . . . . . . . . . . . . 22 0 = (0g𝐺)
2827fvexi 6904 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
2928a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 0 ∈ V)
30 elsuppfn 8158 . . . . . . . . . . . . . . . . . . . 20 (( Fn 𝐼𝐼𝑉0 ∈ V) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3125, 26, 29, 30syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∈ (𝐵m 𝐼)) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3231eubidv 2578 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 )))
33 df-reu 3375 . . . . . . . . . . . . . . . . . 18 (∃!𝑐𝐼 (𝑐) ≠ 0 ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 ))
3432, 33bitr4di 288 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐𝐼 (𝑐) ≠ 0 ))
3524ad2antlr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → Fn 𝐼)
36 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥) ∈ V
3736, 28ifex 4577 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) ∈ V
38 eqid 2730 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
3937, 38fnmpti 6692 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼
4039a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼)
41 eqeq1 2734 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
42 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥) = (𝑣))
4341, 42ifbieq1d 4551 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑣 → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4443, 38, 37fvmpt3i 7002 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4544adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
46 eqidd 2731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → (𝑣) = (𝑣))
47 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
48 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ∃!𝑐𝐼 (𝑐) ≠ 0 )
49 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑣 → (𝑐) = (𝑣))
5049neeq1d 2998 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑣 → ((𝑐) ≠ 0 ↔ (𝑣) ≠ 0 ))
5150riota2 7393 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣𝐼 ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
5247, 48, 51syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
53 necom 2992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( 0 ≠ (𝑣) ↔ (𝑣) ≠ 0 )
54 eqcom 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣)
5552, 53, 543bitr4g 313 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5655biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) → 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5756necon1bd 2956 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) → 0 = (𝑣)))
5857imp 405 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ ¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → 0 = (𝑣))
5946, 58ifeqda 4563 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ) = (𝑣))
6045, 59eqtr2d 2771 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (𝑣) = ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣))
6135, 40, 60eqfnfvd 7034 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
62 riotacl 7385 . . . . . . . . . . . . . . . . . . . . 21 (∃!𝑐𝐼 (𝑐) ≠ 0 → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
6362adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
64 elmapi 8845 . . . . . . . . . . . . . . . . . . . . . 22 ( ∈ (𝐵m 𝐼) → :𝐼𝐵)
6564ad2antlr 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → :𝐼𝐵)
6665, 63ffvelcdmd 7086 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵)
67 fsuppind.1 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎𝐼𝑏𝐵)) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6867ralrimivva 3198 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6968ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70 eqeq2 2742 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥 = 𝑎𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )))
7170ifbid 4550 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ))
7271mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )))
7372eleq1d 2816 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥) = (‘(𝑐𝐼 (𝑐) ≠ 0 )))
7574eqeq2d 2741 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑏 = (𝑥) ↔ 𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 ))))
7675biimparc 478 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∧ 𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )) → 𝑏 = (𝑥))
7776ifeq1da 4558 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
7877mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
7978eleq1d 2816 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻))
8073, 79rspc2va 3622 . . . . . . . . . . . . . . . . . . . 20 ((((𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼 ∧ (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8163, 66, 69, 80syl21anc 834 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8261, 81eqeltrd 2831 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → 𝐻)
8382ex 411 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐𝐼 (𝑐) ≠ 0𝐻))
8434, 83sylbid 239 . . . . . . . . . . . . . . . 16 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) → 𝐻))
8523, 84biimtrid 241 . . . . . . . . . . . . . . 15 ((𝜑 ∈ (𝐵m 𝐼)) → (1 = (♯‘( supp 0 )) → 𝐻))
8685ralrimiva 3144 . . . . . . . . . . . . . 14 (𝜑 → ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻))
87 fsuppind.g . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺 ∈ Grp)
881, 27grpidcl 18886 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ Grp → 0𝐵)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑0𝐵)
9089ad5antr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 0𝐵)
91 eqid 2730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵m 𝐼) = (𝐵m 𝐼)
92 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵m 𝐼))
9392ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑙 ∈ (𝐵m 𝐼))
94 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑥𝐼)
9591, 93, 94mapfvd 8875 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → (𝑙𝑥) ∈ 𝐵)
9690, 95ifcld 4573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ 𝐵)
9796fmpttd 7115 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵)
982a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐵 ∈ V)
994ad4antr 728 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
10098, 99elmapd 8836 . . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
103 fvoveq1 7434 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
104103eqeq2d 2741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))))
105 oveq1 7418 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
106105eqeq2d 2741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ↔ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
107104, 106anbi12d 629 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))))
108107adantl 480 . . . . . . . . . . . . . . . . . . . . 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 7446 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
110 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧𝐼)
111 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙𝑧) ≠ 0 )
112 elmapfn 8861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (𝐵m 𝐼) → 𝑙 Fn 𝐼)
113112ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
114113adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
1154ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝐼𝑉)
11628a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 0 ∈ V)
117 elsuppfn 8158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
118114, 115, 116, 117syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
119110, 111, 118mpbir2and 709 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
120 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
121120nnnn0d 12536 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ0)
122 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
123122eqcomd 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
124 hashdifsnp1 14461 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) → ((♯‘(𝑙 supp 0 )) = (𝑗 + 1) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗))
125124imp 405 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) ∧ (♯‘(𝑙 supp 0 )) = (𝑗 + 1)) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126109, 119, 121, 123, 125syl31anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
127 eldifsn 4789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧))
128 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙𝑥) ∈ V
12928, 128ifex 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ V
130 eqid 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))
131129, 130fnmpti 6692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼
132131a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼)
1334ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
13428a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 0 ∈ V)
135 elsuppfn 8158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
136132, 133, 134, 135syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
137 iftrue 4533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 )
138 olc 864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → ((𝑙𝑣) = 0𝑣 = 𝑧))
139137, 1382thd 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
140 iffalse 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = (𝑙𝑣))
141140eqeq1d 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ (𝑙𝑣) = 0 ))
142 biorf 933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 )))
143 orcom 866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧)))
149 neanior 3033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑙𝑣) ≠ 0𝑣𝑧) ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧))
150148, 149bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ((𝑙𝑣) ≠ 0𝑣𝑧)))
151150anbi2d 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧))))
152 anass 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧)))
153151, 152bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
154 equequ1 2026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑥 = 𝑧𝑣 = 𝑧))
155 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑙𝑥) = (𝑙𝑣))
156154, 155ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
157156, 130, 129fvmpt3i 7002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
158157adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
159158neeq1d 2998 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ))
160159pm5.32da 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 )))
161113adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 Fn 𝐼)
162 elsuppfn 8158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
163161, 133, 134, 162syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
164163anbi1d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))
169168fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
170169adantrl 712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
171126, 170eqtr3d 2772 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
172128, 28ifex 4577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑥 = 𝑧, (𝑙𝑥), 0 ) ∈ V
173 eqid 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
174172, 173fnmpti 6692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼
175174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼)
176 inidm 4217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐼𝐼) = 𝐼
177132, 175, 133, 133, 176offn 7685 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) Fn 𝐼)
178154, 155ifbieq1d 4551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
179178, 173, 172fvmpt3i 7002 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
180179adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
181132, 175, 133, 133, 176, 158, 180ofval 7683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )))
18287ad4antr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝐺 ∈ Grp)
183 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙𝑧) ≠ 0𝑣𝐼)) → 𝑙 ∈ (𝐵m 𝐼))
184183anassrs 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑙 ∈ (𝐵m 𝐼))
185 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
18691, 184, 185mapfvd 8875 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) ∈ 𝐵)
187 fsuppind.p . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 + = (+g𝐺)
1881, 187, 27grplid 18888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ( 0 + (𝑙𝑣)) = (𝑙𝑣))
1891, 187, 27grprid 18889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ((𝑙𝑣) + 0 ) = (𝑙𝑣))
190188, 189ifeq12d 4548 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
191182, 186, 190syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
192 ovif12 7510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 ))
193 ifid 4567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)) = (𝑙𝑣)
194193eqcomi 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣))
195191, 192, 1943eqtr4g 2795 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = (𝑙𝑣))
196181, 195eqtr2d 2771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) = (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣))
197161, 177, 196eqfnfvd 7034 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
198197adantrl 712 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
199171, 198jca 510 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
200199adantllr 715 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
201102, 108, 200rspcedvd 3613 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
202112ad2antrl 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
2034ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼𝑉)
20428a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
205 suppvalfn 8156 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
206202, 203, 204, 205syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
207 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
208 peano2nn 12228 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
209208ad3antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
210209nnne0d 12266 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
211207, 210eqnetrrd 3007 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
212 ovex 7444 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 supp 0 ) ∈ V
213 hasheq0 14327 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
214213necon3bid 2983 . . . . . . . . . . . . . . . . . . . . . . . 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 3007 . . . . . . . . . . . . . . . . . . . . 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 3169 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
221 rexcom 3285 . . . . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
224 fvoveq1 7434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ( = 𝑚 → (♯‘( supp 0 )) = (♯‘(𝑚 supp 0 )))
225224eqeq2d 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝑗 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
226 eleq1w 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝐻𝑚𝐻))
227225, 226imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( = 𝑚 → ((𝑗 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻)))
228227rspccva 3610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
229228adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
230229imp 405 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
231230adantllr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
232231adantlrr 717 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
233232adantrr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑚𝐻)
234 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑧𝐼)
23592ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 ∈ (𝐵m 𝐼))
23691, 235, 234mapfvd 8875 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑙𝑧) ∈ 𝐵)
23768ad5antr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
238 equequ2 2027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑧 → (𝑥 = 𝑎𝑥 = 𝑧))
239238ifbid 4550 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
240239mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
241240eleq1d 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑧 → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
242 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑧 → (𝑙𝑥) = (𝑙𝑧))
243242eqeq2d 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → (𝑏 = (𝑙𝑥) ↔ 𝑏 = (𝑙𝑧)))
244243biimparc 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 = (𝑙𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙𝑥))
245244ifeq1da 4558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = (𝑙𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
246245mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = (𝑙𝑧) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))
247246eleq1d 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (𝑙𝑧) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻))
248241, 247rspc2va 3622 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧𝐼 ∧ (𝑙𝑧) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
249234, 236, 237, 248syl21anc 834 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
250 fsuppind.2 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑥𝐻𝑦𝐻)) → (𝑥f + 𝑦) ∈ 𝐻)
251250ralrimivva 3198 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
252251ad5antr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
253 ovrspc2v 7437 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑚𝐻 ∧ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
254233, 249, 252, 253syl21anc 834 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
255223, 254eqeltrd 2831 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙𝐻)
256255ex 411 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) → 𝑙𝐻))
257256rexlimdvva 3209 . . . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → (𝑙 ∈ (𝐵m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻)))
260259ralrimiv 3143 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → ∀𝑙 ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻))
261 fvoveq1 7434 . . . . . . . . . . . . . . . . . 18 (𝑙 = → (♯‘(𝑙 supp 0 )) = (♯‘( supp 0 )))
262261eqeq2d 2741 . . . . . . . . . . . . . . . . 17 (𝑙 = → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
263 eleq1w 2814 . . . . . . . . . . . . . . . . 17 (𝑙 = → (𝑙𝐻𝐻))
264262, 263imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑙 = → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
265264cbvralvw 3232 . . . . . . . . . . . . . . 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 12236 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
268267ralrimiva 3144 . . . . . . . . . . . 12 (𝜑 → ∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
269 ralcom 3284 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
270268, 269sylib 217 . . . . . . . . . . 11 (𝜑 → ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
271 biidd 261 . . . . . . . . . . . . . 14 (𝑛 = (♯‘( supp 0 )) → (𝐻𝐻))
272271ceqsralv 3512 . . . . . . . . . . . . 13 ((♯‘( supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ 𝐻))
273272biimpcd 248 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ((♯‘( supp 0 )) ∈ ℕ → 𝐻))
274273ralimi 3081 . . . . . . . . . . 11 (∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
275270, 274syl 17 . . . . . . . . . 10 (𝜑 → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
276 fvoveq1 7434 . . . . . . . . . . . . 13 ( = 𝑋 → (♯‘( supp 0 )) = (♯‘(𝑋 supp 0 )))
277276eleq1d 2816 . . . . . . . . . . . 12 ( = 𝑋 → ((♯‘( supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
278 eleq1 2819 . . . . . . . . . . . 12 ( = 𝑋 → (𝐻𝑋𝐻))
279277, 278imbi12d 343 . . . . . . . . . . 11 ( = 𝑋 → (((♯‘( supp 0 )) ∈ ℕ → 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
280279rspcv 3607 . . . . . . . . . 10 (𝑋 ∈ (𝐵m 𝐼) → (∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
281275, 280syl5com 31 . . . . . . . . 9 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
282281com23 86 . . . . . . . 8 (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻)))
283282imp 405 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻))
2846, 283sylbird 259 . . . . . 6 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋:𝐼𝐵𝑋𝐻))
285284imp 405 . . . . 5 (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧ 𝑋:𝐼𝐵) → 𝑋𝐻)
286285an32s 648 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
287286adantlr 711 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
288 ovex 7444 . . . . 5 (𝑋 supp 0 ) ∈ V
289 hasheq0 14327 . . . . 5 ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
290288, 289ax-mp 5 . . . 4 ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
291 ffn 6716 . . . . . . . 8 (𝑋:𝐼𝐵𝑋 Fn 𝐼)
292291ad2antlr 723 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
2934ad2antrr 722 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼𝑉)
29428a1i 11 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
295 fnsuppeq0 8179 . . . . . . 7 ((𝑋 Fn 𝐼𝐼𝑉0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296292, 293, 294, 295syl3anc 1369 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
297296biimpa 475 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
298 fsuppind.0 . . . . . 6 (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
299298ad3antrrr 726 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
300297, 299eqeltrd 2831 . . . 4 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋𝐻)
301290, 300sylan2b 592 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋𝐻)
302 simpr 483 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
303302fsuppimpd 9371 . . . . 5 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
304 hashcl 14320 . . . . 5 ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
305303, 304syl 17 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
306 elnn0 12478 . . . 4 ((♯‘(𝑋 supp 0 )) ∈ ℕ0 ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
307305, 306sylib 217 . . 3 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
308287, 301, 307mpjaodan 955 . 2 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋𝐻)
309308anasss 465 1 ((𝜑 ∧ (𝑋:𝐼𝐵𝑋 finSupp 0 )) → 𝑋𝐻)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 843  w3a 1085   = wceq 1539  wcel 2104  ∃!weu 2560  wne 2938  wral 3059  wrex 3068  ∃!wreu 3372  {crab 3430  Vcvv 3472  cdif 3944  c0 4321  ifcif 4527  {csn 4627   class class class wbr 5147  cmpt 5230   × cxp 5673   Fn wfn 6537  wf 6538  cfv 6542  crio 7366  (class class class)co 7411  f cof 7670   supp csupp 8148  m cmap 8822  Fincfn 8941   finSupp cfsupp 9363  0cc0 11112  1c1 11113   + caddc 11115  cn 12216  0cn0 12476  chash 14294  Basecbs 17148  +gcplusg 17201  0gc0g 17389  Grpcgrp 18855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  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 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13489  df-hash 14295  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858
This theorem is referenced by:  fsuppssind  41467
  Copyright terms: Public domain W3C validator