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

Theorem incexclem 14276
Description: Lemma for incexc 14277. (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 4278 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
2 uni0 4299 . . . . . . . . . . 11 ∅ = ∅
31, 2syl6eq 2564 . . . . . . . . . 10 (𝑥 = ∅ → 𝑥 = ∅)
43ineq2d 3679 . . . . . . . . 9 (𝑥 = ∅ → (𝑏 𝑥) = (𝑏 ∩ ∅))
5 in0 3823 . . . . . . . . 9 (𝑏 ∩ ∅) = ∅
64, 5syl6eq 2564 . . . . . . . 8 (𝑥 = ∅ → (𝑏 𝑥) = ∅)
76fveq2d 5991 . . . . . . 7 (𝑥 = ∅ → (#‘(𝑏 𝑥)) = (#‘∅))
8 hash0 12884 . . . . . . 7 (#‘∅) = 0
97, 8syl6eq 2564 . . . . . 6 (𝑥 = ∅ → (#‘(𝑏 𝑥)) = 0)
109oveq2d 6442 . . . . 5 (𝑥 = ∅ → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − 0))
11 pweq 4014 . . . . . . 7 (𝑥 = ∅ → 𝒫 𝑥 = 𝒫 ∅)
12 pw0 4186 . . . . . . 7 𝒫 ∅ = {∅}
1311, 12syl6eq 2564 . . . . . 6 (𝑥 = ∅ → 𝒫 𝑥 = {∅})
1413sumeq1d 14148 . . . . 5 (𝑥 = ∅ → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
1510, 14eqeq12d 2529 . . . 4 (𝑥 = ∅ → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
1615ralbidv 2873 . . 3 (𝑥 = ∅ → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
17 unieq 4278 . . . . . . . 8 (𝑥 = 𝑦 𝑥 = 𝑦)
1817ineq2d 3679 . . . . . . 7 (𝑥 = 𝑦 → (𝑏 𝑥) = (𝑏 𝑦))
1918fveq2d 5991 . . . . . 6 (𝑥 = 𝑦 → (#‘(𝑏 𝑥)) = (#‘(𝑏 𝑦)))
2019oveq2d 6442 . . . . 5 (𝑥 = 𝑦 → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − (#‘(𝑏 𝑦))))
21 pweq 4014 . . . . . 6 (𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 𝑦)
2221sumeq1d 14148 . . . . 5 (𝑥 = 𝑦 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
2320, 22eqeq12d 2529 . . . 4 (𝑥 = 𝑦 → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
2423ralbidv 2873 . . 3 (𝑥 = 𝑦 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
25 unieq 4278 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧}))
26 uniun 4290 . . . . . . . . . 10 (𝑦 ∪ {𝑧}) = ( 𝑦 {𝑧})
27 vex 3080 . . . . . . . . . . . 12 𝑧 ∈ V
2827unisn 4285 . . . . . . . . . . 11 {𝑧} = 𝑧
2928uneq2i 3630 . . . . . . . . . 10 ( 𝑦 {𝑧}) = ( 𝑦𝑧)
3026, 29eqtri 2536 . . . . . . . . 9 (𝑦 ∪ {𝑧}) = ( 𝑦𝑧)
3125, 30syl6eq 2564 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = ( 𝑦𝑧))
3231ineq2d 3679 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑏 𝑥) = (𝑏 ∩ ( 𝑦𝑧)))
3332fveq2d 5991 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (#‘(𝑏 𝑥)) = (#‘(𝑏 ∩ ( 𝑦𝑧))))
3433oveq2d 6442 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))))
35 pweq 4014 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → 𝒫 𝑥 = 𝒫 (𝑦 ∪ {𝑧}))
3635sumeq1d 14148 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
3734, 36eqeq12d 2529 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
3837ralbidv 2873 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
39 unieq 4278 . . . . . . . 8 (𝑥 = 𝐴 𝑥 = 𝐴)
4039ineq2d 3679 . . . . . . 7 (𝑥 = 𝐴 → (𝑏 𝑥) = (𝑏 𝐴))
4140fveq2d 5991 . . . . . 6 (𝑥 = 𝐴 → (#‘(𝑏 𝑥)) = (#‘(𝑏 𝐴)))
4241oveq2d 6442 . . . . 5 (𝑥 = 𝐴 → ((#‘𝑏) − (#‘(𝑏 𝑥))) = ((#‘𝑏) − (#‘(𝑏 𝐴))))
43 pweq 4014 . . . . . 6 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
4443sumeq1d 14148 . . . . 5 (𝑥 = 𝐴 → Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
4542, 44eqeq12d 2529 . . . 4 (𝑥 = 𝐴 → (((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
4645ralbidv 2873 . . 3 (𝑥 = 𝐴 → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑥))) = Σ𝑠 ∈ 𝒫 𝑥((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
47 hashcl 12874 . . . . . . 7 (𝑏 ∈ Fin → (#‘𝑏) ∈ ℕ0)
4847nn0cnd 11108 . . . . . 6 (𝑏 ∈ Fin → (#‘𝑏) ∈ ℂ)
4948mulid2d 9813 . . . . 5 (𝑏 ∈ Fin → (1 · (#‘𝑏)) = (#‘𝑏))
50 0ex 4617 . . . . . 6 ∅ ∈ V
5149, 48eqeltrd 2592 . . . . . 6 (𝑏 ∈ Fin → (1 · (#‘𝑏)) ∈ ℂ)
52 fveq2 5987 . . . . . . . . . . 11 (𝑠 = ∅ → (#‘𝑠) = (#‘∅))
5352, 8syl6eq 2564 . . . . . . . . . 10 (𝑠 = ∅ → (#‘𝑠) = 0)
5453oveq2d 6442 . . . . . . . . 9 (𝑠 = ∅ → (-1↑(#‘𝑠)) = (-1↑0))
55 neg1cn 10879 . . . . . . . . . 10 -1 ∈ ℂ
56 exp0 12594 . . . . . . . . . 10 (-1 ∈ ℂ → (-1↑0) = 1)
5755, 56ax-mp 5 . . . . . . . . 9 (-1↑0) = 1
5854, 57syl6eq 2564 . . . . . . . 8 (𝑠 = ∅ → (-1↑(#‘𝑠)) = 1)
59 rint0 4350 . . . . . . . . 9 (𝑠 = ∅ → (𝑏 𝑠) = 𝑏)
6059fveq2d 5991 . . . . . . . 8 (𝑠 = ∅ → (#‘(𝑏 𝑠)) = (#‘𝑏))
6158, 60oveq12d 6444 . . . . . . 7 (𝑠 = ∅ → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = (1 · (#‘𝑏)))
6261sumsn 14188 . . . . . 6 ((∅ ∈ V ∧ (1 · (#‘𝑏)) ∈ ℂ) → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = (1 · (#‘𝑏)))
6350, 51, 62sylancr 693 . . . . 5 (𝑏 ∈ Fin → Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = (1 · (#‘𝑏)))
6448subid1d 10132 . . . . 5 (𝑏 ∈ Fin → ((#‘𝑏) − 0) = (#‘𝑏))
6549, 63, 643eqtr4rd 2559 . . . 4 (𝑏 ∈ Fin → ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
6665rgen 2810 . . 3 𝑏 ∈ Fin ((#‘𝑏) − 0) = Σ𝑠 ∈ {∅} ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))
67 fveq2 5987 . . . . . . . . . . . 12 (𝑏 = 𝑥 → (#‘𝑏) = (#‘𝑥))
68 ineq1 3672 . . . . . . . . . . . . 13 (𝑏 = 𝑥 → (𝑏 𝑦) = (𝑥 𝑦))
6968fveq2d 5991 . . . . . . . . . . . 12 (𝑏 = 𝑥 → (#‘(𝑏 𝑦)) = (#‘(𝑥 𝑦)))
7067, 69oveq12d 6444 . . . . . . . . . . 11 (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 𝑦))) = ((#‘𝑥) − (#‘(𝑥 𝑦))))
71 simpl 471 . . . . . . . . . . . . . . 15 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → 𝑏 = 𝑥)
7271ineq1d 3678 . . . . . . . . . . . . . 14 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → (𝑏 𝑠) = (𝑥 𝑠))
7372fveq2d 5991 . . . . . . . . . . . . 13 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → (#‘(𝑏 𝑠)) = (#‘(𝑥 𝑠)))
7473oveq2d 6442 . . . . . . . . . . . 12 ((𝑏 = 𝑥𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
7574sumeq2dv 14150 . . . . . . . . . . 11 (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
7670, 75eqeq12d 2529 . . . . . . . . . 10 (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
7776rspcva 3184 . . . . . . . . 9 ((𝑥 ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
7877adantll 745 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
79 simpr 475 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
80 inss1 3698 . . . . . . . . . 10 (𝑥𝑧) ⊆ 𝑥
81 ssfi 7941 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ (𝑥𝑧) ⊆ 𝑥) → (𝑥𝑧) ∈ Fin)
8279, 80, 81sylancl 692 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑥𝑧) ∈ Fin)
83 fveq2 5987 . . . . . . . . . . . 12 (𝑏 = (𝑥𝑧) → (#‘𝑏) = (#‘(𝑥𝑧)))
84 ineq1 3672 . . . . . . . . . . . . . 14 (𝑏 = (𝑥𝑧) → (𝑏 𝑦) = ((𝑥𝑧) ∩ 𝑦))
85 in32 3690 . . . . . . . . . . . . . . 15 ((𝑥𝑧) ∩ 𝑦) = ((𝑥 𝑦) ∩ 𝑧)
86 inass 3688 . . . . . . . . . . . . . . 15 ((𝑥 𝑦) ∩ 𝑧) = (𝑥 ∩ ( 𝑦𝑧))
8785, 86eqtri 2536 . . . . . . . . . . . . . 14 ((𝑥𝑧) ∩ 𝑦) = (𝑥 ∩ ( 𝑦𝑧))
8884, 87syl6eq 2564 . . . . . . . . . . . . 13 (𝑏 = (𝑥𝑧) → (𝑏 𝑦) = (𝑥 ∩ ( 𝑦𝑧)))
8988fveq2d 5991 . . . . . . . . . . . 12 (𝑏 = (𝑥𝑧) → (#‘(𝑏 𝑦)) = (#‘(𝑥 ∩ ( 𝑦𝑧))))
9083, 89oveq12d 6444 . . . . . . . . . . 11 (𝑏 = (𝑥𝑧) → ((#‘𝑏) − (#‘(𝑏 𝑦))) = ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))
91 ineq1 3672 . . . . . . . . . . . . . . 15 (𝑏 = (𝑥𝑧) → (𝑏 𝑠) = ((𝑥𝑧) ∩ 𝑠))
92 in32 3690 . . . . . . . . . . . . . . . 16 ((𝑥𝑧) ∩ 𝑠) = ((𝑥 𝑠) ∩ 𝑧)
93 inass 3688 . . . . . . . . . . . . . . . 16 ((𝑥 𝑠) ∩ 𝑧) = (𝑥 ∩ ( 𝑠𝑧))
9492, 93eqtri 2536 . . . . . . . . . . . . . . 15 ((𝑥𝑧) ∩ 𝑠) = (𝑥 ∩ ( 𝑠𝑧))
9591, 94syl6eq 2564 . . . . . . . . . . . . . 14 (𝑏 = (𝑥𝑧) → (𝑏 𝑠) = (𝑥 ∩ ( 𝑠𝑧)))
9695fveq2d 5991 . . . . . . . . . . . . 13 (𝑏 = (𝑥𝑧) → (#‘(𝑏 𝑠)) = (#‘(𝑥 ∩ ( 𝑠𝑧))))
9796oveq2d 6442 . . . . . . . . . . . 12 (𝑏 = (𝑥𝑧) → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
9897sumeq2sdv 14151 . . . . . . . . . . 11 (𝑏 = (𝑥𝑧) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
9990, 98eqeq12d 2529 . . . . . . . . . 10 (𝑏 = (𝑥𝑧) → (((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
10099rspcva 3184 . . . . . . . . 9 (((𝑥𝑧) ∈ Fin ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
10182, 100sylan 486 . . . . . . . 8 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
10278, 101oveq12d 6444 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
103 inss1 3698 . . . . . . . . . . . . . 14 (𝑥 𝑦) ⊆ 𝑥
104 ssfi 7941 . . . . . . . . . . . . . 14 ((𝑥 ∈ Fin ∧ (𝑥 𝑦) ⊆ 𝑥) → (𝑥 𝑦) ∈ Fin)
10579, 103, 104sylancl 692 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 𝑦) ∈ Fin)
106 hashun3 12899 . . . . . . . . . . . . 13 (((𝑥 𝑦) ∈ Fin ∧ (𝑥𝑧) ∈ Fin) → (#‘((𝑥 𝑦) ∪ (𝑥𝑧))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘((𝑥 𝑦) ∩ (𝑥𝑧)))))
107105, 82, 106syl2anc 690 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘((𝑥 𝑦) ∪ (𝑥𝑧))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘((𝑥 𝑦) ∩ (𝑥𝑧)))))
108 indi 3735 . . . . . . . . . . . . 13 (𝑥 ∩ ( 𝑦𝑧)) = ((𝑥 𝑦) ∪ (𝑥𝑧))
109108fveq2i 5990 . . . . . . . . . . . 12 (#‘(𝑥 ∩ ( 𝑦𝑧))) = (#‘((𝑥 𝑦) ∪ (𝑥𝑧)))
110 inindi 3695 . . . . . . . . . . . . . 14 (𝑥 ∩ ( 𝑦𝑧)) = ((𝑥 𝑦) ∩ (𝑥𝑧))
111110fveq2i 5990 . . . . . . . . . . . . 13 (#‘(𝑥 ∩ ( 𝑦𝑧))) = (#‘((𝑥 𝑦) ∩ (𝑥𝑧)))
112111oveq2i 6437 . . . . . . . . . . . 12 (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘((𝑥 𝑦) ∩ (𝑥𝑧))))
113107, 109, 1123eqtr4g 2573 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) = (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))
114 hashcl 12874 . . . . . . . . . . . . . 14 ((𝑥 𝑦) ∈ Fin → (#‘(𝑥 𝑦)) ∈ ℕ0)
115105, 114syl 17 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 𝑦)) ∈ ℕ0)
116115nn0cnd 11108 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 𝑦)) ∈ ℂ)
117 hashcl 12874 . . . . . . . . . . . . . 14 ((𝑥𝑧) ∈ Fin → (#‘(𝑥𝑧)) ∈ ℕ0)
11882, 117syl 17 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥𝑧)) ∈ ℕ0)
119118nn0cnd 11108 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥𝑧)) ∈ ℂ)
120 inss1 3698 . . . . . . . . . . . . . . 15 (𝑥 ∩ ( 𝑦𝑧)) ⊆ 𝑥
121 ssfi 7941 . . . . . . . . . . . . . . 15 ((𝑥 ∈ Fin ∧ (𝑥 ∩ ( 𝑦𝑧)) ⊆ 𝑥) → (𝑥 ∩ ( 𝑦𝑧)) ∈ Fin)
12279, 120, 121sylancl 692 . . . . . . . . . . . . . 14 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑥 ∩ ( 𝑦𝑧)) ∈ Fin)
123 hashcl 12874 . . . . . . . . . . . . . 14 ((𝑥 ∩ ( 𝑦𝑧)) ∈ Fin → (#‘(𝑥 ∩ ( 𝑦𝑧))) ∈ ℕ0)
124122, 123syl 17 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) ∈ ℕ0)
125124nn0cnd 11108 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) ∈ ℂ)
126116, 119, 125addsubassd 10163 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (((#‘(𝑥 𝑦)) + (#‘(𝑥𝑧))) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
127113, 126eqtrd 2548 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘(𝑥 ∩ ( 𝑦𝑧))) = ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
128127oveq2d 6442 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = ((#‘𝑥) − ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))))
129 hashcl 12874 . . . . . . . . . . . 12 (𝑥 ∈ Fin → (#‘𝑥) ∈ ℕ0)
130129adantl 480 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℕ0)
131130nn0cnd 11108 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (#‘𝑥) ∈ ℂ)
132119, 125subcld 10143 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) ∈ ℂ)
133131, 116, 132subsub4d 10174 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))) = ((#‘𝑥) − ((#‘(𝑥 𝑦)) + ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))))
134128, 133eqtr4d 2551 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
135134adantr 479 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = (((#‘𝑥) − (#‘(𝑥 𝑦))) − ((#‘(𝑥𝑧)) − (#‘(𝑥 ∩ ( 𝑦𝑧))))))
136 disjdif 3895 . . . . . . . . . . 11 (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅
137136a1i 11 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝒫 𝑦 ∩ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = ∅)
138 ssun1 3642 . . . . . . . . . . . . . 14 𝑦 ⊆ (𝑦 ∪ {𝑧})
139 sspwb 4742 . . . . . . . . . . . . . 14 (𝑦 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
140138, 139mpbi 218 . . . . . . . . . . . . 13 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧})
141 undif 3904 . . . . . . . . . . . . 13 (𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧}))
142140, 141mpbi 218 . . . . . . . . . . . 12 (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) = 𝒫 (𝑦 ∪ {𝑧})
143142eqcomi 2523 . . . . . . . . . . 11 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
144143a1i 11 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) = (𝒫 𝑦 ∪ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)))
145 simpll 785 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝑦 ∈ Fin)
146 snfi 7799 . . . . . . . . . . . 12 {𝑧} ∈ Fin
147 unfi 7988 . . . . . . . . . . . 12 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
148145, 146, 147sylancl 692 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
149 pwfi 8020 . . . . . . . . . . 11 ((𝑦 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
150148, 149sylib 206 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 (𝑦 ∪ {𝑧}) ∈ Fin)
15155a1i 11 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → -1 ∈ ℂ)
152 elpwi 4020 . . . . . . . . . . . . . 14 (𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
153 ssfi 7941 . . . . . . . . . . . . . 14 (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝑠 ⊆ (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
154148, 152, 153syl2an 492 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑠 ∈ Fin)
155 hashcl 12874 . . . . . . . . . . . . 13 (𝑠 ∈ Fin → (#‘𝑠) ∈ ℕ0)
156154, 155syl 17 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘𝑠) ∈ ℕ0)
157151, 156expcld 12738 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (-1↑(#‘𝑠)) ∈ ℂ)
158 simplr 787 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → 𝑥 ∈ Fin)
159 inss1 3698 . . . . . . . . . . . . . 14 (𝑥 𝑠) ⊆ 𝑥
160 ssfi 7941 . . . . . . . . . . . . . 14 ((𝑥 ∈ Fin ∧ (𝑥 𝑠) ⊆ 𝑥) → (𝑥 𝑠) ∈ Fin)
161158, 159, 160sylancl 692 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 𝑠) ∈ Fin)
162 hashcl 12874 . . . . . . . . . . . . 13 ((𝑥 𝑠) ∈ Fin → (#‘(𝑥 𝑠)) ∈ ℕ0)
163161, 162syl 17 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 𝑠)) ∈ ℕ0)
164163nn0cnd 11108 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 𝑠)) ∈ ℂ)
165157, 164mulcld 9815 . . . . . . . . . 10 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
166137, 144, 150, 165fsumsplit 14187 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
167 fveq2 5987 . . . . . . . . . . . . . 14 (𝑠 = (𝑡 ∪ {𝑧}) → (#‘𝑠) = (#‘(𝑡 ∪ {𝑧})))
168167oveq2d 6442 . . . . . . . . . . . . 13 (𝑠 = (𝑡 ∪ {𝑧}) → (-1↑(#‘𝑠)) = (-1↑(#‘(𝑡 ∪ {𝑧}))))
169 inteq 4311 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑡 ∪ {𝑧}) → 𝑠 = (𝑡 ∪ {𝑧}))
17027intunsn 4349 . . . . . . . . . . . . . . . 16 (𝑡 ∪ {𝑧}) = ( 𝑡𝑧)
171169, 170syl6eq 2564 . . . . . . . . . . . . . . 15 (𝑠 = (𝑡 ∪ {𝑧}) → 𝑠 = ( 𝑡𝑧))
172171ineq2d 3679 . . . . . . . . . . . . . 14 (𝑠 = (𝑡 ∪ {𝑧}) → (𝑥 𝑠) = (𝑥 ∩ ( 𝑡𝑧)))
173172fveq2d 5991 . . . . . . . . . . . . 13 (𝑠 = (𝑡 ∪ {𝑧}) → (#‘(𝑥 𝑠)) = (#‘(𝑥 ∩ ( 𝑡𝑧))))
174168, 173oveq12d 6444 . . . . . . . . . . . 12 (𝑠 = (𝑡 ∪ {𝑧}) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))))
175 pwfi 8020 . . . . . . . . . . . . 13 (𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin)
176145, 175sylib 206 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ∈ Fin)
177 eqid 2514 . . . . . . . . . . . . 13 (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})) = (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))
178 elpwi 4020 . . . . . . . . . . . . . . . . 17 (𝑢 ∈ 𝒫 𝑦𝑢𝑦)
179178adantl 480 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑢𝑦)
180 unss1 3648 . . . . . . . . . . . . . . . 16 (𝑢𝑦 → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
181179, 180syl 17 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
182 vex 3080 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
183 snex 4734 . . . . . . . . . . . . . . . . 17 {𝑧} ∈ V
184182, 183unex 6730 . . . . . . . . . . . . . . . 16 (𝑢 ∪ {𝑧}) ∈ V
185184elpw 4017 . . . . . . . . . . . . . . 15 ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧}))
186181, 185sylibr 222 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝑦 ∪ {𝑧}))
187 simpllr 794 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ 𝑧𝑦)
188 elpwi 4020 . . . . . . . . . . . . . . . 16 ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦 → (𝑢 ∪ {𝑧}) ⊆ 𝑦)
189 ssun2 3643 . . . . . . . . . . . . . . . . . . 19 {𝑧} ⊆ (𝑢 ∪ {𝑧})
19027snss 4162 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧}))
191189, 190mpbir 219 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ (𝑢 ∪ {𝑧})
192191a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → 𝑧 ∈ (𝑢 ∪ {𝑧}))
193 ssel 3466 . . . . . . . . . . . . . . . . 17 ((𝑢 ∪ {𝑧}) ⊆ 𝑦 → (𝑧 ∈ (𝑢 ∪ {𝑧}) → 𝑧𝑦))
194192, 193syl5com 31 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ⊆ 𝑦𝑧𝑦))
195188, 194syl5 33 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ((𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦𝑧𝑦))
196187, 195mtod 187 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → ¬ (𝑢 ∪ {𝑧}) ∈ 𝒫 𝑦)
197186, 196eldifd 3455 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑢 ∈ 𝒫 𝑦) → (𝑢 ∪ {𝑧}) ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
198 eldifi 3598 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
199198adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
200199elpwid 4021 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ (𝑦 ∪ {𝑧}))
201 uncom 3623 . . . . . . . . . . . . . . . 16 (𝑦 ∪ {𝑧}) = ({𝑧} ∪ 𝑦)
202200, 201syl6sseq 3518 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → 𝑠 ⊆ ({𝑧} ∪ 𝑦))
203 ssundif 3907 . . . . . . . . . . . . . . 15 (𝑠 ⊆ ({𝑧} ∪ 𝑦) ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
204202, 203sylib 206 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ⊆ 𝑦)
205 vex 3080 . . . . . . . . . . . . . . 15 𝑦 ∈ V
206205elpw2 4654 . . . . . . . . . . . . . 14 ((𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦 ↔ (𝑠 ∖ {𝑧}) ⊆ 𝑦)
207204, 206sylibr 222 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → (𝑠 ∖ {𝑧}) ∈ 𝒫 𝑦)
208 elpwunsn 4074 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦) → 𝑧𝑠)
209208ad2antll 760 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑧𝑠)
210209snssd 4184 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → {𝑧} ⊆ 𝑠)
211 ssequn2 3652 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑧}) = 𝑠)
212210, 211sylib 206 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 ∪ {𝑧}) = 𝑠)
213212eqcomd 2520 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑠 = (𝑠 ∪ {𝑧}))
214 uneq1 3626 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = ((𝑠 ∖ {𝑧}) ∪ {𝑧}))
215 undif1 3898 . . . . . . . . . . . . . . . . 17 ((𝑠 ∖ {𝑧}) ∪ {𝑧}) = (𝑠 ∪ {𝑧})
216214, 215syl6eq 2564 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑠 ∖ {𝑧}) → (𝑢 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
217216eqeq2d 2524 . . . . . . . . . . . . . . 15 (𝑢 = (𝑠 ∖ {𝑧}) → (𝑠 = (𝑢 ∪ {𝑧}) ↔ 𝑠 = (𝑠 ∪ {𝑧})))
218213, 217syl5ibrcom 235 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) → 𝑠 = (𝑢 ∪ {𝑧})))
219178ad2antrl 759 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢𝑦)
220 simpllr 794 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧𝑦)
221219, 220ssneldd 3475 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → ¬ 𝑧𝑢)
222 difsnb 4181 . . . . . . . . . . . . . . . . 17 𝑧𝑢 ↔ (𝑢 ∖ {𝑧}) = 𝑢)
223221, 222sylib 206 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 ∖ {𝑧}) = 𝑢)
224223eqcomd 2520 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → 𝑢 = (𝑢 ∖ {𝑧}))
225 difeq1 3587 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = ((𝑢 ∪ {𝑧}) ∖ {𝑧}))
226 difun2 3903 . . . . . . . . . . . . . . . . 17 ((𝑢 ∪ {𝑧}) ∖ {𝑧}) = (𝑢 ∖ {𝑧})
227225, 226syl6eq 2564 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑢 ∪ {𝑧}) → (𝑠 ∖ {𝑧}) = (𝑢 ∖ {𝑧}))
228227eqeq2d 2524 . . . . . . . . . . . . . . 15 (𝑠 = (𝑢 ∪ {𝑧}) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑢 = (𝑢 ∖ {𝑧})))
229224, 228syl5ibrcom 235 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑠 = (𝑢 ∪ {𝑧}) → 𝑢 = (𝑠 ∖ {𝑧})))
230218, 229impbid 200 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ (𝑢 ∈ 𝒫 𝑦𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))) → (𝑢 = (𝑠 ∖ {𝑧}) ↔ 𝑠 = (𝑢 ∪ {𝑧})))
231177, 197, 207, 230f1o2d 6661 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧})):𝒫 𝑦1-1-onto→(𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦))
232 uneq1 3626 . . . . . . . . . . . . . 14 (𝑢 = 𝑡 → (𝑢 ∪ {𝑧}) = (𝑡 ∪ {𝑧}))
233 vex 3080 . . . . . . . . . . . . . . 15 𝑡 ∈ V
234233, 183unex 6730 . . . . . . . . . . . . . 14 (𝑡 ∪ {𝑧}) ∈ V
235232, 177, 234fvmpt 6075 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 𝑦 → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
236235adantl 480 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑡 ∈ 𝒫 𝑦) → ((𝑢 ∈ 𝒫 𝑦 ↦ (𝑢 ∪ {𝑧}))‘𝑡) = (𝑡 ∪ {𝑧}))
237198, 165sylan2 489 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
238174, 176, 231, 236, 237fsumf1o 14170 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))))
239 uneq1 3626 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑠 → (𝑡 ∪ {𝑧}) = (𝑠 ∪ {𝑧}))
240239fveq2d 5991 . . . . . . . . . . . . . . 15 (𝑡 = 𝑠 → (#‘(𝑡 ∪ {𝑧})) = (#‘(𝑠 ∪ {𝑧})))
241240oveq2d 6442 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (-1↑(#‘(𝑡 ∪ {𝑧}))) = (-1↑(#‘(𝑠 ∪ {𝑧}))))
242 inteq 4311 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑠 𝑡 = 𝑠)
243242ineq1d 3678 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑠 → ( 𝑡𝑧) = ( 𝑠𝑧))
244243ineq2d 3679 . . . . . . . . . . . . . . 15 (𝑡 = 𝑠 → (𝑥 ∩ ( 𝑡𝑧)) = (𝑥 ∩ ( 𝑠𝑧)))
245244fveq2d 5991 . . . . . . . . . . . . . 14 (𝑡 = 𝑠 → (#‘(𝑥 ∩ ( 𝑡𝑧))) = (#‘(𝑥 ∩ ( 𝑠𝑧))))
246241, 245oveq12d 6444 . . . . . . . . . . . . 13 (𝑡 = 𝑠 → ((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))) = ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
247246cbvsumv 14143 . . . . . . . . . . . 12 Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧))))
24855a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → -1 ∈ ℂ)
249 elpwi 4020 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ 𝒫 𝑦𝑠𝑦)
250 ssfi 7941 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ Fin ∧ 𝑠𝑦) → 𝑠 ∈ Fin)
251145, 249, 250syl2an 492 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ Fin)
252251, 155syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘𝑠) ∈ ℕ0)
253248, 252expp1d 12739 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑((#‘𝑠) + 1)) = ((-1↑(#‘𝑠)) · -1))
254249adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠𝑦)
255 simpllr 794 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧𝑦)
256254, 255ssneldd 3475 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ¬ 𝑧𝑠)
257 hashunsng 12907 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ V → ((𝑠 ∈ Fin ∧ ¬ 𝑧𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1)))
25827, 257ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ Fin ∧ ¬ 𝑧𝑠) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
259251, 256, 258syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑠 ∪ {𝑧})) = ((#‘𝑠) + 1))
260259oveq2d 6442 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1↑((#‘𝑠) + 1)))
261140sseli 3468 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ 𝒫 𝑦𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
262261, 157sylan2 489 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘𝑠)) ∈ ℂ)
263248, 262mulcomd 9816 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = ((-1↑(#‘𝑠)) · -1))
264253, 260, 2633eqtr4d 2558 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = (-1 · (-1↑(#‘𝑠))))
265262mulm1d 10232 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1 · (-1↑(#‘𝑠))) = -(-1↑(#‘𝑠)))
266264, 265eqtrd 2548 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-1↑(#‘(𝑠 ∪ {𝑧}))) = -(-1↑(#‘𝑠)))
267266oveq1d 6441 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
268 inss1 3698 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝑠𝑧)) ⊆ 𝑥
269 ssfi 7941 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ Fin ∧ (𝑥 ∩ ( 𝑠𝑧)) ⊆ 𝑥) → (𝑥 ∩ ( 𝑠𝑧)) ∈ Fin)
270158, 268, 269sylancl 692 . . . . . . . . . . . . . . . . . 18 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (𝑥 ∩ ( 𝑠𝑧)) ∈ Fin)
271 hashcl 12874 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∩ ( 𝑠𝑧)) ∈ Fin → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℕ0)
272270, 271syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℕ0)
273272nn0cnd 11108 . . . . . . . . . . . . . . . 16 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℂ)
274261, 273sylan2 489 . . . . . . . . . . . . . . 15 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (#‘(𝑥 ∩ ( 𝑠𝑧))) ∈ ℂ)
275262, 274mulneg1d 10233 . . . . . . . . . . . . . 14 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → (-(-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
276267, 275eqtrd 2548 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = -((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
277276sumeq2dv 14150 . . . . . . . . . . . 12 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘(𝑠 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
278247, 277syl5eq 2560 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑡 ∈ 𝒫 𝑦((-1↑(#‘(𝑡 ∪ {𝑧}))) · (#‘(𝑥 ∩ ( 𝑡𝑧)))) = Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
279157, 273mulcld 9815 . . . . . . . . . . . . 13 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
280261, 279sylan2 489 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
281176, 280fsumneg 14230 . . . . . . . . . . 11 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦-((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
282238, 278, 2813eqtrd 2552 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))))
283282oveq2d 6442 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + Σ𝑠 ∈ (𝒫 (𝑦 ∪ {𝑧}) ∖ 𝒫 𝑦)((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
284140a1i 11 . . . . . . . . . . . . 13 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → 𝒫 𝑦 ⊆ 𝒫 (𝑦 ∪ {𝑧}))
285284sselda 3472 . . . . . . . . . . . 12 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → 𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧}))
286285, 165syldan 485 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
287176, 286fsumcl 14180 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) ∈ ℂ)
288285, 279syldan 485 . . . . . . . . . . 11 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ 𝑠 ∈ 𝒫 𝑦) → ((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
289176, 288fsumcl 14180 . . . . . . . . . 10 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧)))) ∈ ℂ)
290287, 289negsubd 10149 . . . . . . . . 9 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) + -Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
291166, 283, 2903eqtrd 2552 . . . . . . . 8 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
292291adantr 479 . . . . . . 7 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) = (Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))) − Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑥 ∩ ( 𝑠𝑧))))))
293102, 135, 2923eqtr4d 2558 . . . . . 6 ((((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) ∧ ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
294293ex 448 . . . . 5 (((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) ∧ 𝑥 ∈ Fin) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) → ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
295294ralrimdva 2856 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) → ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
296 ineq1 3672 . . . . . . . 8 (𝑏 = 𝑥 → (𝑏 ∩ ( 𝑦𝑧)) = (𝑥 ∩ ( 𝑦𝑧)))
297296fveq2d 5991 . . . . . . 7 (𝑏 = 𝑥 → (#‘(𝑏 ∩ ( 𝑦𝑧))) = (#‘(𝑥 ∩ ( 𝑦𝑧))))
29867, 297oveq12d 6444 . . . . . 6 (𝑏 = 𝑥 → ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))))
299 ineq1 3672 . . . . . . . . 9 (𝑏 = 𝑥 → (𝑏 𝑠) = (𝑥 𝑠))
300299fveq2d 5991 . . . . . . . 8 (𝑏 = 𝑥 → (#‘(𝑏 𝑠)) = (#‘(𝑥 𝑠)))
301300oveq2d 6442 . . . . . . 7 (𝑏 = 𝑥 → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
302301sumeq2sdv 14151 . . . . . 6 (𝑏 = 𝑥 → Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
303298, 302eqeq12d 2529 . . . . 5 (𝑏 = 𝑥 → (((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠)))))
304303cbvralv 3051 . . . 4 (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ∀𝑥 ∈ Fin ((#‘𝑥) − (#‘(𝑥 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑥 𝑠))))
305295, 304syl6ibr 240 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝑦))) = Σ𝑠 ∈ 𝒫 𝑦((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 ∩ ( 𝑦𝑧)))) = Σ𝑠 ∈ 𝒫 (𝑦 ∪ {𝑧})((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠)))))
30616, 24, 38, 46, 66, 305findcard2s 7962 . 2 (𝐴 ∈ Fin → ∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))))
307 fveq2 5987 . . . . 5 (𝑏 = 𝐵 → (#‘𝑏) = (#‘𝐵))
308 ineq1 3672 . . . . . 6 (𝑏 = 𝐵 → (𝑏 𝐴) = (𝐵 𝐴))
309308fveq2d 5991 . . . . 5 (𝑏 = 𝐵 → (#‘(𝑏 𝐴)) = (#‘(𝐵 𝐴)))
310307, 309oveq12d 6444 . . . 4 (𝑏 = 𝐵 → ((#‘𝑏) − (#‘(𝑏 𝐴))) = ((#‘𝐵) − (#‘(𝐵 𝐴))))
311 simpl 471 . . . . . . . 8 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → 𝑏 = 𝐵)
312311ineq1d 3678 . . . . . . 7 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → (𝑏 𝑠) = (𝐵 𝑠))
313312fveq2d 5991 . . . . . 6 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → (#‘(𝑏 𝑠)) = (#‘(𝐵 𝑠)))
314313oveq2d 6442 . . . . 5 ((𝑏 = 𝐵𝑠 ∈ 𝒫 𝐴) → ((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = ((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
315314sumeq2dv 14150 . . . 4 (𝑏 = 𝐵 → Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
316310, 315eqeq12d 2529 . . 3 (𝑏 = 𝐵 → (((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ↔ ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠)))))
317316rspccva 3185 . 2 ((∀𝑏 ∈ Fin ((#‘𝑏) − (#‘(𝑏 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝑏 𝑠))) ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
318306, 317sylan 486 1 ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘𝐵) − (#‘(𝐵 𝐴))) = Σ𝑠 ∈ 𝒫 𝐴((-1↑(#‘𝑠)) · (#‘(𝐵 𝑠))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1938  wral 2800  Vcvv 3077  cdif 3441  cun 3442  cin 3443  wss 3444  c0 3777  𝒫 cpw 4011  {csn 4028   cuni 4270   cint 4308  cmpt 4541  cfv 5689  (class class class)co 6426  Fincfn 7717  cc 9689  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696  cmin 10017  -cneg 10018  0cn0 11047  cexp 12590  #chash 12847  Σcsu 14133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-om 6834  df-1st 6934  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-2o 7324  df-oadd 7327  df-er 7505  df-map 7622  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-sup 8107  df-oi 8174  df-card 8524  df-cda 8749  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-n0 11048  df-z 11119  df-uz 11428  df-rp 11575  df-fz 12066  df-fzo 12203  df-seq 12532  df-exp 12591  df-hash 12848  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-clim 13933  df-sum 14134
This theorem is referenced by:  incexc  14277
  Copyright terms: Public domain W3C validator