| Step | Hyp | Ref
| Expression |
| 1 | | rexnal 3100 |
. . . . 5
⊢
(∃𝑥 ∈
𝐼 ¬ (𝑋‘𝑥) = 0 ↔ ¬ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = 0) |
| 2 | | df-ne 2941 |
. . . . . . 7
⊢ ((𝑋‘𝑥) ≠ 0 ↔ ¬ (𝑋‘𝑥) = 0) |
| 3 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑋 → (ℂfld
Σg ℎ) = (ℂfld
Σg 𝑋)) |
| 4 | | tdeglem.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) |
| 5 | | ovex 7464 |
. . . . . . . . . . . 12
⊢
(ℂfld Σg 𝑋) ∈ V |
| 6 | 3, 4, 5 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐴 → (𝐻‘𝑋) = (ℂfld
Σg 𝑋)) |
| 7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝐻‘𝑋) = (ℂfld
Σg 𝑋)) |
| 8 | | tdeglem.a |
. . . . . . . . . . . . . 14
⊢ 𝐴 = {𝑚 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑚 “ ℕ) ∈
Fin} |
| 9 | 8 | psrbagf 21938 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐴 → 𝑋:𝐼⟶ℕ0) |
| 10 | 9 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → 𝑋 = (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦))) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → 𝑋 = (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦))) |
| 12 | 11 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (ℂfld
Σg 𝑋) = (ℂfld
Σg (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)))) |
| 13 | | cnfldbas 21368 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
| 14 | | cnfld0 21405 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘ℂfld) |
| 15 | | cnfldadd 21370 |
. . . . . . . . . . 11
⊢ + =
(+g‘ℂfld) |
| 16 | | cnring 21403 |
. . . . . . . . . . . 12
⊢
ℂfld ∈ Ring |
| 17 | | ringcmn 20279 |
. . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
| 18 | 16, 17 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ℂfld
∈ CMnd) |
| 19 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ 𝐴) |
| 20 | 9 | ffnd 6737 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐴 → 𝑋 Fn 𝐼) |
| 21 | 19, 20 | fndmexd 7926 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → 𝐼 ∈ V) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → 𝐼 ∈ V) |
| 23 | 9 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐼) → (𝑋‘𝑦) ∈
ℕ0) |
| 24 | 23 | nn0cnd 12589 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐼) → (𝑋‘𝑦) ∈ ℂ) |
| 25 | 24 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) ∧ 𝑦 ∈ 𝐼) → (𝑋‘𝑦) ∈ ℂ) |
| 26 | 8 | psrbagfsupp 21939 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝐴 → 𝑋 finSupp 0) |
| 27 | 10, 26 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝐴 → (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) finSupp 0) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) finSupp 0) |
| 29 | | disjdifr 4473 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∖ {𝑥}) ∩ {𝑥}) = ∅ |
| 30 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ((𝐼 ∖ {𝑥}) ∩ {𝑥}) = ∅) |
| 31 | | difsnid 4810 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐼 → ((𝐼 ∖ {𝑥}) ∪ {𝑥}) = 𝐼) |
| 32 | 31 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 → 𝐼 = ((𝐼 ∖ {𝑥}) ∪ {𝑥})) |
| 33 | 32 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → 𝐼 = ((𝐼 ∖ {𝑥}) ∪ {𝑥})) |
| 34 | 13, 14, 15, 18, 22, 25, 28, 30, 33 | gsumsplit2 19947 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (ℂfld
Σg (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦))) = ((ℂfld
Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) + (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦))))) |
| 35 | 7, 12, 34 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝐻‘𝑋) = ((ℂfld
Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) + (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦))))) |
| 36 | 22 | difexd 5331 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝐼 ∖ {𝑥}) ∈ V) |
| 37 | | nn0subm 21440 |
. . . . . . . . . . . . 13
⊢
ℕ0 ∈
(SubMnd‘ℂfld) |
| 38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ℕ0 ∈
(SubMnd‘ℂfld)) |
| 39 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → 𝑋:𝐼⟶ℕ0) |
| 40 | | eldifi 4131 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) → 𝑦 ∈ 𝐼) |
| 41 | | ffvelcdm 7101 |
. . . . . . . . . . . . . 14
⊢ ((𝑋:𝐼⟶ℕ0 ∧ 𝑦 ∈ 𝐼) → (𝑋‘𝑦) ∈
ℕ0) |
| 42 | 39, 40, 41 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) ∧ 𝑦 ∈ (𝐼 ∖ {𝑥})) → (𝑋‘𝑦) ∈
ℕ0) |
| 43 | 42 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)):(𝐼 ∖ {𝑥})⟶ℕ0) |
| 44 | 36 | mptexd 7244 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) ∈ V) |
| 45 | | funmpt 6604 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) |
| 46 | 45 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → Fun (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) |
| 47 | | funmpt 6604 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) |
| 48 | | difss 4136 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∖ {𝑥}) ⊆ 𝐼 |
| 49 | | mptss 6060 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∖ {𝑥}) ⊆ 𝐼 → (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) ⊆ (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦))) |
| 50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) ⊆ (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) |
| 51 | 22 | mptexd 7244 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) ∈ V) |
| 52 | | funsssuppss 8215 |
. . . . . . . . . . . . . 14
⊢ ((Fun
(𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) ∧ (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) ⊆ (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) ∧ (𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) ∈ V) → ((𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) supp 0) ⊆ ((𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) supp 0)) |
| 53 | 47, 50, 51, 52 | mp3an12i 1467 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ((𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) supp 0) ⊆ ((𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) supp 0)) |
| 54 | | fsuppsssupp 9421 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) ∈ V ∧ Fun (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) ∧ ((𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) finSupp 0 ∧ ((𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) supp 0) ⊆ ((𝑦 ∈ 𝐼 ↦ (𝑋‘𝑦)) supp 0))) → (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) finSupp 0) |
| 55 | 44, 46, 28, 53, 54 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦)) finSupp 0) |
| 56 | 14, 18, 36, 38, 43, 55 | gsumsubmcl 19937 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (ℂfld
Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) ∈
ℕ0) |
| 57 | | ringmnd 20240 |
. . . . . . . . . . . . . 14
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
| 58 | 16, 57 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
ℂfld ∈ Mnd |
| 59 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → 𝑥 ∈ 𝐼) |
| 60 | 39, 59 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑋‘𝑥) ∈
ℕ0) |
| 61 | 60 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑋‘𝑥) ∈ ℂ) |
| 62 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (𝑋‘𝑦) = (𝑋‘𝑥)) |
| 63 | 13, 62 | gsumsn 19972 |
. . . . . . . . . . . . 13
⊢
((ℂfld ∈ Mnd ∧ 𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ∈ ℂ) →
(ℂfld Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦))) = (𝑋‘𝑥)) |
| 64 | 58, 59, 61, 63 | mp3an2i 1468 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦))) = (𝑋‘𝑥)) |
| 65 | | elnn0 12528 |
. . . . . . . . . . . . . 14
⊢ ((𝑋‘𝑥) ∈ ℕ0 ↔ ((𝑋‘𝑥) ∈ ℕ ∨ (𝑋‘𝑥) = 0)) |
| 66 | 60, 65 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ((𝑋‘𝑥) ∈ ℕ ∨ (𝑋‘𝑥) = 0)) |
| 67 | | neneq 2946 |
. . . . . . . . . . . . . 14
⊢ ((𝑋‘𝑥) ≠ 0 → ¬ (𝑋‘𝑥) = 0) |
| 68 | 67 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ¬ (𝑋‘𝑥) = 0) |
| 69 | 66, 68 | olcnd 878 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝑋‘𝑥) ∈ ℕ) |
| 70 | 64, 69 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦))) ∈ ℕ) |
| 71 | | nn0nnaddcl 12557 |
. . . . . . . . . . 11
⊢
(((ℂfld Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) ∈ ℕ0 ∧
(ℂfld Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦))) ∈ ℕ) →
((ℂfld Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) + (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦)))) ∈ ℕ) |
| 72 | 56, 70, 71 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ((ℂfld
Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) + (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦)))) ∈ ℕ) |
| 73 | 72 | nnne0d 12316 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → ((ℂfld
Σg (𝑦 ∈ (𝐼 ∖ {𝑥}) ↦ (𝑋‘𝑦))) + (ℂfld
Σg (𝑦 ∈ {𝑥} ↦ (𝑋‘𝑦)))) ≠ 0) |
| 74 | 35, 73 | eqnetrd 3008 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ (𝑥 ∈ 𝐼 ∧ (𝑋‘𝑥) ≠ 0)) → (𝐻‘𝑋) ≠ 0) |
| 75 | 74 | expr 456 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ 𝐼) → ((𝑋‘𝑥) ≠ 0 → (𝐻‘𝑋) ≠ 0)) |
| 76 | 2, 75 | biimtrrid 243 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ 𝐼) → (¬ (𝑋‘𝑥) = 0 → (𝐻‘𝑋) ≠ 0)) |
| 77 | 76 | rexlimdva 3155 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (∃𝑥 ∈ 𝐼 ¬ (𝑋‘𝑥) = 0 → (𝐻‘𝑋) ≠ 0)) |
| 78 | 1, 77 | biimtrrid 243 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (¬ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = 0 → (𝐻‘𝑋) ≠ 0)) |
| 79 | 78 | necon4bd 2960 |
. . 3
⊢ (𝑋 ∈ 𝐴 → ((𝐻‘𝑋) = 0 → ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = 0)) |
| 80 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 81 | | fnconstg 6796 |
. . . . . 6
⊢ (0 ∈
V → (𝐼 × {0}) Fn
𝐼) |
| 82 | 80, 81 | mp1i 13 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝐼 × {0}) Fn 𝐼) |
| 83 | | eqfnfv 7051 |
. . . . 5
⊢ ((𝑋 Fn 𝐼 ∧ (𝐼 × {0}) Fn 𝐼) → (𝑋 = (𝐼 × {0}) ↔ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = ((𝐼 × {0})‘𝑥))) |
| 84 | 20, 82, 83 | syl2anc 584 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (𝑋 = (𝐼 × {0}) ↔ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = ((𝐼 × {0})‘𝑥))) |
| 85 | 80 | fvconst2 7224 |
. . . . . 6
⊢ (𝑥 ∈ 𝐼 → ((𝐼 × {0})‘𝑥) = 0) |
| 86 | 85 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 ∈ 𝐼 → ((𝑋‘𝑥) = ((𝐼 × {0})‘𝑥) ↔ (𝑋‘𝑥) = 0)) |
| 87 | 86 | ralbiia 3091 |
. . . 4
⊢
(∀𝑥 ∈
𝐼 (𝑋‘𝑥) = ((𝐼 × {0})‘𝑥) ↔ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = 0) |
| 88 | 84, 87 | bitrdi 287 |
. . 3
⊢ (𝑋 ∈ 𝐴 → (𝑋 = (𝐼 × {0}) ↔ ∀𝑥 ∈ 𝐼 (𝑋‘𝑥) = 0)) |
| 89 | 79, 88 | sylibrd 259 |
. 2
⊢ (𝑋 ∈ 𝐴 → ((𝐻‘𝑋) = 0 → 𝑋 = (𝐼 × {0}))) |
| 90 | 8 | psrbag0 22086 |
. . . . 5
⊢ (𝐼 ∈ V → (𝐼 × {0}) ∈ 𝐴) |
| 91 | | oveq2 7439 |
. . . . . 6
⊢ (ℎ = (𝐼 × {0}) → (ℂfld
Σg ℎ) = (ℂfld
Σg (𝐼 × {0}))) |
| 92 | | ovex 7464 |
. . . . . 6
⊢
(ℂfld Σg (𝐼 × {0})) ∈ V |
| 93 | 91, 4, 92 | fvmpt 7016 |
. . . . 5
⊢ ((𝐼 × {0}) ∈ 𝐴 → (𝐻‘(𝐼 × {0})) = (ℂfld
Σg (𝐼 × {0}))) |
| 94 | 21, 90, 93 | 3syl 18 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (𝐻‘(𝐼 × {0})) = (ℂfld
Σg (𝐼 × {0}))) |
| 95 | | fconstmpt 5747 |
. . . . . 6
⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0) |
| 96 | 95 | oveq2i 7442 |
. . . . 5
⊢
(ℂfld Σg (𝐼 × {0})) = (ℂfld
Σg (𝑥 ∈ 𝐼 ↦ 0)) |
| 97 | 14 | gsumz 18849 |
. . . . . 6
⊢
((ℂfld ∈ Mnd ∧ 𝐼 ∈ V) → (ℂfld
Σg (𝑥 ∈ 𝐼 ↦ 0)) = 0) |
| 98 | 58, 21, 97 | sylancr 587 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (ℂfld
Σg (𝑥 ∈ 𝐼 ↦ 0)) = 0) |
| 99 | 96, 98 | eqtrid 2789 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (ℂfld
Σg (𝐼 × {0})) = 0) |
| 100 | 94, 99 | eqtrd 2777 |
. . 3
⊢ (𝑋 ∈ 𝐴 → (𝐻‘(𝐼 × {0})) = 0) |
| 101 | | fveqeq2 6915 |
. . 3
⊢ (𝑋 = (𝐼 × {0}) → ((𝐻‘𝑋) = 0 ↔ (𝐻‘(𝐼 × {0})) = 0)) |
| 102 | 100, 101 | syl5ibrcom 247 |
. 2
⊢ (𝑋 ∈ 𝐴 → (𝑋 = (𝐼 × {0}) → (𝐻‘𝑋) = 0)) |
| 103 | 89, 102 | impbid 212 |
1
⊢ (𝑋 ∈ 𝐴 → ((𝐻‘𝑋) = 0 ↔ 𝑋 = (𝐼 × {0}))) |