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 42600
Description: Induction on functions 𝐹:𝐴𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 21776 and frlmplusgval 21784). This theorem is structurally general for polynomial proof usage (see mplelbas 22011 and mpladd 22029). 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 6920 . . . . . . . . . 10 𝐵 ∈ V
32a1i 11 . . . . . . . . 9 (𝜑𝐵 ∈ V)
4 fsuppind.v . . . . . . . . 9 (𝜑𝐼𝑉)
53, 4elmapd 8880 . . . . . . . 8 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
65adantr 480 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) ↔ 𝑋:𝐼𝐵))
7 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑖 = 1 → (𝑖 = (♯‘( supp 0 )) ↔ 1 = (♯‘( supp 0 ))))
87imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = 1 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (1 = (♯‘( supp 0 )) → 𝐻)))
98ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = 1 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻)))
10 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘( supp 0 ))))
1110imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = 𝑗 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘( supp 0 )) → 𝐻)))
1211ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)))
13 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘( supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
1413imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
1514ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = (𝑗 + 1) → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
16 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑛 → (𝑖 = (♯‘( supp 0 )) ↔ 𝑛 = (♯‘( supp 0 ))))
1716imbi1d 341 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → ((𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑛 = (♯‘( supp 0 )) → 𝐻)))
1817ralbidv 3178 . . . . . . . . . . . . . 14 (𝑖 = 𝑛 → (∀ ∈ (𝐵m 𝐼)(𝑖 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻)))
19 eqcom 2744 . . . . . . . . . . . . . . . . 17 (1 = (♯‘( supp 0 )) ↔ (♯‘( supp 0 )) = 1)
20 ovex 7464 . . . . . . . . . . . . . . . . . 18 ( supp 0 ) ∈ V
21 euhash1 14459 . . . . . . . . . . . . . . . . . 18 (( supp 0 ) ∈ V → ((♯‘( supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ ( supp 0 )))
2220, 21ax-mp 5 . . . . . . . . . . . . . . . . 17 ((♯‘( supp 0 )) = 1 ↔ ∃!𝑐 𝑐 ∈ ( supp 0 ))
2319, 22bitri 275 . . . . . . . . . . . . . . . 16 (1 = (♯‘( supp 0 )) ↔ ∃!𝑐 𝑐 ∈ ( supp 0 ))
24 elmapfn 8905 . . . . . . . . . . . . . . . . . . . . 21 ( ∈ (𝐵m 𝐼) → Fn 𝐼)
2524adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → Fn 𝐼)
264adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 𝐼𝑉)
27 fsuppind.z . . . . . . . . . . . . . . . . . . . . . 22 0 = (0g𝐺)
2827fvexi 6920 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
2928a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∈ (𝐵m 𝐼)) → 0 ∈ V)
30 elsuppfn 8195 . . . . . . . . . . . . . . . . . . . 20 (( Fn 𝐼𝐼𝑉0 ∈ V) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3125, 26, 29, 30syl3anc 1373 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∈ (𝐵m 𝐼)) → (𝑐 ∈ ( supp 0 ) ↔ (𝑐𝐼 ∧ (𝑐) ≠ 0 )))
3231eubidv 2586 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 )))
33 df-reu 3381 . . . . . . . . . . . . . . . . . 18 (∃!𝑐𝐼 (𝑐) ≠ 0 ↔ ∃!𝑐(𝑐𝐼 ∧ (𝑐) ≠ 0 ))
3432, 33bitr4di 289 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) ↔ ∃!𝑐𝐼 (𝑐) ≠ 0 ))
3524ad2antlr 727 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → Fn 𝐼)
36 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥) ∈ V
3736, 28ifex 4576 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) ∈ V
38 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
3937, 38fnmpti 6711 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼
4039a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) Fn 𝐼)
41 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
42 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑣 → (𝑥) = (𝑣))
4341, 42ifbieq1d 4550 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑣 → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4443, 38, 37fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
4544adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣) = if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ))
46 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → (𝑣) = (𝑣))
47 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
48 simplr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ∃!𝑐𝐼 (𝑐) ≠ 0 )
49 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑣 → (𝑐) = (𝑣))
5049neeq1d 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑣 → ((𝑐) ≠ 0 ↔ (𝑣) ≠ 0 ))
5150riota2 7413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑣𝐼 ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
5247, 48, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑣) ≠ 0 ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣))
53 necom 2994 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( 0 ≠ (𝑣) ↔ (𝑣) ≠ 0 )
54 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) ↔ (𝑐𝐼 (𝑐) ≠ 0 ) = 𝑣)
5552, 53, 543bitr4g 314 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) ↔ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5655biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → ( 0 ≠ (𝑣) → 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )))
5756necon1bd 2958 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ) → 0 = (𝑣)))
5857imp 406 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) ∧ ¬ 𝑣 = (𝑐𝐼 (𝑐) ≠ 0 )) → 0 = (𝑣))
5946, 58ifeqda 4562 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑣), 0 ) = (𝑣))
6045, 59eqtr2d 2778 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) ∧ 𝑣𝐼) → (𝑣) = ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))‘𝑣))
6135, 40, 60eqfnfvd 7054 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
62 riotacl 7405 . . . . . . . . . . . . . . . . . . . . 21 (∃!𝑐𝐼 (𝑐) ≠ 0 → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
6362adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼)
64 elmapi 8889 . . . . . . . . . . . . . . . . . . . . . 22 ( ∈ (𝐵m 𝐼) → :𝐼𝐵)
6564ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → :𝐼𝐵)
6665, 63ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵)
67 fsuppind.1 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎𝐼𝑏𝐵)) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6867ralrimivva 3202 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
6968ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
70 eqeq2 2749 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥 = 𝑎𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )))
7170ifbid 4549 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ))
7271mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )))
7372eleq1d 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑐𝐼 (𝑐) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻))
74 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥) = (‘(𝑐𝐼 (𝑐) ≠ 0 )))
7574eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ) → (𝑏 = (𝑥) ↔ 𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 ))))
7675biimparc 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∧ 𝑥 = (𝑐𝐼 (𝑐) ≠ 0 )) → 𝑏 = (𝑥))
7776ifeq1da 4557 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 ))
7877mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )))
7978eleq1d 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = (‘(𝑐𝐼 (𝑐) ≠ 0 )) → ((𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻))
8073, 79rspc2va 3634 . . . . . . . . . . . . . . . . . . . 20 ((((𝑐𝐼 (𝑐) ≠ 0 ) ∈ 𝐼 ∧ (‘(𝑐𝐼 (𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8163, 66, 69, 80syl21anc 838 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = (𝑐𝐼 (𝑐) ≠ 0 ), (𝑥), 0 )) ∈ 𝐻)
8261, 81eqeltrd 2841 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∈ (𝐵m 𝐼)) ∧ ∃!𝑐𝐼 (𝑐) ≠ 0 ) → 𝐻)
8382ex 412 . . . . . . . . . . . . . . . . 17 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐𝐼 (𝑐) ≠ 0𝐻))
8434, 83sylbid 240 . . . . . . . . . . . . . . . 16 ((𝜑 ∈ (𝐵m 𝐼)) → (∃!𝑐 𝑐 ∈ ( supp 0 ) → 𝐻))
8523, 84biimtrid 242 . . . . . . . . . . . . . . 15 ((𝜑 ∈ (𝐵m 𝐼)) → (1 = (♯‘( supp 0 )) → 𝐻))
8685ralrimiva 3146 . . . . . . . . . . . . . 14 (𝜑 → ∀ ∈ (𝐵m 𝐼)(1 = (♯‘( supp 0 )) → 𝐻))
87 fvoveq1 7454 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (♯‘(𝑚 supp 0 )) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
8887eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))))
89 oveq1 7438 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
9089eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → (𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ↔ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
9188, 90anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))))
92 fsuppind.g . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺 ∈ Grp)
931, 27grpidcl 18983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ Grp → 0𝐵)
9492, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑0𝐵)
9594ad5antr 734 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 0𝐵)
96 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐵m 𝐼) = (𝐵m 𝐼)
97 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵m 𝐼))
9897ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑙 ∈ (𝐵m 𝐼))
99 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → 𝑥𝐼)
10096, 98, 99mapfvd 8919 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → (𝑙𝑥) ∈ 𝐵)
10195, 100ifcld 4572 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑥𝐼) → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ 𝐵)
102101fmpttd 7135 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵)
1032a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐵 ∈ V)
1044ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
105103, 104elmapd 8880 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼) ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))):𝐼𝐵))
106102, 105mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
107106adantrl 716 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∈ (𝐵m 𝐼))
108 ovexd 7466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈ V)
109 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧𝐼)
110 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑙𝑧) ≠ 0 )
111 elmapfn 8905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑙 ∈ (𝐵m 𝐼) → 𝑙 Fn 𝐼)
112111ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
113112adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 Fn 𝐼)
1144ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝐼𝑉)
11528a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 0 ∈ V)
116 elsuppfn 8195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
117113, 114, 115, 116syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )))
118109, 110, 117mpbir2and 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 ))
119 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ)
120119nnnn0d 12587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 ∈ ℕ0)
121 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
122121eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘(𝑙 supp 0 )) = (𝑗 + 1))
123 hashdifsnp1 14545 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) → ((♯‘(𝑙 supp 0 )) = (𝑗 + 1) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗))
124123imp 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) ∧ (♯‘(𝑙 supp 0 )) = (𝑗 + 1)) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
125108, 118, 120, 122, 124syl31anc 1375 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = 𝑗)
126 eldifsn 4786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧))
127 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑙𝑥) ∈ V
12828, 127ifex 4576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 if(𝑥 = 𝑧, 0 , (𝑙𝑥)) ∈ V
129 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))
130128, 129fnmpti 6711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼
131130a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼)
1324ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝐼𝑉)
13328a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 0 ∈ V)
134 elsuppfn 8195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
135131, 132, 133, 134syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ) ↔ (𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 )))
136 iftrue 4531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 )
137 olc 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑣 = 𝑧 → ((𝑙𝑣) = 0𝑣 = 𝑧))
138136, 1372thd 265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
139 iffalse 4534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = (𝑙𝑣))
140139eqeq1d 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ (𝑙𝑣) = 0 ))
141 biorf 937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 )))
142 orcom 871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑙𝑣) = 0𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙𝑣) = 0 ))
143141, 142bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 𝑣 = 𝑧 → ((𝑙𝑣) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
144140, 143bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
145138, 144pm2.61i 182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧))
146145a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) = 0 ↔ ((𝑙𝑣) = 0𝑣 = 𝑧)))
147146necon3abid 2977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧)))
148 neanior 3035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑙𝑣) ≠ 0𝑣𝑧) ↔ ¬ ((𝑙𝑣) = 0𝑣 = 𝑧))
149147, 148bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ↔ ((𝑙𝑣) ≠ 0𝑣𝑧)))
150149anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧))))
151 anass 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧) ↔ (𝑣𝐼 ∧ ((𝑙𝑣) ≠ 0𝑣𝑧)))
152150, 151bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
153 equequ1 2024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑥 = 𝑧𝑣 = 𝑧))
154 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = 𝑣 → (𝑙𝑥) = (𝑙𝑣))
155153, 154ifbieq2d 4552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
156155, 129, 128fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
157156adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙𝑣)))
158157neeq1d 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 ))
159158pm5.32da 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙𝑣)) ≠ 0 )))
160112adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 Fn 𝐼)
161 elsuppfn 8195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
162160, 132, 133, 161syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 )))
163162anbi1d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧) ↔ ((𝑣𝐼 ∧ (𝑙𝑣) ≠ 0 ) ∧ 𝑣𝑧)))
164152, 159, 1633bitr4d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣𝐼 ∧ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧)))
165135, 164bitr2d 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣𝑧) ↔ 𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
166126, 165bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
167166eqrdv 2735 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 ))
168167fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
169168adantrl 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (♯‘((𝑙 supp 0 ) ∖ {𝑧})) = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
170125, 169eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )))
171127, 28ifex 4576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑥 = 𝑧, (𝑙𝑥), 0 ) ∈ V
172 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
173171, 172fnmpti 6711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼
174173a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) Fn 𝐼)
175 inidm 4227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐼𝐼) = 𝐼
176131, 174, 132, 132, 175offn 7710 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) Fn 𝐼)
177153, 154ifbieq1d 4550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
178177, 172, 171fvmpt3i 7021 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣𝐼 → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
179178adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), 0 ))
180131, 174, 132, 132, 175, 157, 179ofval 7708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )))
18192ad4antr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝐺 ∈ Grp)
182 simplrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙𝑧) ≠ 0𝑣𝐼)) → 𝑙 ∈ (𝐵m 𝐼))
183182anassrs 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑙 ∈ (𝐵m 𝐼))
184 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → 𝑣𝐼)
18596, 183, 184mapfvd 8919 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) ∈ 𝐵)
186 fsuppind.p . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 + = (+g𝐺)
1871, 186, 27grplid 18985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ( 0 + (𝑙𝑣)) = (𝑙𝑣))
1881, 186, 27grprid 18986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → ((𝑙𝑣) + 0 ) = (𝑙𝑣))
189187, 188ifeq12d 4547 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐺 ∈ Grp ∧ (𝑙𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
190181, 185, 189syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)))
191 ovif12 7533 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙𝑣)), ((𝑙𝑣) + 0 ))
192 ifid 4566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣)) = (𝑙𝑣)
193192eqcomi 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑙𝑣) = if(𝑣 = 𝑧, (𝑙𝑣), (𝑙𝑣))
194190, 191, 1933eqtr4g 2802 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙𝑣)) + if(𝑣 = 𝑧, (𝑙𝑣), 0 )) = (𝑙𝑣))
195180, 194eqtr2d 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) ∧ 𝑣𝐼) → (𝑙𝑣) = (((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))‘𝑣))
196160, 176, 195eqfnfvd 7054 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙𝑧) ≠ 0 ) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
197196adantrl 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
198170, 197jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
199198adantllr 719 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙𝑥))) ∘f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
20091, 107, 199rspcedvdw 3625 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧𝐼 ∧ (𝑙𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
201111ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼)
2024ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼𝑉)
20328a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈ V)
204 suppvalfn 8193 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑙 Fn 𝐼𝐼𝑉0 ∈ V) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
205201, 202, 203, 204syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 })
206 simprr 773 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 )))
207 peano2nn 12278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ℕ → (𝑗 + 1) ∈ ℕ)
208207ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈ ℕ)
209208nnne0d 12316 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0)
210206, 209eqnetrrd 3009 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (♯‘(𝑙 supp 0 )) ≠ 0)
211 ovex 7464 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑙 supp 0 ) ∈ V
212 hasheq0 14402 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) = 0 ↔ (𝑙 supp 0 ) = ∅))
213212necon3bid 2985 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙 supp 0 ) ∈ V → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
214211, 213mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ((♯‘(𝑙 supp 0 )) ≠ 0 ↔ (𝑙 supp 0 ) ≠ ∅))
215210, 214mpbid 232 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) ≠ ∅)
216205, 215eqnetrrd 3009 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 } ≠ ∅)
217 rabn0 4389 . . . . . . . . . . . . . . . . . . . . 21 ({𝑧𝐼 ∣ (𝑙𝑧) ≠ 0 } ≠ ∅ ↔ ∃𝑧𝐼 (𝑙𝑧) ≠ 0 )
218216, 217sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼 (𝑙𝑧) ≠ 0 )
219200, 218reximddv 3171 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧𝐼𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
220 rexcom 3290 . . . . . . . . . . . . . . . . . . 19 (∃𝑧𝐼𝑚 ∈ (𝐵m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) ↔ ∃𝑚 ∈ (𝐵m 𝐼)∃𝑧𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
221219, 220sylib 218 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑚 ∈ (𝐵m 𝐼)∃𝑧𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))))
222 simprr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))
223 fvoveq1 7454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ( = 𝑚 → (♯‘( supp 0 )) = (♯‘(𝑚 supp 0 )))
224223eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝑗 = (♯‘( supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 ))))
225 eleq1w 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ( = 𝑚 → (𝐻𝑚𝐻))
226224, 225imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ( = 𝑚 → ((𝑗 = (♯‘( supp 0 )) → 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻)))
227226rspccva 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
228227adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚𝐻))
229228imp 406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
230229adantllr 719 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
231230adantlrr 721 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚𝐻)
232231adantrr 717 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑚𝐻)
233 simplrr 778 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑧𝐼)
23497ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙 ∈ (𝐵m 𝐼))
23596, 234, 233mapfvd 8919 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑙𝑧) ∈ 𝐵)
23668ad5antr 734 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)
237 equequ2 2025 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑧 → (𝑥 = 𝑎𝑥 = 𝑧))
238237ifbid 4549 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 ))
239238mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )))
240239eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = 𝑧 → ((𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻))
241 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑧 → (𝑙𝑥) = (𝑙𝑧))
242241eqeq2d 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = 𝑧 → (𝑏 = (𝑙𝑥) ↔ 𝑏 = (𝑙𝑧)))
243242biimparc 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑏 = (𝑙𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙𝑥))
244243ifeq1da 4557 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 = (𝑙𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙𝑥), 0 ))
245244mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 = (𝑙𝑧) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))
246245eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 = (𝑙𝑧) → ((𝑥𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻))
247240, 246rspc2va 3634 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑧𝐼 ∧ (𝑙𝑧) ∈ 𝐵) ∧ ∀𝑎𝐼𝑏𝐵 (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
248233, 235, 236, 247syl21anc 838 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻)
249 fsuppind.2 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑥𝐻𝑦𝐻)) → (𝑥f + 𝑦) ∈ 𝐻)
250249ralrimivva 3202 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
251250ad5antr 734 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻)
252 ovrspc2v 7457 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑚𝐻 ∧ (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥𝐻𝑦𝐻 (𝑥f + 𝑦) ∈ 𝐻) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
253232, 248, 251, 252syl21anc 838 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))) ∈ 𝐻)
254222, 253eqeltrd 2841 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 ))))) → 𝑙𝐻)
255254ex 412 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵m 𝐼) ∧ 𝑧𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) → 𝑙𝐻))
256255rexlimdvva 3213 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (∃𝑚 ∈ (𝐵m 𝐼)∃𝑧𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚f + (𝑥𝐼 ↦ if(𝑥 = 𝑧, (𝑙𝑥), 0 )))) → 𝑙𝐻))
257221, 256mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) ∧ (𝑙 ∈ (𝐵m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙𝐻)
258257exp32 420 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → (𝑙 ∈ (𝐵m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻)))
259258ralrimiv 3145 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → ∀𝑙 ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻))
260 fvoveq1 7454 . . . . . . . . . . . . . . . . . 18 (𝑙 = → (♯‘(𝑙 supp 0 )) = (♯‘( supp 0 )))
261260eqeq2d 2748 . . . . . . . . . . . . . . . . 17 (𝑙 = → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘( supp 0 ))))
262 eleq1w 2824 . . . . . . . . . . . . . . . . 17 (𝑙 = → (𝑙𝐻𝐻))
263261, 262imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑙 = → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻) ↔ ((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻)))
264263cbvralvw 3237 . . . . . . . . . . . . . . 15 (∀𝑙 ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙𝐻) ↔ ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻))
265259, 264sylib 218 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ℕ) ∧ ∀ ∈ (𝐵m 𝐼)(𝑗 = (♯‘( supp 0 )) → 𝐻)) → ∀ ∈ (𝐵m 𝐼)((𝑗 + 1) = (♯‘( supp 0 )) → 𝐻))
2669, 12, 15, 18, 86, 265nnindd 12286 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
267266ralrimiva 3146 . . . . . . . . . . . 12 (𝜑 → ∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻))
268 ralcom 3289 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ ∀ ∈ (𝐵m 𝐼)(𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
269267, 268sylib 218 . . . . . . . . . . 11 (𝜑 → ∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻))
270 biidd 262 . . . . . . . . . . . . . 14 (𝑛 = (♯‘( supp 0 )) → (𝐻𝐻))
271270ceqsralv 3522 . . . . . . . . . . . . 13 ((♯‘( supp 0 )) ∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) ↔ 𝐻))
272271biimpcd 249 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ((♯‘( supp 0 )) ∈ ℕ → 𝐻))
273272ralimi 3083 . . . . . . . . . . 11 (∀ ∈ (𝐵m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘( supp 0 )) → 𝐻) → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
274269, 273syl 17 . . . . . . . . . 10 (𝜑 → ∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻))
275 fvoveq1 7454 . . . . . . . . . . . . 13 ( = 𝑋 → (♯‘( supp 0 )) = (♯‘(𝑋 supp 0 )))
276275eleq1d 2826 . . . . . . . . . . . 12 ( = 𝑋 → ((♯‘( supp 0 )) ∈ ℕ ↔ (♯‘(𝑋 supp 0 )) ∈ ℕ))
277 eleq1 2829 . . . . . . . . . . . 12 ( = 𝑋 → (𝐻𝑋𝐻))
278276, 277imbi12d 344 . . . . . . . . . . 11 ( = 𝑋 → (((♯‘( supp 0 )) ∈ ℕ → 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
279278rspcv 3618 . . . . . . . . . 10 (𝑋 ∈ (𝐵m 𝐼) → (∀ ∈ (𝐵m 𝐼)((♯‘( supp 0 )) ∈ ℕ → 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
280274, 279syl5com 31 . . . . . . . . 9 (𝜑 → (𝑋 ∈ (𝐵m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ → 𝑋𝐻)))
281280com23 86 . . . . . . . 8 (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻)))
282281imp 406 . . . . . . 7 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋 ∈ (𝐵m 𝐼) → 𝑋𝐻))
2836, 282sylbird 260 . . . . . 6 ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → (𝑋:𝐼𝐵𝑋𝐻))
284283imp 406 . . . . 5 (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧ 𝑋:𝐼𝐵) → 𝑋𝐻)
285284an32s 652 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
286285adantlr 715 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) → 𝑋𝐻)
287 ovex 7464 . . . . 5 (𝑋 supp 0 ) ∈ V
288 hasheq0 14402 . . . . 5 ((𝑋 supp 0 ) ∈ V → ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅))
289287, 288ax-mp 5 . . . 4 ((♯‘(𝑋 supp 0 )) = 0 ↔ (𝑋 supp 0 ) = ∅)
290 ffn 6736 . . . . . . . 8 (𝑋:𝐼𝐵𝑋 Fn 𝐼)
291290ad2antlr 727 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼)
2924ad2antrr 726 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼𝑉)
29328a1i 11 . . . . . . 7 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈ V)
294 fnsuppeq0 8217 . . . . . . 7 ((𝑋 Fn 𝐼𝐼𝑉0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
295291, 292, 293, 294syl3anc 1373 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 })))
296295biimpa 476 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 }))
297 fsuppind.0 . . . . . 6 (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)
298297ad3antrrr 730 . . . . 5 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻)
299296, 298eqeltrd 2841 . . . 4 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋𝐻)
300289, 299sylan2b 594 . . 3 ((((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) ∧ (♯‘(𝑋 supp 0 )) = 0) → 𝑋𝐻)
301 simpr 484 . . . . . 6 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 )
302301fsuppimpd 9409 . . . . 5 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈ Fin)
303 hashcl 14395 . . . . 5 ((𝑋 supp 0 ) ∈ Fin → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
304302, 303syl 17 . . . 4 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → (♯‘(𝑋 supp 0 )) ∈ ℕ0)
305 elnn0 12528 . . . 4 ((♯‘(𝑋 supp 0 )) ∈ ℕ0 ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
306304, 305sylib 218 . . 3 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0))
307286, 300, 306mpjaodan 961 . 2 (((𝜑𝑋:𝐼𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋𝐻)
308307anasss 466 1 ((𝜑 ∧ (𝑋:𝐼𝐵𝑋 finSupp 0 )) → 𝑋𝐻)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  ∃!weu 2568  wne 2940  wral 3061  wrex 3070  ∃!wreu 3378  {crab 3436  Vcvv 3480  cdif 3948  c0 4333  ifcif 4525  {csn 4626   class class class wbr 5143  cmpt 5225   × cxp 5683   Fn wfn 6556  wf 6557  cfv 6561  crio 7387  (class class class)co 7431  f cof 7695   supp csupp 8185  m cmap 8866  Fincfn 8985   finSupp cfsupp 9401  0cc0 11155  1c1 11156   + caddc 11158  cn 12266  0cn0 12526  chash 14369  Basecbs 17247  +gcplusg 17297  0gc0g 17484  Grpcgrp 18951
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-hash 14370  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954
This theorem is referenced by:  fsuppssind  42603
  Copyright terms: Public domain W3C validator