MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  incexclem Structured version   Visualization version   GIF version

Theorem incexclem 14612
Description: Lemma for incexc 14613. (Contributed by Mario Carneiro, 7-Aug-2017.)
Assertion
Ref Expression
incexclem ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
Distinct variable groups:   𝐴,𝑠   𝐵,𝑠

Proof of Theorem incexclem
Dummy variables 𝑏 𝑡 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4476 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
2 uni0 4497 . . . . . . . . . . 11 ∅ = ∅
31, 2syl6eq 2701 . . . . . . . . . 10 (𝑥 = ∅ → 𝑥 = ∅)
43ineq2d 3847 . . . . . . . . 9 (𝑥 = ∅ → (𝑏 𝑥) = (𝑏 ∩ ∅))
5 in0 4001 . . . . . . . . 9 (𝑏 ∩ ∅) = ∅
64, 5syl6eq 2701 . . . . . . . 8 (𝑥 = ∅ → (𝑏 𝑥) = ∅)
76fveq2d 6233 . . . . . . 7 (𝑥 = ∅ → (#‘(𝑏 𝑥)) = (#‘∅))
8 hash0 13196 . . . . . . 7 (#‘∅) = 0
97, 8syl6eq 2701 . . . . . 6 (𝑥 = ∅ → (#‘(𝑏 𝑥)) = 0)
109oveq2d 6706 . . . . 5 (𝑥 = ∅ → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − 0))
11 pweq 4194 . . . . . . 7 (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12 pw0 4375 . . . . . . 7 𝒫 ∅ = {∅}
1311, 12syl6eq 2701 . . . . . 6 (𝑥 = ∅ → 𝒫 𝑥 = {∅})
1413sumeq1d 14475 . . . . 5 (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
1510, 14eqeq12d 2666 . . . 4 (𝑥 = ∅ → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
1615ralbidv 3015 . . 3 (𝑥 = ∅ → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
17 unieq 4476 . . . . . . . 8 (𝑥 = 𝑦 𝑥 = 𝑦)
1817ineq2d 3847 . . . . . . 7 (𝑥 = 𝑦 → (𝑏 𝑥) = (𝑏 𝑦))
1918fveq2d 6233 . . . . . 6 (𝑥 = 𝑦 → (#‘(𝑏 𝑥)) = (#‘(𝑏 𝑦)))
2019oveq2d 6706 . . . . 5 (𝑥 = 𝑦 → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − (#‘(𝑏 𝑦))))
21 pweq 4194 . . . . . 6 (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
2221sumeq1d 14475 . . . . 5 (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
2320, 22eqeq12d 2666 . . . 4 (𝑥 = 𝑦 → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
2423ralbidv 3015 . . 3 (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
25 unieq 4476 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧}))
26 uniun 4488 . . . . . . . . . 10 (𝑦 ∪ {𝑧}) = ( 𝑦 {𝑧})
27 vex 3234 . . . . . . . . . . . 12 𝑧 ∈ V
2827unisn 4483 . . . . . . . . . . 11 {𝑧} = 𝑧
2928uneq2i 3797 . . . . . . . . . 10 ( 𝑦 {𝑧}) = ( 𝑦𝑧)
3026, 29eqtri 2673 . . . . . . . . 9 (𝑦 ∪ {𝑧}) = ( 𝑦𝑧)
3125, 30syl6eq 2701 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = ( 𝑦𝑧))
3231ineq2d 3847 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 𝑥) = (𝑏 ∩ ( 𝑦𝑧)))
3332fveq2d 6233 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑏 𝑥)) = (#‘(𝑏 ∩ ( 𝑦𝑧))))
3433oveq2d 6706 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))))
35 pweq 4194 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
3635sumeq1d 14475 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
3734, 36eqeq12d 2666 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
3837ralbidv 3015 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
39 unieq 4476 . . . . . . . 8 (𝑥 = 𝐴 𝑥 = 𝐴)
4039ineq2d 3847 . . . . . . 7 (𝑥 = 𝐴 → (𝑏 𝑥) = (𝑏 𝐴))
4140fveq2d 6233 . . . . . 6 (𝑥 = 𝐴 → (#‘(𝑏 𝑥)) = (#‘(𝑏 𝐴)))
4241oveq2d 6706 . . . . 5 (𝑥 = 𝐴 → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − (#‘(𝑏 𝐴))))
43 pweq 4194 . . . . . 6 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
4443sumeq1d 14475 . . . . 5 (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
4542, 44eqeq12d 2666 . . . 4 (𝑥 = 𝐴 → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
4645ralbidv 3015 . . 3 (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
47 hashcl 13185 . . . . . . 7 (𝑏 ∈ Fin → (#‘𝑏) ∈ ℕ0)
4847nn0cnd 11391 . . . . . 6 (𝑏 ∈ Fin → (#‘𝑏) ∈ ℂ)
4948mulid2d 10096 . . . . 5 (𝑏 ∈ Fin → (1 · (#‘𝑏)) = (#‘𝑏))
50 0ex 4823 . . . . . 6 ∅ ∈ V
5149, 48eqeltrd 2730 . . . . . 6 (𝑏 ∈ Fin → (1 · (#‘𝑏)) ∈ ℂ)
52 fveq2 6229 . . . . . . . . . . 11 (𝑠 = ∅ → (#‘𝑠) = (#‘∅))
5352, 8syl6eq 2701 . . . . . . . . . 10 (𝑠 = ∅ → (#‘𝑠) = 0)
5453oveq2d 6706 . . . . . . . . 9 (𝑠 = ∅ → (-1↑(#‘𝑠)) = (-1↑0))
55 neg1cn 11162 . . . . . . . . . 10 -1 ∈ ℂ
56 exp0 12904 . . . . . . . . . 10 (-1 ∈ ℂ → (-1↑0) = 1)
5755, 56ax-mp 5 . . . . . . . . 9 (-1↑0) = 1
5854, 57syl6eq 2701 . . . . . . . 8 (𝑠 = ∅ → (-1↑(#‘𝑠)) = 1)
59 rint0 4549 . . . . . . . . 9 (𝑠 = ∅ → (𝑏 𝑠) = 𝑏)
6059fveq2d 6233 . . . . . . . 8 (𝑠 = ∅ → (#‘(𝑏 𝑠)) = (#‘𝑏))
6158, 60oveq12d 6708 . . . . . . 7 (𝑠 = ∅ → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = (1 · (#‘𝑏)))
6261sumsn 14519 . . . . . 6 ((∅ ∈ V ∧ (1 · (#‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = (1 · (#‘𝑏)))
6350, 51, 62sylancr 696 . . . . 5 (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = (1 · (#‘𝑏)))
6448subid1d 10419 . . . . 5 (𝑏 ∈ Fin → ((#‘𝑏) − 0) = (#‘𝑏))
6549, 63, 643eqtr4rd 2696 . . . 4 (𝑏 ∈ Fin → ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
6665rgen 2951 . . 3 𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))
67 fveq2 6229 . . . . . . . . . . . 12 (𝑏 = 𝑥 → (#‘𝑏) = (#‘𝑥))
68 ineq1 3840 . . . . . . . . . . . . 13 (𝑏 = 𝑥 → (𝑏 𝑦) = (𝑥 𝑦))
6968fveq2d 6233 . . . . . . . . . . . 12 (𝑏 = 𝑥 → (#‘(𝑏 𝑦)) = (#‘(𝑥 𝑦)))
7067, 69oveq12d 6708 . . . . . . . . . . 11 (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 𝑦))) = ((#‘𝑥) − (#‘(𝑥 𝑦))))
71 simpl 472 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
7271ineq1d 3846 . . . . . . . . . . . . . 14 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → (𝑏 𝑠) = (𝑥 𝑠))
7372fveq2d 6233 . . . . . . . . . . . . 13 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → (#‘(𝑏 𝑠)) = (#‘(𝑥 𝑠)))
7473oveq2d 6706 . . . . . . . . . . . 12 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
7574sumeq2dv 14477 . . . . . . . . . . 11 (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
7670, 75eqeq12d 2666 . . . . . . . . . 10 (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
7776rspcva 3338 . . . . . . . . 9 ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
7877adantll 750 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
79 simpr 476 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
80 inss1 3866 . . . . . . . . . 10 (𝑥𝑧) ⊆ 𝑥
81 ssfi 8221 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ (𝑥𝑧) ⊆ 𝑥) → (𝑥𝑧) ∈ Fin)
8279, 80, 81sylancl 695 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑥𝑧) ∈ Fin)
83 fveq2 6229 . . . . . . . . . . . 12 (𝑏 = (𝑥𝑧) → (#‘𝑏) = (#‘(𝑥𝑧)))
84 ineq1 3840 . . . . . . . . . . . . . 14 (𝑏 = (𝑥𝑧) → (𝑏 𝑦) = ((𝑥𝑧) ∩ 𝑦))
85 in32 3858 . . . . . . . . . . . . . . 15 ((𝑥𝑧) ∩ 𝑦) = ((𝑥 𝑦) ∩ 𝑧)
86 inass 3856 . . . . . . . . . . . . . . 15 ((𝑥 𝑦) ∩ 𝑧) = (𝑥 ∩ ( 𝑦𝑧))
8785, 86eqtri 2673 . . . . . . . . . . . . . 14 ((𝑥𝑧) ∩ 𝑦) = (𝑥 ∩ ( 𝑦𝑧))
8884, 87syl6eq 2701 . . . . . . . . . . . . 13 (𝑏 = (𝑥𝑧) → (𝑏 𝑦) = (𝑥 ∩ ( 𝑦𝑧)))
8988fveq2d 6233 . . . . . . . . . . . 12 (𝑏 = (𝑥𝑧) → (#‘(𝑏 𝑦)) = (#‘(𝑥 ∩ ( 𝑦𝑧))))
9083, 89oveq12d 6708 . . . . . . . . . . 11 (𝑏 = (𝑥𝑧) → ((#‘𝑏) − (#‘(𝑏 𝑦))) = ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))
91 ineq1 3840 . . . . . . . . . . . . . . 15 (𝑏 = (𝑥𝑧) → (𝑏 𝑠) = ((𝑥𝑧) ∩ 𝑠))
92 in32 3858 . . . . . . . . . . . . . . . 16 ((𝑥𝑧) ∩ 𝑠) = ((𝑥 𝑠) ∩ 𝑧)
93 inass 3856 . . . . . . . . . . . . . . . 16 ((𝑥 𝑠) ∩ 𝑧) = (𝑥 ∩ ( 𝑠𝑧))
9492, 93eqtri 2673 . . . . . . . . . . . . . . 15 ((𝑥𝑧) ∩ 𝑠) = (𝑥 ∩ ( 𝑠𝑧))
9591, 94syl6eq 2701 . . . . . . . . . . . . . 14 (𝑏 = (𝑥𝑧) → (𝑏 𝑠) = (𝑥 ∩ ( 𝑠𝑧)))
9695fveq2d 6233 . . . . . . . . . . . . 13 (𝑏 = (𝑥𝑧) → (#‘(𝑏 𝑠)) = (#‘(𝑥 ∩ ( 𝑠𝑧))))
9796oveq2d 6706 . . . . . . . . . . . 12 (𝑏 = (𝑥𝑧) → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
9897sumeq2sdv 14479 . . . . . . . . . . 11 (𝑏 = (𝑥𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
9990, 98eqeq12d 2666 . . . . . . . . . 10 (𝑏 = (𝑥𝑧) → (((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
10099rspcva 3338 . . . . . . . . 9 (((𝑥𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
10182, 100sylan 487 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
10278, 101oveq12d 6708 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
103 inss1 3866 . . . . . . . . . . . . . 14 (𝑥 𝑦) ⊆ 𝑥
104 ssfi 8221 . . . . . . . . . . . . . 14 ((𝑥 ∈ Fin ∧ (𝑥 𝑦) ⊆ 𝑥) → (𝑥 𝑦) ∈ Fin)
10579, 103, 104sylancl 695 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 𝑦) ∈ Fin)
106 hashun3 13211 . . . . . . . . . . . . 13 (((𝑥 𝑦) ∈ Fin ∧ (𝑥𝑧) ∈ Fin) → (#‘((𝑥 𝑦) ∪ (𝑥𝑧))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘((𝑥 𝑦) ∩ (𝑥𝑧)))))
107105, 82, 106syl2anc 694 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘((𝑥 𝑦) ∪ (𝑥𝑧))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘((𝑥 𝑦) ∩ (𝑥𝑧)))))
108 indi 3906 . . . . . . . . . . . . 13 (𝑥 ∩ ( 𝑦𝑧)) = ((𝑥 𝑦) ∪ (𝑥𝑧))
109108fveq2i 6232 . . . . . . . . . . . 12 (#‘(𝑥 ∩ ( 𝑦𝑧))) = (#‘((𝑥 𝑦) ∪ (𝑥𝑧)))
110 inindi 3863 . . . . . . . . . . . . . 14 (𝑥 ∩ ( 𝑦𝑧)) = ((𝑥 𝑦) ∩ (𝑥𝑧))
111110fveq2i 6232 . . . . . . . . . . . . 13 (#‘(𝑥 ∩ ( 𝑦𝑧))) = (#‘((𝑥 𝑦) ∩ (𝑥𝑧)))
112111oveq2i 6701 . . . . . . . . . . . 12 (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘((𝑥 𝑦) ∩ (𝑥𝑧))))
113107, 109, 1123eqtr4g 2710 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))
114 hashcl 13185 . . . . . . . . . . . . . 14 ((𝑥 𝑦) ∈ Fin → (#‘(𝑥 𝑦)) ∈ ℕ0)
115105, 114syl 17 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 𝑦)) ∈ ℕ0)
116115nn0cnd 11391 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 𝑦)) ∈ ℂ)
117 hashcl 13185 . . . . . . . . . . . . . 14 ((𝑥𝑧) ∈ Fin → (#‘(𝑥𝑧)) ∈ ℕ0)
11882, 117syl 17 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥𝑧)) ∈ ℕ0)
119118nn0cnd 11391 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥𝑧)) ∈ ℂ)
120 inss1 3866 . . . . . . . . . . . . . . 15 (𝑥 ∩ ( 𝑦𝑧)) ⊆ 𝑥
121 ssfi 8221 . . . . . . . . . . . . . . 15 ((𝑥 ∈ Fin ∧ (𝑥 ∩ ( 𝑦𝑧)) ⊆ 𝑥) → (𝑥 ∩ ( 𝑦𝑧)) ∈ Fin)
12279, 120, 121sylancl 695 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ( 𝑦𝑧)) ∈ Fin)
123 hashcl 13185 . . . . . . . . . . . . . 14 ((𝑥 ∩ ( 𝑦𝑧)) ∈ Fin → (#‘(𝑥 ∩ ( 𝑦𝑧))) ∈ ℕ0)
124122, 123syl 17 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) ∈ ℕ0)
125124nn0cnd 11391 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) ∈ ℂ)
126116, 119, 125addsubassd 10450 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
127113, 126eqtrd 2685 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) = ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
128127oveq2d 6706 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = ((#‘𝑥) − ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))))
129 hashcl 13185 . . . . . . . . . . . 12 (𝑥 ∈ Fin → (#‘𝑥) ∈ ℕ0)
130129adantl 481 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℕ0)
131130nn0cnd 11391 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℂ)
132119, 125subcld 10430 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) ∈ ℂ)
133131, 116, 132subsub4d 10461 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))) = ((#‘𝑥) − ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))))
134128, 133eqtr4d 2688 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
135134adantr 480 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
136 disjdif 4073 . . . . . . . . . . 11 (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
137136a1i 11 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
138 ssun1 3809 . . . . . . . . . . . . . 14 𝑦 ⊆ (𝑦 ∪ {𝑧})
139 sspwb 4947 . . . . . . . . . . . . . 14 (𝑦 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
140138, 139mpbi 220 . . . . . . . . . . . . 13 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
141 undif 4082 . . . . . . . . . . . . 13 (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
142140, 141mpbi 220 . . . . . . . . . . . 12 (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
143142eqcomi 2660 . . . . . . . . . . 11 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
144143a1i 11 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
145 simpll 805 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
146 snfi 8079 . . . . . . . . . . . 12 {𝑧} ∈ Fin
147 unfi 8268 . . . . . . . . . . . 12 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
148145, 146, 147sylancl 695 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
149 pwfi 8302 . . . . . . . . . . 11 ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
150148, 149sylib 208 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
15155a1i 11 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
152 elpwi 4201 . . . . . . . . . . . . . 14 (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
153 ssfi 8221 . . . . . . . . . . . . . 14 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
154148, 152, 153syl2an 493 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
155 hashcl 13185 . . . . . . . . . . . . 13 (𝑠 ∈ Fin → (#‘𝑠) ∈ ℕ0)
156154, 155syl 17 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘𝑠) ∈ ℕ0)
157151, 156expcld 13048 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(#‘𝑠)) ∈ ℂ)
158 simplr 807 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
159 inss1 3866 . . . . . . . . . . . . . 14 (𝑥 𝑠) ⊆ 𝑥
160 ssfi 8221 . . . . . . . . . . . . . 14 ((𝑥 ∈ Fin ∧ (𝑥 𝑠) ⊆ 𝑥) → (𝑥 𝑠) ∈ Fin)
161158, 159, 160sylancl 695 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 𝑠) ∈ Fin)
162 hashcl 13185 . . . . . . . . . . . . 13 ((𝑥 𝑠) ∈ Fin → (#‘(𝑥 𝑠)) ∈ ℕ0)
163161, 162syl 17 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 𝑠)) ∈ ℕ0)
164163nn0cnd 11391 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 𝑠)) ∈ ℂ)
165157, 164mulcld 10098 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
166137, 144, 150, 165fsumsplit 14515 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
167 fveq2 6229 . . . . . . . . . . . . . 14 (𝑠 = (𝑡 ∪ {𝑧}) → (#‘𝑠) = (#‘(𝑡 ∪ {𝑧})))
168167oveq2d 6706 . . . . . . . . . . . . 13 (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(#‘𝑠)) = (-1↑(#‘(𝑡 ∪ {𝑧}))))
169 inteq 4510 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑡 ∪ {𝑧}) → 𝑠 = (𝑡 ∪ {𝑧}))
17027intunsn 4548 . . . . . . . . . . . . . . . 16 (𝑡 ∪ {𝑧}) = ( 𝑡𝑧)
171169, 170syl6eq 2701 . . . . . . . . . . . . . . 15 (𝑠 = (𝑡 ∪ {𝑧}) → 𝑠 = ( 𝑡𝑧))
172171ineq2d 3847 . . . . . . . . . . . . . 14 (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 𝑠) = (𝑥 ∩ ( 𝑡𝑧)))
173172fveq2d 6233 . . . . . . . . . . . . 13 (𝑠 = (𝑡 ∪ {𝑧}) → (#‘(𝑥 𝑠)) = (#‘(𝑥 ∩ ( 𝑡𝑧))))
174168, 173oveq12d 6708 . . . . . . . . . . . 12 (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))))
175 pwfi 8302 . . . . . . . . . . . . 13 (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
176145, 175sylib 208 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
177 eqid 2651 . . . . . . . . . . . . 13 (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
178 elpwi 4201 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ 𝒫 𝑦𝑢𝑦)
179178adantl 481 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢𝑦)
180 unss1 3815 . . . . . . . . . . . . . . . 16 (𝑢𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
181179, 180syl 17 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
182 vex 3234 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
183 snex 4938 . . . . . . . . . . . . . . . . 17 {𝑧} ∈ V
184182, 183unex 6998 . . . . . . . . . . . . . . . 16 (𝑢 ∪ {𝑧}) ∈ V
185184elpw 4197 . . . . . . . . . . . . . . 15 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
186181, 185sylibr 224 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
187 simpllr 815 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧𝑦)
188 elpwi 4201 . . . . . . . . . . . . . . . 16 ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
189 ssun2 3810 . . . . . . . . . . . . . . . . . 18 {𝑧} ⊆ (𝑢 ∪ {𝑧})
19027snss 4348 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
191189, 190mpbir 221 . . . . . . . . . . . . . . . . 17 𝑧 ∈ (𝑢 ∪ {𝑧})
192191a1i 11 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
193 ssel 3630 . . . . . . . . . . . . . . . 16 ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧𝑦))
194188, 192, 193syl2imc 41 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦𝑧𝑦))
195187, 194mtod 189 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
196186, 195eldifd 3618 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
197 eldifi 3765 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
198197adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
199198elpwid 4203 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
200 uncom 3790 . . . . . . . . . . . . . . . 16 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
201199, 200syl6sseq 3684 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
202 ssundif 4085 . . . . . . . . . . . . . . 15 (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
203201, 202sylib 208 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204 vex 3234 . . . . . . . . . . . . . . 15 𝑦 ∈ V
205204elpw2 4858 . . . . . . . . . . . . . 14 ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
206203, 205sylibr 224 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
207 elpwunsn 4256 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧𝑠)
208207ad2antll 765 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧𝑠)
209208snssd 4372 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
210 ssequn2 3819 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
211209, 210sylib 208 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
212211eqcomd 2657 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
213 uneq1 3793 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
214 undif1 4076 . . . . . . . . . . . . . . . . 17 ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
215213, 214syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
216215eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
217212, 216syl5ibrcom 237 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
218178ad2antrl 764 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢𝑦)
219 simpllr 815 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧𝑦)
220218, 219ssneldd 3639 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧𝑢)
221 difsnb 4369 . . . . . . . . . . . . . . . . 17 𝑧𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
222220, 221sylib 208 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
223222eqcomd 2657 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
224 difeq1 3754 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
225 difun2 4081 . . . . . . . . . . . . . . . . 17 ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
226224, 225syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
227226eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
228223, 227syl5ibrcom 237 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
229217, 228impbid 202 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
230177, 196, 206, 229f1o2d 6929 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
231 uneq1 3793 . . . . . . . . . . . . . 14 (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
232 vex 3234 . . . . . . . . . . . . . . 15 𝑡 ∈ V
233232, 183unex 6998 . . . . . . . . . . . . . 14 (𝑡 ∪ {𝑧}) ∈ V
234231, 177, 233fvmpt 6321 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
235234adantl 481 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
236197, 165sylan2 490 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
237174, 176, 230, 235, 236fsumf1o 14498 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))))
238 uneq1 3793 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
239238fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑡 = 𝑠 → (#‘(𝑡 ∪ {𝑧})) = (#‘(𝑠 ∪ {𝑧})))
240239oveq2d 6706 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (-1↑(#‘(𝑡 ∪ {𝑧}))) = (-1↑(#‘(𝑠 ∪ {𝑧}))))
241 inteq 4510 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑠 𝑡 = 𝑠)
242241ineq1d 3846 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑠 → ( 𝑡𝑧) = ( 𝑠𝑧))
243242ineq2d 3847 . . . . . . . . . . . . . . 15 (𝑡 = 𝑠 → (𝑥 ∩ ( 𝑡𝑧)) = (𝑥 ∩ ( 𝑠𝑧)))
244243fveq2d 6233 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (#‘(𝑥 ∩ ( 𝑡𝑧))) = (#‘(𝑥 ∩ ( 𝑠𝑧))))
245240, 244oveq12d 6708 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))) = ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
246245cbvsumv 14470 . . . . . . . . . . . 12 Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧))))
24755a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
248 elpwi 4201 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ 𝒫 𝑦𝑠𝑦)
249 ssfi 8221 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ Fin ∧ 𝑠𝑦) → 𝑠 ∈ Fin)
250145, 248, 249syl2an 493 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
251250, 155syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘𝑠) ∈ ℕ0)
252247, 251expp1d 13049 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((#‘𝑠) + 1)) = ((-1↑(#‘𝑠)) · -1))
253248adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠𝑦)
254 simpllr 815 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧𝑦)
255253, 254ssneldd 3639 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧𝑠)
256 hashunsng 13219 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1)))
25727, 256ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ Fin ∧ ¬ 𝑧𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
258250, 255, 257syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
259258oveq2d 6706 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1↑((#‘𝑠) + 1)))
260140sseli 3632 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ 𝒫 𝑦𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
261260, 157sylan2 490 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘𝑠)) ∈ ℂ)
262247, 261mulcomd 10099 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = ((-1↑(#‘𝑠)) · -1))
263252, 259, 2623eqtr4d 2695 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1 · (-1↑(#‘𝑠))))
264261mulm1d 10520 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = -(-1↑(#‘𝑠)))
265263, 264eqtrd 2685 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = -(-1↑(#‘𝑠)))
266265oveq1d 6705 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
267 inss1 3866 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝑠𝑧)) ⊆ 𝑥
268 ssfi 8221 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ Fin ∧ (𝑥 ∩ ( 𝑠𝑧)) ⊆ 𝑥) → (𝑥 ∩ ( 𝑠𝑧)) ∈ Fin)
269158, 267, 268sylancl 695 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ( 𝑠𝑧)) ∈ Fin)
270 hashcl 13185 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∩ ( 𝑠𝑧)) ∈ Fin → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℕ0)
271269, 270syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℕ0)
272271nn0cnd 11391 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℂ)
273260, 272sylan2 490 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℂ)
274261, 273mulneg1d 10521 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
275266, 274eqtrd 2685 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
276275sumeq2dv 14477 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
277246, 276syl5eq 2697 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
278157, 272mulcld 10098 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
279260, 278sylan2 490 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
280176, 279fsumneg 14563 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
281237, 277, 2803eqtrd 2689 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
282281oveq2d 6706 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
283140a1i 11 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
284283sselda 3636 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
285284, 165syldan 486 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
286176, 285fsumcl 14508 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
287284, 278syldan 486 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
288176, 287fsumcl 14508 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
289286, 288negsubd 10436 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
290166, 282, 2893eqtrd 2689 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
291290adantr 480 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
292102, 135, 2913eqtr4d 2695 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
293292ex 449 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
294293ralrimdva 2998 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) → ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
295 ineq1 3840 . . . . . . . 8 (𝑏 = 𝑥 → (𝑏 ∩ ( 𝑦𝑧)) = (𝑥 ∩ ( 𝑦𝑧)))
296295fveq2d 6233 . . . . . . 7 (𝑏 = 𝑥 → (#‘(𝑏 ∩ ( 𝑦𝑧))) = (#‘(𝑥 ∩ ( 𝑦𝑧))))
29767, 296oveq12d 6708 . . . . . 6 (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))
298 ineq1 3840 . . . . . . . . 9 (𝑏 = 𝑥 → (𝑏 𝑠) = (𝑥 𝑠))
299298fveq2d 6233 . . . . . . . 8 (𝑏 = 𝑥 → (#‘(𝑏 𝑠)) = (#‘(𝑥 𝑠)))
300299oveq2d 6706 . . . . . . 7 (𝑏 = 𝑥 → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
301300sumeq2sdv 14479 . . . . . 6 (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
302297, 301eqeq12d 2666 . . . . 5 (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
303302cbvralv 3201 . . . 4 (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
304294, 303syl6ibr 242 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
30516, 24, 38, 46, 66, 304findcard2s 8242 . 2 (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
306 fveq2 6229 . . . . 5 (𝑏 = 𝐵 → (#‘𝑏) = (#‘𝐵))
307 ineq1 3840 . . . . . 6 (𝑏 = 𝐵 → (𝑏 𝐴) = (𝐵 𝐴))
308307fveq2d 6233 . . . . 5 (𝑏 = 𝐵 → (#‘(𝑏 𝐴)) = (#‘(𝐵 𝐴)))
309306, 308oveq12d 6708 . . . 4 (𝑏 = 𝐵 → ((#‘𝑏) − (#‘(𝑏 𝐴))) = ((#‘𝐵) − (#‘(𝐵 𝐴))))
310 simpl 472 . . . . . . . 8 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
311310ineq1d 3846 . . . . . . 7 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → (𝑏 𝑠) = (𝐵 𝑠))
312311fveq2d 6233 . . . . . 6 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → (#‘(𝑏 𝑠)) = (#‘(𝐵 𝑠)))
313312oveq2d 6706 . . . . 5 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
314313sumeq2dv 14477 . . . 4 (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
315309, 314eqeq12d 2666 . . 3 (𝑏 = 𝐵 → (((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠)))))
316315rspccva 3339 . 2 ((∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
317305, 316sylan 487 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1523  wcel 2030  wral 2941  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   cuni 4468   cint 4507  cmpt 4762  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  cmin 10304  -cneg 10305  0cn0 11330  cexp 12900  #chash 13157  Σcsu 14460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461
This theorem is referenced by:  incexc  14613
  Copyright terms: Public domain W3C validator