| Step | Hyp | Ref
| Expression |
| 1 | | fsuppind.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐺) |
| 2 | 1 | fvexi 6920 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
| 3 | 2 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ V) |
| 4 | | fsuppind.v |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 5 | 3, 4 | elmapd 8880 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑m 𝐼) ↔ 𝑋:𝐼⟶𝐵)) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
(𝑋 ∈ (𝐵 ↑m 𝐼) ↔ 𝑋:𝐼⟶𝐵)) |
| 7 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 1 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 1 =
(♯‘(ℎ supp 0
)))) |
| 8 | 7 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 1 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 9 | 8 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 10 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(ℎ supp 0 )))) |
| 11 | 10 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 12 | 11 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 13 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 + 1) → (𝑖 = (♯‘(ℎ supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 )))) |
| 14 | 13 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 + 1) → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 15 | 14 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑗 + 1) → (∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 16 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑛 → (𝑖 = (♯‘(ℎ supp 0 )) ↔ 𝑛 = (♯‘(ℎ supp 0 )))) |
| 17 | 16 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → ((𝑖 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 18 | 17 | ralbidv 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 ))) |
| 22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(ℎ
supp 0 ))
= 1 ↔ ∃!𝑐 𝑐 ∈ (ℎ supp 0 )) |
| 23 | 19, 22 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ (1 =
(♯‘(ℎ supp 0 )) ↔
∃!𝑐 𝑐 ∈ (ℎ supp 0 )) |
| 24 | | elmapfn 8905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ Fn 𝐼) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → ℎ Fn 𝐼) |
| 26 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → 𝐼 ∈ 𝑉) |
| 27 | | fsuppind.z |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 =
(0g‘𝐺) |
| 28 | 27 | fvexi 6920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
V |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → 0 ∈ V) |
| 30 | | elsuppfn 8195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))) |
| 31 | 25, 26, 29, 30 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (𝑐 ∈ (ℎ supp 0 ) ↔ (𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))) |
| 32 | 31 | eubidv 2586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 ))) |
| 33 | | df-reu 3381 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃!𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ↔ ∃!𝑐(𝑐 ∈ 𝐼 ∧ (ℎ‘𝑐) ≠ 0 )) |
| 34 | 32, 33 | bitr4di 289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) ↔ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) |
| 35 | 24 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ Fn 𝐼) |
| 36 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ‘𝑥) ∈ V |
| 37 | 36, 28 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) ∈
V |
| 38 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) |
| 39 | 37, 38 | fnmpti 6711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼 |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) Fn 𝐼) |
| 41 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑣 → (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
| 42 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑣 → (ℎ‘𝑥) = (ℎ‘𝑣)) |
| 43 | 41, 42 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑣 → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 )) |
| 44 | 43, 38, 37 | fvmpt3i 7021 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣) = if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 )) |
| 45 | 44 | adantl 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
⊢ (𝑐 = 𝑣 → (ℎ‘𝑐) = (ℎ‘𝑣)) |
| 50 | 49 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = 𝑣 → ((ℎ‘𝑐) ≠ 0 ↔ (ℎ‘𝑣) ≠ 0 )) |
| 51 | 50 | riota2 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ 𝐼 ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((ℎ‘𝑣) ≠ 0 ↔
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣)) |
| 52 | 47, 48, 51 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((ℎ‘𝑣) ≠ 0 ↔
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣)) |
| 53 | | necom 2994 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ( 0 ≠ (ℎ‘𝑣) ↔ (ℎ‘𝑣) ≠ 0 ) |
| 54 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ↔
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) = 𝑣) |
| 55 | 52, 53, 54 | 3bitr4g 314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) ↔ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
| 56 | 55 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ( 0 ≠ (ℎ‘𝑣) → 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
| 57 | 56 | necon1bd 2958 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → 0 = (ℎ‘𝑣))) |
| 58 | 57 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) ∧ ¬ 𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 0 = (ℎ‘𝑣)) |
| 59 | 46, 58 | ifeqda 4562 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → if(𝑣 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑣), 0 ) = (ℎ‘𝑣)) |
| 60 | 45, 59 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (ℎ‘𝑣) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))‘𝑣)) |
| 61 | 35, 40, 60 | eqfnfvd 7054 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))) |
| 62 | | riotacl 7405 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃!𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 →
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) →
(℩𝑐 ∈
𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼) |
| 64 | | elmapi 8889 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ:𝐼⟶𝐵) |
| 65 | 64 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ:𝐼⟶𝐵) |
| 66 | 65, 63 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) |
| 67 | | fsuppind.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
| 68 | 67 | ralrimivva 3202 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
| 69 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
| 70 | | eqeq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 = 𝑎 ↔ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
| 71 | 70 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) |
| 72 | 71 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ))) |
| 73 | 72 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻)) |
| 74 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (ℎ‘𝑥) = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ))) |
| 75 | 74 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑏 = (ℎ‘𝑥) ↔ 𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )))) |
| 76 | 75 | biimparc 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∧ 𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → 𝑏 = (ℎ‘𝑥)) |
| 77 | 76 | ifeq1da 4557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 ) = if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) |
| 78 | 77 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 ))) |
| 79 | 78 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 = (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻)) |
| 80 | 73, 79 | rspc2va 3634 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((℩𝑐
∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) ∈ 𝐼 ∧ (ℎ‘(℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 )) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻) |
| 81 | 63, 66, 69, 80 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = (℩𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ), (ℎ‘𝑥), 0 )) ∈ 𝐻) |
| 82 | 61, 81 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) ∧ ∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 ) → ℎ ∈ 𝐻) |
| 83 | 82 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 ∈ 𝐼 (ℎ‘𝑐) ≠ 0 → ℎ ∈ 𝐻)) |
| 84 | 34, 83 | sylbid 240 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (∃!𝑐 𝑐 ∈ (ℎ supp 0 ) → ℎ ∈ 𝐻)) |
| 85 | 23, 84 | biimtrid 242 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ℎ ∈ (𝐵 ↑m 𝐼)) → (1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 86 | 85 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑m 𝐼)(1 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 87 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (♯‘(𝑚 supp 0 )) =
(♯‘((𝑥 ∈
𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
| 88 | 87 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑗 = (♯‘(𝑚 supp 0 )) ↔ 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )))) |
| 89 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
| 90 | 89 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → (𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ↔ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
| 91 | 88, 90 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) ↔ (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))))) |
| 92 | | fsuppind.g |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 93 | 1, 27 | grpidcl 18983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
| 94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈ 𝐵) |
| 95 | 94 | ad5antr 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 𝐼)) |
| 98 | 97 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
| 99 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
| 100 | 96, 98, 99 | mapfvd 8919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → (𝑙‘𝑥) ∈ 𝐵) |
| 101 | 95, 100 | ifcld 4572 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ 𝐵) |
| 102 | 101 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵) |
| 103 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐵 ∈ V) |
| 104 | 4 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉) |
| 105 | 103, 104 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑m 𝐼) ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))):𝐼⟶𝐵)) |
| 106 | 102, 105 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∈ (𝐵 ↑m 𝐼)) |
| 107 | 106 | adantrl 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 𝐼) |
| 112 | 111 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼) |
| 113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 Fn 𝐼) |
| 114 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝐼 ∈ 𝑉) |
| 115 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 0 ∈
V) |
| 116 | | elsuppfn 8195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 ))) |
| 117 | 113, 114,
115, 116 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑧 ∈ (𝑙 supp 0 ) ↔ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 ))) |
| 118 | 109, 110,
117 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑧 ∈ (𝑙 supp 0 )) |
| 119 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈
ℕ) |
| 120 | 119 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 ∈
ℕ0) |
| 121 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 + 1) = (♯‘(𝑙 supp 0 ))) |
| 122 | 121 | eqcomd 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 )
∖ {𝑧})) = 𝑗)) |
| 124 | 123 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑙 supp 0 ) ∈ V ∧ 𝑧 ∈ (𝑙 supp 0 ) ∧ 𝑗 ∈ ℕ0) ∧
(♯‘(𝑙 supp
0 )) =
(𝑗 + 1)) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) = 𝑗) |
| 125 | 108, 118,
120, 122, 124 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) = 𝑗) |
| 126 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧)) |
| 127 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑙‘𝑥) ∈ V |
| 128 | 28, 127 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) ∈ V |
| 129 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) |
| 130 | 128, 129 | fnmpti 6711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼 |
| 131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) Fn 𝐼) |
| 132 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝐼 ∈ 𝑉) |
| 133 | 28 | a1i 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 ))) |
| 135 | 131, 132,
133, 134 | syl3anc 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 ∨ 𝑣 = 𝑧)) |
| 138 | 136, 137 | 2thd 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
| 139 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (¬
𝑣 = 𝑧 → if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = (𝑙‘𝑣)) |
| 140 | 139 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬
𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ (𝑙‘𝑣) = 0 )) |
| 141 | | biorf 937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (¬
𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 ))) |
| 142 | | orcom 871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧) ↔ (𝑣 = 𝑧 ∨ (𝑙‘𝑣) = 0 )) |
| 143 | 141, 142 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬
𝑣 = 𝑧 → ((𝑙‘𝑣) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
| 144 | 140, 143 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (¬
𝑣 = 𝑧 → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
| 145 | 138, 144 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)) |
| 146 | 145 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) = 0 ↔ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
| 147 | 146 | necon3abid 2977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧))) |
| 148 | | neanior 3035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧) ↔ ¬ ((𝑙‘𝑣) = 0 ∨ 𝑣 = 𝑧)) |
| 149 | 147, 148 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ↔ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧))) |
| 150 | 149 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧)))) |
| 151 | | anass 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧) ↔ (𝑣 ∈ 𝐼 ∧ ((𝑙‘𝑣) ≠ 0 ∧ 𝑣 ≠ 𝑧))) |
| 152 | 150, 151 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧))) |
| 153 | | equequ1 2024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = 𝑣 → (𝑥 = 𝑧 ↔ 𝑣 = 𝑧)) |
| 154 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = 𝑣 → (𝑙‘𝑥) = (𝑙‘𝑣)) |
| 155 | 153, 154 | ifbieq2d 4552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣))) |
| 156 | 155, 129,
128 | fvmpt3i 7021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣))) |
| 157 | 156 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) = if(𝑣 = 𝑧, 0 , (𝑙‘𝑣))) |
| 158 | 157 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ↔ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 )) |
| 159 | 158 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ 𝐼 ∧ if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) ≠ 0 ))) |
| 160 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 Fn 𝐼) |
| 161 | | elsuppfn 8195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ))) |
| 162 | 160, 132,
133, 161 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ (𝑙 supp 0 ) ↔ (𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ))) |
| 163 | 162 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ ((𝑣 ∈ 𝐼 ∧ (𝑙‘𝑣) ≠ 0 ) ∧ 𝑣 ≠ 𝑧))) |
| 164 | 152, 159,
163 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ 𝐼 ∧ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥)))‘𝑣) ≠ 0 ) ↔ (𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧))) |
| 165 | 135, 164 | bitr2d 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑣 ∈ (𝑙 supp 0 ) ∧ 𝑣 ≠ 𝑧) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
| 166 | 126, 165 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑣 ∈ ((𝑙 supp 0 ) ∖ {𝑧}) ↔ 𝑣 ∈ ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
| 167 | 166 | eqrdv 2735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑙 supp 0 ) ∖ {𝑧}) = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) |
| 168 | 167 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) =
(♯‘((𝑥 ∈
𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
| 169 | 168 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) →
(♯‘((𝑙 supp
0 )
∖ {𝑧})) =
(♯‘((𝑥 ∈
𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
| 170 | 125, 169 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 ))) |
| 171 | 127, 28 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) ∈
V |
| 172 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) |
| 173 | 171, 172 | fnmpti 6711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼 |
| 174 | 173 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) Fn 𝐼) |
| 175 | | inidm 4227 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
| 176 | 131, 174,
132, 132, 175 | offn 7710 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) Fn 𝐼) |
| 177 | 153, 154 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑣 → if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) |
| 178 | 177, 172,
171 | fvmpt3i 7021 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑣 ∈ 𝐼 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) |
| 179 | 178 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) |
| 180 | 131, 174,
132, 132, 175, 157, 179 | ofval 7708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣) = (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 ))) |
| 181 | 92 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝐺 ∈ Grp) |
| 182 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ ((𝑙‘𝑧) ≠ 0 ∧ 𝑣 ∈ 𝐼)) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
| 183 | 182 | anassrs 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
| 184 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼) |
| 185 | 96, 183, 184 | mapfvd 8919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) ∈ 𝐵) |
| 186 | | fsuppind.p |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ + =
(+g‘𝐺) |
| 187 | 1, 186, 27 | grplid 18985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ( 0 + (𝑙‘𝑣)) = (𝑙‘𝑣)) |
| 188 | 1, 186, 27 | grprid 18986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → ((𝑙‘𝑣) + 0 ) = (𝑙‘𝑣)) |
| 189 | 187, 188 | ifeq12d 4547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐺 ∈ Grp ∧ (𝑙‘𝑣) ∈ 𝐵) → if(𝑣 = 𝑧, ( 0 + (𝑙‘𝑣)), ((𝑙‘𝑣) + 0 )) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣))) |
| 190 | 181, 185,
189 | syl2anc 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(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) = (𝑙‘𝑣) |
| 193 | 192 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙‘𝑣) = if(𝑣 = 𝑧, (𝑙‘𝑣), (𝑙‘𝑣)) |
| 194 | 190, 191,
193 | 3eqtr4g 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (if(𝑣 = 𝑧, 0 , (𝑙‘𝑣)) + if(𝑣 = 𝑧, (𝑙‘𝑣), 0 )) = (𝑙‘𝑣)) |
| 195 | 180, 194 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) ∧ 𝑣 ∈ 𝐼) → (𝑙‘𝑣) = (((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))‘𝑣)) |
| 196 | 160, 176,
195 | eqfnfvd 7054 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑙‘𝑧) ≠ 0 ) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
| 197 | 196 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) |
| 198 | 170, 197 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
| 199 | 198 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → (𝑗 = (♯‘((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) supp 0 )) ∧ 𝑙 = ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 0 , (𝑙‘𝑥))) ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
| 200 | 91, 107, 199 | rspcedvdw 3625 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ≠ 0 )) → ∃𝑚 ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) |
| 201 | 111 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 Fn 𝐼) |
| 202 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝐼 ∈ 𝑉) |
| 203 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 0 ∈
V) |
| 204 | | suppvalfn 8193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑙 supp 0 ) = {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 }) |
| 205 | 201, 202,
203, 204 | syl3anc 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) ∈
ℕ) |
| 208 | 207 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ∈
ℕ) |
| 209 | 208 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑗 + 1) ≠ 0) |
| 210 | 206, 209 | eqnetrrd 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 ) =
∅)) |
| 213 | 212 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 supp 0 ) ∈ V →
((♯‘(𝑙 supp
0 )) ≠
0 ↔ (𝑙 supp 0 ) ≠
∅)) |
| 214 | 211, 213 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) →
((♯‘(𝑙 supp
0 )) ≠
0 ↔ (𝑙 supp 0 ) ≠
∅)) |
| 215 | 210, 214 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (𝑙 supp 0 ) ≠
∅) |
| 216 | 205, 215 | eqnetrrd 3009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → {𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠
∅) |
| 217 | | rabn0 4389 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑧 ∈ 𝐼 ∣ (𝑙‘𝑧) ≠ 0 } ≠ ∅ ↔
∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 ) |
| 218 | 216, 217 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → ∃𝑧 ∈ 𝐼 (𝑙‘𝑧) ≠ 0 ) |
| 219 | 200, 218 | reximddv 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 ))))) |
| 221 | 219, 220 | sylib 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 ))) |
| 224 | 223 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ℎ = 𝑚 → (𝑗 = (♯‘(ℎ supp 0 )) ↔ 𝑗 = (♯‘(𝑚 supp 0 )))) |
| 225 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ℎ = 𝑚 → (ℎ ∈ 𝐻 ↔ 𝑚 ∈ 𝐻)) |
| 226 | 224, 225 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℎ = 𝑚 → ((𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻))) |
| 227 | 226 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((∀ℎ ∈
(𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)) |
| 228 | 227 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) → (𝑗 = (♯‘(𝑚 supp 0 )) → 𝑚 ∈ 𝐻)) |
| 229 | 228 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻) |
| 230 | 229 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ 𝑚 ∈ (𝐵 ↑m 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻) |
| 231 | 230 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ 𝑗 = (♯‘(𝑚 supp 0 ))) → 𝑚 ∈ 𝐻) |
| 232 | 231 | adantrr 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 ))))) → 𝑧 ∈ 𝐼) |
| 234 | 97 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ (𝐵 ↑m 𝐼)) |
| 235 | 96, 234, 233 | mapfvd 8919 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑙‘𝑧) ∈ 𝐵) |
| 236 | 68 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) |
| 237 | | equequ2 2025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = 𝑧 → (𝑥 = 𝑎 ↔ 𝑥 = 𝑧)) |
| 238 | 237 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑧 → if(𝑥 = 𝑎, 𝑏, 0 ) = if(𝑥 = 𝑧, 𝑏, 0 )) |
| 239 | 238 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑧 → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 ))) |
| 240 | 239 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑧 → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻)) |
| 241 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑧 → (𝑙‘𝑥) = (𝑙‘𝑧)) |
| 242 | 241 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 𝑧 → (𝑏 = (𝑙‘𝑥) ↔ 𝑏 = (𝑙‘𝑧))) |
| 243 | 242 | biimparc 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑏 = (𝑙‘𝑧) ∧ 𝑥 = 𝑧) → 𝑏 = (𝑙‘𝑥)) |
| 244 | 243 | ifeq1da 4557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 = (𝑙‘𝑧) → if(𝑥 = 𝑧, 𝑏, 0 ) = if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) |
| 245 | 244 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 = (𝑙‘𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) |
| 246 | 245 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = (𝑙‘𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, 𝑏, 0 )) ∈ 𝐻 ↔ (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻)) |
| 247 | 240, 246 | rspc2va 3634 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑧 ∈ 𝐼 ∧ (𝑙‘𝑧) ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐼 ∀𝑏 ∈ 𝐵 (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) |
| 248 | 233, 235,
236, 247 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )) ∈ 𝐻) |
| 249 | | fsuppind.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 ∘f + 𝑦) ∈ 𝐻) |
| 250 | 249 | ralrimivva 3202 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 ∘f + 𝑦) ∈ 𝐻) |
| 251 | 250 | ad5antr 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 ))) ∈ 𝐻) |
| 253 | 232, 248,
251, 252 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))) ∈ 𝐻) |
| 254 | 222, 253 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) ∧ (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 ))))) → 𝑙 ∈ 𝐻) |
| 255 | 254 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑗 ∈ ℕ) ∧
∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) ∧ (𝑚 ∈ (𝐵 ↑m 𝐼) ∧ 𝑧 ∈ 𝐼)) → ((𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻)) |
| 256 | 255 | rexlimdvva 3213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → (∃𝑚 ∈ (𝐵 ↑m 𝐼)∃𝑧 ∈ 𝐼 (𝑗 = (♯‘(𝑚 supp 0 )) ∧ 𝑙 = (𝑚 ∘f + (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑧, (𝑙‘𝑥), 0 )))) → 𝑙 ∈ 𝐻)) |
| 257 | 221, 256 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) ∧ (𝑙 ∈ (𝐵 ↑m 𝐼) ∧ (𝑗 + 1) = (♯‘(𝑙 supp 0 )))) → 𝑙 ∈ 𝐻) |
| 258 | 257 | exp32 420 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → (𝑙 ∈ (𝐵 ↑m 𝐼) → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻))) |
| 259 | 258 | ralrimiv 3145 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀𝑙 ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻)) |
| 260 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = ℎ → (♯‘(𝑙 supp 0 )) = (♯‘(ℎ supp 0 ))) |
| 261 | 260 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = ℎ → ((𝑗 + 1) = (♯‘(𝑙 supp 0 )) ↔ (𝑗 + 1) = (♯‘(ℎ supp 0 )))) |
| 262 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = ℎ → (𝑙 ∈ 𝐻 ↔ ℎ ∈ 𝐻)) |
| 263 | 261, 262 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = ℎ → (((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻))) |
| 264 | 263 | cbvralvw 3237 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑙 ∈
(𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(𝑙 supp 0 )) → 𝑙 ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 265 | 259, 264 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑗 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) → ∀ℎ ∈ (𝐵 ↑m 𝐼)((𝑗 + 1) = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 266 | 9, 12, 15, 18, 86, 265 | nnindd 12286 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 267 | 266 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀ℎ ∈ (𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 268 | | ralcom 3289 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ ∀ℎ ∈
(𝐵 ↑m 𝐼)(𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ∀ℎ ∈ (𝐵 ↑m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 269 | 267, 268 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻)) |
| 270 | | biidd 262 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (♯‘(ℎ supp 0 )) → (ℎ ∈ 𝐻 ↔ ℎ ∈ 𝐻)) |
| 271 | 270 | ceqsralv 3522 |
. . . . . . . . . . . . 13
⊢
((♯‘(ℎ
supp 0 ))
∈ ℕ → (∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) ↔ ℎ ∈ 𝐻)) |
| 272 | 271 | biimpcd 249 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ℕ (𝑛 =
(♯‘(ℎ supp 0 )) →
ℎ ∈ 𝐻) → ((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻)) |
| 273 | 272 | ralimi 3083 |
. . . . . . . . . . 11
⊢
(∀ℎ ∈
(𝐵 ↑m 𝐼)∀𝑛 ∈ ℕ (𝑛 = (♯‘(ℎ supp 0 )) → ℎ ∈ 𝐻) → ∀ℎ ∈ (𝐵 ↑m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻)) |
| 274 | 269, 273 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∀ℎ ∈ (𝐵 ↑m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻)) |
| 275 | | fvoveq1 7454 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑋 → (♯‘(ℎ supp 0 )) = (♯‘(𝑋 supp 0 ))) |
| 276 | 275 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑋 → ((♯‘(ℎ supp 0 )) ∈ ℕ ↔
(♯‘(𝑋 supp
0 ))
∈ ℕ)) |
| 277 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑋 → (ℎ ∈ 𝐻 ↔ 𝑋 ∈ 𝐻)) |
| 278 | 276, 277 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑋 → (((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻) ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ →
𝑋 ∈ 𝐻))) |
| 279 | 278 | rspcv 3618 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐵 ↑m 𝐼) → (∀ℎ ∈ (𝐵 ↑m 𝐼)((♯‘(ℎ supp 0 )) ∈ ℕ →
ℎ ∈ 𝐻) → ((♯‘(𝑋 supp 0 )) ∈ ℕ →
𝑋 ∈ 𝐻))) |
| 280 | 274, 279 | syl5com 31 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ (𝐵 ↑m 𝐼) → ((♯‘(𝑋 supp 0 )) ∈ ℕ →
𝑋 ∈ 𝐻))) |
| 281 | 280 | com23 86 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝑋 supp 0 )) ∈ ℕ →
(𝑋 ∈ (𝐵 ↑m 𝐼) → 𝑋 ∈ 𝐻))) |
| 282 | 281 | imp 406 |
. . . . . . 7
⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
(𝑋 ∈ (𝐵 ↑m 𝐼) → 𝑋 ∈ 𝐻)) |
| 283 | 6, 282 | sylbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
(𝑋:𝐼⟶𝐵 → 𝑋 ∈ 𝐻)) |
| 284 | 283 | imp 406 |
. . . . 5
⊢ (((𝜑 ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) ∧
𝑋:𝐼⟶𝐵) → 𝑋 ∈ 𝐻) |
| 285 | 284 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ (♯‘(𝑋 supp 0 )) ∈ ℕ) →
𝑋 ∈ 𝐻) |
| 286 | 285 | adantlr 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 ) =
∅)) |
| 289 | 287, 288 | ax-mp 5 |
. . . 4
⊢
((♯‘(𝑋
supp 0 ))
= 0 ↔ (𝑋 supp 0 ) =
∅) |
| 290 | | ffn 6736 |
. . . . . . . 8
⊢ (𝑋:𝐼⟶𝐵 → 𝑋 Fn 𝐼) |
| 291 | 290 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 Fn 𝐼) |
| 292 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝐼 ∈ 𝑉) |
| 293 | 28 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 0 ∈
V) |
| 294 | | fnsuppeq0 8217 |
. . . . . . 7
⊢ ((𝑋 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 }))) |
| 295 | 291, 292,
293, 294 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → ((𝑋 supp 0 ) = ∅ ↔ 𝑋 = (𝐼 × { 0 }))) |
| 296 | 295 | biimpa 476 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 = (𝐼 × { 0 })) |
| 297 | | fsuppind.0 |
. . . . . 6
⊢ (𝜑 → (𝐼 × { 0 }) ∈ 𝐻) |
| 298 | 297 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → (𝐼 × { 0 }) ∈ 𝐻) |
| 299 | 296, 298 | eqeltrd 2841 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧ (𝑋 supp 0 ) = ∅) → 𝑋 ∈ 𝐻) |
| 300 | 289, 299 | sylan2b 594 |
. . 3
⊢ ((((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) ∧
(♯‘(𝑋 supp
0 )) = 0)
→ 𝑋 ∈ 𝐻) |
| 301 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 finSupp 0 ) |
| 302 | 301 | fsuppimpd 9409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → (𝑋 supp 0 ) ∈
Fin) |
| 303 | | hashcl 14395 |
. . . . 5
⊢ ((𝑋 supp 0 ) ∈ Fin →
(♯‘(𝑋 supp
0 ))
∈ ℕ0) |
| 304 | 302, 303 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) →
(♯‘(𝑋 supp
0 ))
∈ ℕ0) |
| 305 | | elnn0 12528 |
. . . 4
⊢
((♯‘(𝑋
supp 0 ))
∈ ℕ0 ↔ ((♯‘(𝑋 supp 0 )) ∈ ℕ ∨
(♯‘(𝑋 supp
0 )) =
0)) |
| 306 | 304, 305 | sylib 218 |
. . 3
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) →
((♯‘(𝑋 supp
0 ))
∈ ℕ ∨ (♯‘(𝑋 supp 0 )) = 0)) |
| 307 | 286, 300,
306 | mpjaodan 961 |
. 2
⊢ (((𝜑 ∧ 𝑋:𝐼⟶𝐵) ∧ 𝑋 finSupp 0 ) → 𝑋 ∈ 𝐻) |
| 308 | 307 | anasss 466 |
1
⊢ ((𝜑 ∧ (𝑋:𝐼⟶𝐵 ∧ 𝑋 finSupp 0 )) → 𝑋 ∈ 𝐻) |