Step | Hyp | Ref
| Expression |
1 | | fsuppind.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐺) |
2 | 1 | fvexi 6665 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
3 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ V) |
4 | | fsuppind.v |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
5 | 3, 4 | elmapd 8423 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑m 𝐼) ↔ 𝑋:𝐼⟶𝐵)) |
6 | 5 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
(𝑋 ∈ (𝐵 ↑m 𝐼) ↔ 𝑋:𝐼⟶𝐵)) |
7 | | eqeq1 2763 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 1 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 1 =
(♯‘(ℎ supp 0
)))) |
8 | 7 | imbi1d 346 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 1 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
9 | 8 | ralbidv 3124 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
10 | | eqeq1 2763 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(ℎ supp 0 )))) |
11 | 10 | imbi1d 346 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
12 | 11 | ralbidv 3124 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
13 | | eqeq1 2763 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘(ℎ supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 )))) |
14 | 13 | imbi1d 346 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
15 | 14 | ralbidv 3124 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑗 + 1) → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
16 | | eqeq1 2763 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑛 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑛 = (♯‘(ℎ supp 0 )))) |
17 | 16 | imbi1d 346 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
18 | 17 | ralbidv 3124 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
19 | | eqcom 2766 |
. . . . . . . . . . . . . . . . 17
⊢ (1 =
(♯‘(ℎ supp 0 )) ↔
(♯‘(ℎ supp 0 )) =
1) |
20 | | ovex 7176 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ supp 0 ) ∈
V |
21 | | euhash1 13816 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ℎ supp 0 ) ∈ V →
((♯‘(ℎ supp
0 )) = 1
↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 ))) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(ℎ
supp 0 ))
= 1 ↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 )) |
23 | 19, 22 | bitri 278 |
. . . . . . . . . . . . . . . 16
⊢ (1 =
(♯‘(ℎ supp 0 )) ↔
∃!𝑐 𝑐 ∈ (ℎ supp 0 )) |
24 | | elmapfn 8440 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ Fn 𝐼) |
25 | 24 | adantl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → ℎ Fn 𝐼) |
26 | 4 | adantr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → 𝐼 ∈ 𝑉) |
27 | | fsuppind.z |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 =
(0g‘𝐺) |
28 | 27 | fvexi 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → 0 ∈ V) |
30 | | elsuppfn 7838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))) |
31 | 25, 26, 29, 30 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))) |
32 | 31 | eubidv 2607 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))) |
33 | | df-reu 3075 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃!𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )) |
34 | 32, 33 | bitr4di 293 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) |
35 | 24 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ Fn 𝐼) |
36 | | fvex 6664 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ‘𝑥) ∈ V |
37 | 36, 28 | ifex 4463 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) ∈
V |
38 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) |
39 | 37, 38 | fnmpti 6467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼 |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼) |
41 | | eqeq1 2763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑣 → (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
42 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑣 → (ℎ‘𝑥) = (ℎ‘𝑣)) |
43 | 41, 42 | ifbieq1d 4437 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑣 → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 )) |
44 | 43, 38, 37 | fvmpt3i 6757 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 )) |
45 | 44 | adantl 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 )) |
46 | | eqidd 2760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (ℎ‘𝑣) = (ℎ‘𝑣)) |
47 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼) |
48 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) |
49 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = 𝑣 → (ℎ‘𝑐) = (ℎ‘𝑣)) |
50 | 49 | neeq1d 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = 𝑣 → ((ℎ‘𝑐) ≠ 0 ↔ (ℎ‘𝑣) ≠ 0 )) |
51 | 50 | riota2 7126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ 𝐼 ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((ℎ‘𝑣) ≠ 0 ↔
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣)) |
52 | 47, 48, 51 | syl2anc 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((ℎ‘𝑣) ≠ 0 ↔
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣)) |
53 | | necom 3002 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ( 0 ≠ (ℎ‘𝑣) ↔ (ℎ‘𝑣) ≠ 0 ) |
54 | | eqcom 2766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣) |
55 | 52, 53, 54 | 3bitr4g 318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
56 | 55 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) → 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
57 | 56 | necon1bd 2967 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → 0 = (ℎ‘𝑣))) |
58 | 57 | imp 411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ ¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 0 = (ℎ‘𝑣)) |
59 | 46, 58 | ifeqda 4449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ) = (ℎ‘𝑣)) |
60 | 45, 59 | eqtr2d 2795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (ℎ‘𝑣) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣)) |
61 | 35, 40, 60 | eqfnfvd 6789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))) |
62 | | riotacl 7118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃!𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 →
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼) |
63 | 62 | adantl 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) →
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼) |
64 | | elmapi 8431 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ:𝐼⟶𝐵) |
65 | 64 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ:𝐼⟶𝐵) |
66 | 65, 63 | ffvelrnd 6836 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) |
67 | | fsuppind.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
68 | 67 | ralrimivva 3118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
69 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
70 | | eqeq2 2771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 = 𝑎 ↔ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
71 | 70 | ifbid 4436 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) |
72 | 71 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ))) |
73 | 72 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻)) |
74 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘𝑥) = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
75 | 74 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑏 = (ℎ‘𝑥) ↔ 𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))) |
76 | 75 | biimparc 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∧ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 𝑏 = (ℎ‘𝑥)) |
77 | 76 | ifeq1da 4444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) |
78 | 77 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))) |
79 | 78 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)) |
80 | 73, 79 | rspc2va 3550 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((℩𝑐
∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼 ∧ (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻) |
81 | 63, 66, 69, 80 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻) |
82 | 61, 81 | eqeltrd 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ ∈ 𝐻) |
83 | 82 | ex 417 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → ℎ ∈ 𝐻)) |
84 | 34, 83 | sylbid 243 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) → ℎ ∈ 𝐻)) |
85 | 23, 84 | syl5bi 245 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
86 | 85 | ralrimiva 3111 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
87 | | fsuppind.g |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐺 ∈ Grp) |
88 | 1, 27 | grpidcl 18183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈ 𝐵) |
90 | 89 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 0 ∈ 𝐵) |
91 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵 ↑m 𝐼) = (𝐵 ↑m 𝐼) |
92 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
93 | 92 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
94 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
95 | 91, 93, 94 | mapfvd 8454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑙‘𝑥) ∈ 𝐵) |
96 | 90, 95 | ifcld 4459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ 𝐵) |
97 | 96 | fmpttd 6863 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵) |
98 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐵 ∈ V) |
99 | 4 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉) |
100 | 98, 99 | elmapd 8423 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑m 𝐼) ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵)) |
101 | 97, 100 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑m 𝐼)) |
102 | 101 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑m 𝐼)) |
103 | | fvoveq1 7166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (♯‘(𝑚 supp 0 )) =
(♯‘((𝑥 ∈
𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
104 | 103 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))) |
105 | | oveq1 7150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
106 | 105 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ↔ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
107 | 104, 106 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))) |
108 | 107 | adantl 486 |
. . . . . . . . . . . . . . . . . . . . 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 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙 supp 0 ) ∈
V) |
110 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ 𝐼) |
111 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑙‘𝑧) ≠ 0 ) |
112 | | elmapfn 8440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (𝐵 ↑m 𝐼) → 𝑙 Fn 𝐼) |
113 | 112 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼) |
114 | 113 | adantr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 Fn 𝐼) |
115 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝐼 ∈ 𝑉) |
116 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 0 ∈
V) |
117 | | elsuppfn 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 ))) |
118 | 114, 115,
116, 117 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 ))) |
119 | 110, 111,
118 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 )) |
120 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈
ℕ) |
121 | 120 | nnnn0d 11979 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈
ℕ0) |
122 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 ))) |
123 | 122 | eqcomd 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) →
(♯‘(𝑙 supp
0 )) =
(𝑗 + 1)) |
124 | | hashdifsnp1 13891 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) →
((♯‘(𝑙 supp
0 )) =
(𝑗 + 1) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) = 𝑗)) |
125 | 124 | imp 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) ∧
(♯‘(𝑙 supp
0 )) =
(𝑗 + 1)) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) = 𝑗) |
126 | 109, 119,
121, 123, 125 | syl31anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) = 𝑗) |
127 | | eldifsn 4670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧)) |
128 | | fvex 6664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑙‘𝑥) ∈ V |
129 | 28, 128 | ifex 4463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ V |
130 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) |
131 | 129, 130 | fnmpti 6467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼 |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼) |
133 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉) |
134 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 0 ∈
V) |
135 | | elsuppfn 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ))) |
136 | 132, 133,
134, 135 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ))) |
137 | | iftrue 4419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ) |
138 | | olc 866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)) |
139 | 137, 138 | 2thd 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
140 | | iffalse 4422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (¬
𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = (𝑙‘𝑣)) |
141 | 140 | eqeq1d 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬
𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ (𝑙‘𝑣) = 0 )) |
142 | | biorf 935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (¬
𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 ))) |
143 | | orcom 868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 )) |
144 | 142, 143 | bitr4di 293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬
𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
145 | 141, 144 | bitrd 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (¬
𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
146 | 139, 145 | pm2.61i 185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)) |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
148 | 147 | necon3abid 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
149 | | neanior 3041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧) ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)) |
150 | 148, 149 | bitr4di 293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧))) |
151 | 150 | anbi2d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))) |
152 | | anass 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧))) |
153 | 151, 152 | bitr4di 293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧))) |
154 | | equequ1 2033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = 𝑣 → (𝑥 = 𝑧 ↔ 𝑣 = 𝑧)) |
155 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = 𝑣 → (𝑙‘𝑥) = (𝑙‘𝑣)) |
156 | 154, 155 | ifbieq2d 4439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣))) |
157 | 156, 130,
129 | fvmpt3i 6757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣))) |
158 | 157 | adantl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣))) |
159 | 158 | neeq1d 3008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 )) |
160 | 159 | pm5.32da 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ))) |
161 | 113 | adantr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 Fn 𝐼) |
162 | | elsuppfn 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ))) |
163 | 161, 133,
134, 162 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ))) |
164 | 163 | anbi1d 633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧))) |
165 | 153, 160,
164 | 3bitr4d 315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧))) |
166 | 136, 165 | bitr2d 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
167 | 127, 166 | syl5bb 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
168 | 167 | eqrdv 2757 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) |
169 | 168 | fveq2d 6655 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) =
(♯‘((𝑥 ∈
𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
170 | 169 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) =
(♯‘((𝑥 ∈
𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
171 | 126, 170 | eqtr3d 2796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
172 | 128, 28 | ifex 4463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) ∈
V |
173 | | eqid 2759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) |
174 | 172, 173 | fnmpti 6467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼 |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼) |
176 | | inidm 4119 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
177 | 132, 175,
133, 133, 176 | offn 7410 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) Fn 𝐼) |
178 | 154, 155 | ifbieq1d 4437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) |
179 | 178, 173,
172 | fvmpt3i 6757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) |
180 | 179 | adantl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) |
181 | 132, 175,
133, 133, 176, 158, 180 | ofval 7408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))) |
182 | 87 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝐺 ∈ Grp) |
183 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙‘𝑧) ≠ 0 ∧ 𝑣 ∈ 𝐼)) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
184 | 183 | anassrs 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
185 | | simpr 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼) |
186 | 91, 184, 185 | mapfvd 8454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) ∈ 𝐵) |
187 | | fsuppind.p |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ + =
(+g‘𝐺) |
188 | 1, 187, 27 | grplid 18185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ( 0 + (𝑙‘𝑣)) = (𝑙‘𝑣)) |
189 | 1, 187, 27 | grprid 18186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ((𝑙‘𝑣) + 0 ) = (𝑙‘𝑣)) |
190 | 188, 189 | ifeq12d 4434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣))) |
191 | 182, 186,
190 | syl2anc 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣))) |
192 | | ovif12 7240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) |
193 | | ifid 4453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) = (𝑙‘𝑣) |
194 | 193 | eqcomi 2768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) |
195 | 191, 192,
194 | 3eqtr4g 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = (𝑙‘𝑣)) |
196 | 181, 195 | eqtr2d 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) = (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣)) |
197 | 161, 177,
196 | eqfnfvd 6789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
198 | 197 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
199 | 171, 198 | jca 516 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
200 | 199 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
201 | 102, 108,
200 | rspcedvd 3542 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
202 | 112 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼) |
203 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼 ∈ 𝑉) |
204 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈
V) |
205 | | suppvalfn 7836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 }) |
206 | 202, 203,
204, 205 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 }) |
207 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) = (♯‘(𝑙 supp 0 ))) |
208 | | peano2nn 11671 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 ∈ ℕ → (𝑗 + 1) ∈
ℕ) |
209 | 208 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈
ℕ) |
210 | 209 | nnne0d 11709 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0) |
211 | 207, 210 | eqnetrrd 3017 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) →
(♯‘(𝑙 supp
0 )) ≠
0) |
212 | | ovex 7176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑙 supp 0 ) ∈
V |
213 | | hasheq0 13759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑙 supp 0 ) ∈ V →
((♯‘(𝑙 supp
0 )) = 0
↔ (𝑙 supp 0 ) =
∅)) |
214 | 213 | necon3bid 2993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 supp 0 ) ∈ V →
((♯‘(𝑙 supp
0 )) ≠
0 ↔ (𝑙 supp 0 ) ≠
∅)) |
215 | 212, 214 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) →
((♯‘(𝑙 supp
0 )) ≠
0 ↔ (𝑙 supp 0 ) ≠
∅)) |
216 | 211, 215 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) ≠
∅) |
217 | 206, 216 | eqnetrrd 3017 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠
∅) |
218 | | rabn0 4275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅ ↔
∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 ) |
219 | 217, 218 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 ) |
220 | 201, 219 | reximddv 3197 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 ∃𝑚 ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
221 | | rexcom 3271 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧 ∈
𝐼 ∃𝑚 ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ ∃𝑚 ∈ (𝐵 ↑m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
222 | 220, 221 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑚 ∈ (𝐵 ↑m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
223 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
224 | | fvoveq1 7166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (ℎ = 𝑚 → (♯‘(ℎ supp 0 )) = (♯‘(𝑚 supp 0 ))) |
225 | 224 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ℎ = 𝑚 → (𝑗 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 )))) |
226 | | eleq1w 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ℎ = 𝑚 → (ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻)) |
227 | 225, 226 | imbi12d 349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℎ = 𝑚 → ((𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))) |
228 | 227 | rspccva 3538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀ℎ ∈
(𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)) |
229 | 228 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)) |
230 | 229 | imp 411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻) |
231 | 230 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻) |
232 | 231 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻) |
233 | 232 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑚 ∈ 𝐻) |
234 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑧 ∈ 𝐼) |
235 | 92 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
236 | 91, 235, 234 | mapfvd 8454 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑙‘𝑧) ∈ 𝐵) |
237 | 68 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
238 | | equequ2 2034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = 𝑧 → (𝑥 = 𝑎 ↔ 𝑥 = 𝑧)) |
239 | 238 | ifbid 4436 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 )) |
240 | 239 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑧 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 ))) |
241 | 240 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑧 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻)) |
242 | | fveq2 6651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑧 → (𝑙‘𝑥) = (𝑙‘𝑧)) |
243 | 242 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 𝑧 → (𝑏 = (𝑙‘𝑥) ↔ 𝑏 = (𝑙‘𝑧))) |
244 | 243 | biimparc 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑏 = (𝑙‘𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙‘𝑥)) |
245 | 244 | ifeq1da 4444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 = (𝑙‘𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) |
246 | 245 | mpteq2dv 5121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 = (𝑙‘𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) |
247 | 246 | eleq1d 2835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = (𝑙‘𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)) |
248 | 241, 247 | rspc2va 3550 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) |
249 | 234, 236,
237, 248 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) |
250 | | fsuppind.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻) |
251 | 250 | ralrimivva 3118 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘f + 𝑦) ∈ 𝐻) |
252 | 251 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘f + 𝑦) ∈ 𝐻) |
253 | | ovrspc2v 7169 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑚 ∈ 𝐻 ∧ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) ∧ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘f + 𝑦) ∈ 𝐻) → (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻) |
254 | 233, 249,
252, 253 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻) |
255 | 223, 254 | eqeltrd 2851 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ 𝐻) |
256 | 255 | ex 417 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻)) |
257 | 256 | rexlimdvva 3216 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (∃𝑚 ∈ (𝐵 ↑m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻)) |
258 | 222, 257 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ 𝐻) |
259 | 258 | exp32 425 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → (𝑙 ∈ (𝐵 ↑m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻))) |
260 | 259 | ralrimiv 3110 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀𝑙 ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻)) |
261 | | fvoveq1 7166 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = ℎ → (♯‘(𝑙 supp 0 )) = (♯‘(ℎ supp 0 ))) |
262 | 261 | eqeq2d 2770 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = ℎ → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 )))) |
263 | | eleq1w 2833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = ℎ → (𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻)) |
264 | 262, 263 | imbi12d 349 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = ℎ → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
265 | 264 | cbvralvw 3359 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
(𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
266 | 260, 265 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀ℎ ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
267 | 9, 12, 15, 18, 86, 266 | nnindd 11679 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
268 | 267 | ralrimiva 3111 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
269 | | ralcom 3270 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ ∀ℎ ∈
(𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
270 | 268, 269 | sylib 221 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
271 | | biidd 265 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (♯‘(ℎ supp 0 )) → (ℎ ∈ 𝐻 ↔ ℎ ∈ 𝐻)) |
272 | 271 | ceqsralv 3448 |
. . . . . . . . . . . . 13
⊢
((♯‘(ℎ
supp 0 ))
∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ℎ ∈ 𝐻)) |
273 | 272 | biimpcd 252 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ (𝑛 =
(♯‘(ℎ supp 0 )) →
ℎ ∈ 𝐻) → ((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻)) |
274 | 273 | ralimi 3090 |
. . . . . . . . . . 11
⊢
(∀ℎ ∈
(𝐵 ↑m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ∀ℎ ∈ (𝐵 ↑m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻)) |
275 | 270, 274 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻)) |
276 | | fvoveq1 7166 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑋 → (♯‘(ℎ supp 0 )) = (♯‘(𝑋 supp 0 ))) |
277 | 276 | eleq1d 2835 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑋 → ((♯‘(ℎ supp 0 )) ∈ ℕ ↔
(♯‘(𝑋 supp
0 ))
∈ ℕ)) |
278 | | eleq1 2838 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑋 → (ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻)) |
279 | 277, 278 | imbi12d 349 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑋 → (((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ →
𝑋 ∈ 𝐻))) |
280 | 279 | rspcv 3534 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m 𝐼) → (∀ℎ ∈ (𝐵 ↑m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ →
𝑋 ∈ 𝐻))) |
281 | 275, 280 | syl5com 31 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ →
𝑋 ∈ 𝐻))) |
282 | 281 | com23 86 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ →
(𝑋 ∈ (𝐵 ↑m 𝐼) → 𝑋 ∈ 𝐻))) |
283 | 282 | imp 411 |
. . . . . . 7
⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
(𝑋 ∈ (𝐵 ↑m 𝐼) → 𝑋 ∈ 𝐻)) |
284 | 6, 283 | sylbird 263 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
(𝑋:𝐼⟶𝐵 → 𝑋 ∈ 𝐻)) |
285 | 284 | imp 411 |
. . . . 5
⊢ (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧
𝑋:𝐼⟶𝐵) → 𝑋 ∈ 𝐻) |
286 | 285 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
𝑋 ∈ 𝐻) |
287 | 286 | adantlr 715 |
. . 3
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧
(♯‘(𝑋 supp
0 ))
∈ ℕ) → 𝑋
∈ 𝐻) |
288 | | ovex 7176 |
. . . . 5
⊢ (𝑋 supp 0 ) ∈
V |
289 | | hasheq0 13759 |
. . . . 5
⊢ ((𝑋 supp 0 ) ∈ V →
((♯‘(𝑋 supp
0 )) = 0
↔ (𝑋 supp 0 ) =
∅)) |
290 | 288, 289 | ax-mp 5 |
. . . 4
⊢
((♯‘(𝑋
supp 0 ))
= 0 ↔ (𝑋 supp 0 ) =
∅) |
291 | | ffn 6491 |
. . . . . . . 8
⊢ (𝑋:𝐼⟶𝐵 → 𝑋 Fn 𝐼) |
292 | 291 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼) |
293 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉) |
294 | 28 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈
V) |
295 | | fnsuppeq0 7859 |
. . . . . . 7
⊢ ((𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 }))) |
296 | 292, 293,
294, 295 | syl3anc 1369 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 }))) |
297 | 296 | biimpa 481 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 })) |
298 | | fsuppind.0 |
. . . . . 6
⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻) |
299 | 298 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻) |
300 | 297, 299 | eqeltrd 2851 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 ∈ 𝐻) |
301 | 290, 300 | sylan2b 597 |
. . 3
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧
(♯‘(𝑋 supp
0 )) = 0)
→ 𝑋 ∈ 𝐻) |
302 | | simpr 489 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 ) |
303 | 302 | fsuppimpd 8858 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈
Fin) |
304 | | hashcl 13752 |
. . . . 5
⊢ ((𝑋 supp 0 ) ∈ Fin →
(♯‘(𝑋 supp
0 ))
∈ ℕ0) |
305 | 303, 304 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) →
(♯‘(𝑋 supp
0 ))
∈ ℕ0) |
306 | | elnn0 11921 |
. . . 4
⊢
((♯‘(𝑋
supp 0 ))
∈ ℕ0 ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨
(♯‘(𝑋 supp
0 )) =
0)) |
307 | 305, 306 | sylib 221 |
. . 3
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) →
((♯‘(𝑋 supp
0 ))
∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0)) |
308 | 287, 301,
307 | mpjaodan 957 |
. 2
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 ∈ 𝐻) |
309 | 308 | anasss 471 |
1
⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻) |