Metamath Proof Explorer

Theorem sylow2a

Description: A named lemma of Sylow's second and third theorems. If G is a finite P -group that acts on the finite set Y , then the set Z of all points of Y fixed by every element of G has cardinality equivalent to the cardinality of Y , mod P . (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2a.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
sylow2a.m ⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
sylow2a.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
sylow2a.f ⊢ ( 𝜑 → 𝑋 ∈ Fin )
sylow2a.y ⊢ ( 𝜑 → 𝑌 ∈ Fin )
sylow2a.z ⊢ 𝑍 = { 𝑢 ∈ 𝑌 ∣ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 }
sylow2a.r ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
Assertion sylow2a ( 𝜑 → 𝑃 ∥ ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 sylow2a.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 sylow2a.m ⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
3 sylow2a.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
4 sylow2a.f ⊢ ( 𝜑 → 𝑋 ∈ Fin )
5 sylow2a.y ⊢ ( 𝜑 → 𝑌 ∈ Fin )
6 sylow2a.z ⊢ 𝑍 = { 𝑢 ∈ 𝑌 ∣ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 }
7 sylow2a.r ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
8 1 2 3 4 5 6 7 sylow2alem2 ⊢ ( 𝜑 → 𝑃 ∥ Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )
9 inass ⊢ ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ( ( 𝑌 / ∼ ) ∩ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) )
10 disjdif ⊢ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ∅
11 10 ineq2i ⊢ ( ( 𝑌 / ∼ ) ∩ ( 𝒫 𝑍 ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) ) = ( ( 𝑌 / ∼ ) ∩ ∅ )
12 in0 ⊢ ( ( 𝑌 / ∼ ) ∩ ∅ ) = ∅
13 9 11 12 3eqtri ⊢ ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ∅
14 13 a1i ⊢ ( 𝜑 → ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∩ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ∅ )
15 inundif ⊢ ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) = ( 𝑌 / ∼ )
16 15 eqcomi ⊢ ( 𝑌 / ∼ ) = ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) )
17 16 a1i ⊢ ( 𝜑 → ( 𝑌 / ∼ ) = ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∪ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) )
18 pwfi ⊢ ( 𝑌 ∈ Fin ↔ 𝒫 𝑌 ∈ Fin )
19 5 18 sylib ⊢ ( 𝜑 → 𝒫 𝑌 ∈ Fin )
20 7 1 gaorber ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∼ Er 𝑌 )
21 2 20 syl ⊢ ( 𝜑 → ∼ Er 𝑌 )
22 21 qsss ⊢ ( 𝜑 → ( 𝑌 / ∼ ) ⊆ 𝒫 𝑌 )
23 19 22 ssfid ⊢ ( 𝜑 → ( 𝑌 / ∼ ) ∈ Fin )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑌 ∈ Fin )
25 22 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ∈ 𝒫 𝑌 )
26 25 elpwid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ⊆ 𝑌 )
27 24 26 ssfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → 𝑧 ∈ Fin )
28 hashcl ⊢ ( 𝑧 ∈ Fin → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
30 29 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℂ )
31 14 17 23 30 fsumsplit ⊢ ( 𝜑 → Σ 𝑧 ∈ ( 𝑌 / ∼ ) ( ♯ ‘ 𝑧 ) = ( Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) )
32 21 5 qshash ⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) = Σ 𝑧 ∈ ( 𝑌 / ∼ ) ( ♯ ‘ 𝑧 ) )
33 inss1 ⊢ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ⊆ ( 𝑌 / ∼ )
34 ssfi ⊢ ( ( ( 𝑌 / ∼ ) ∈ Fin ∧ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ⊆ ( 𝑌 / ∼ ) ) → ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∈ Fin )
35 23 33 34 sylancl ⊢ ( 𝜑 → ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∈ Fin )
36 ax-1cn ⊢ 1 ∈ ℂ
37 fsumconst ⊢ ( ( ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) 1 = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) )
38 35 36 37 sylancl ⊢ ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) 1 = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) )
39 elin ⊢ ( 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ↔ ( 𝑧 ∈ ( 𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍 ) )
40 eqid ⊢ ( 𝑌 / ∼ ) = ( 𝑌 / ∼ )
41 sseq1 ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍 ) )
42 velpw ⊢ ( 𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍 )
43 41 42 bitr4di ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍 ) )
44 breq1 ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( [ 𝑤 ] ∼ ≈ 1o ↔ 𝑧 ≈ 1o ) )
45 43 44 imbi12d ⊢ ( [ 𝑤 ] ∼ = 𝑧 → ( ( [ 𝑤 ] ∼ ⊆ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) ↔ ( 𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1o ) ) )
46 21 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ∼ Er 𝑌 )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ 𝑌 )
48 46 47 erref ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∼ 𝑤 )
49 vex ⊢ 𝑤 ∈ V
50 49 49 elec ⊢ ( 𝑤 ∈ [ 𝑤 ] ∼ ↔ 𝑤 ∼ 𝑤 )
51 48 50 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → 𝑤 ∈ [ 𝑤 ] ∼ )
52 ssel ⊢ ( [ 𝑤 ] ∼ ⊆ 𝑍 → ( 𝑤 ∈ [ 𝑤 ] ∼ → 𝑤 ∈ 𝑍 ) )
53 51 52 syl5com ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( [ 𝑤 ] ∼ ⊆ 𝑍 → 𝑤 ∈ 𝑍 ) )
54 1 2 3 4 5 6 7 sylow2alem1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ = { 𝑤 } )
55 49 ensn1 ⊢ { 𝑤 } ≈ 1o
56 54 55 eqbrtrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ ≈ 1o )
57 56 ex ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( 𝑤 ∈ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) )
59 53 58 syld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( [ 𝑤 ] ∼ ⊆ 𝑍 → [ 𝑤 ] ∼ ≈ 1o ) )
60 40 45 59 ectocld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 / ∼ ) ) → ( 𝑧 ∈ 𝒫 𝑍 → 𝑧 ≈ 1o ) )
61 60 impr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 / ∼ ) ∧ 𝑧 ∈ 𝒫 𝑍 ) ) → 𝑧 ≈ 1o )
62 39 61 sylan2b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ≈ 1o )
63 en1b ⊢ ( 𝑧 ≈ 1o ↔ 𝑧 = { ∪ 𝑧 } )
64 62 63 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 = { ∪ 𝑧 } )
65 64 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ { ∪ 𝑧 } ) )
66 vuniex ⊢ ∪ 𝑧 ∈ V
67 hashsng ⊢ ( ∪ 𝑧 ∈ V → ( ♯ ‘ { ∪ 𝑧 } ) = 1 )
68 66 67 ax-mp ⊢ ( ♯ ‘ { ∪ 𝑧 } ) = 1
69 65 68 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) = 1 )
70 69 sumeq2dv ⊢ ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) 1 )
71 6 ssrab3 ⊢ 𝑍 ⊆ 𝑌
72 ssfi ⊢ ( ( 𝑌 ∈ Fin ∧ 𝑍 ⊆ 𝑌 ) → 𝑍 ∈ Fin )
73 5 71 72 sylancl ⊢ ( 𝜑 → 𝑍 ∈ Fin )
74 hashcl ⊢ ( 𝑍 ∈ Fin → ( ♯ ‘ 𝑍 ) ∈ ℕ0 )
75 73 74 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) ∈ ℕ0 )
76 75 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) ∈ ℂ )
77 76 mulridd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) · 1 ) = ( ♯ ‘ 𝑍 ) )
78 6 5 rabexd ⊢ ( 𝜑 → 𝑍 ∈ V )
79 eqid ⊢ ( 𝑤 ∈ 𝑍 ↦ { 𝑤 } ) = ( 𝑤 ∈ 𝑍 ↦ { 𝑤 } )
80 7 relopabiv ⊢ Rel ∼
81 relssdmrn ⊢ ( Rel ∼ → ∼ ⊆ ( dom ∼ × ran ∼ ) )
82 80 81 ax-mp ⊢ ∼ ⊆ ( dom ∼ × ran ∼ )
83 erdm ⊢ ( ∼ Er 𝑌 → dom ∼ = 𝑌 )
84 21 83 syl ⊢ ( 𝜑 → dom ∼ = 𝑌 )
85 84 5 eqeltrd ⊢ ( 𝜑 → dom ∼ ∈ Fin )
86 errn ⊢ ( ∼ Er 𝑌 → ran ∼ = 𝑌 )
87 21 86 syl ⊢ ( 𝜑 → ran ∼ = 𝑌 )
88 87 5 eqeltrd ⊢ ( 𝜑 → ran ∼ ∈ Fin )
89 85 88 xpexd ⊢ ( 𝜑 → ( dom ∼ × ran ∼ ) ∈ V )
90 ssexg ⊢ ( ( ∼ ⊆ ( dom ∼ × ran ∼ ) ∧ ( dom ∼ × ran ∼ ) ∈ V ) → ∼ ∈ V )
91 82 89 90 sylancr ⊢ ( 𝜑 → ∼ ∈ V )
92 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ 𝑍 )
93 71 92 sselid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → 𝑤 ∈ 𝑌 )
94 ecelqsw ⊢ ( ( ∼ ∈ V ∧ 𝑤 ∈ 𝑌 ) → [ 𝑤 ] ∼ ∈ ( 𝑌 / ∼ ) )
95 91 93 94 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → [ 𝑤 ] ∼ ∈ ( 𝑌 / ∼ ) )
96 54 95 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ∈ ( 𝑌 / ∼ ) )
97 snelpwi ⊢ ( 𝑤 ∈ 𝑍 → { 𝑤 } ∈ 𝒫 𝑍 )
98 97 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ∈ 𝒫 𝑍 )
99 96 98 elind ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → { 𝑤 } ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) )
100 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) )
101 100 elin2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ∈ 𝒫 𝑍 )
102 101 elpwid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → 𝑧 ⊆ 𝑍 )
103 64 102 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → { ∪ 𝑧 } ⊆ 𝑍 )
104 66 snss ⊢ ( ∪ 𝑧 ∈ 𝑍 ↔ { ∪ 𝑧 } ⊆ 𝑍 )
105 103 104 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ∪ 𝑧 ∈ 𝑍 )
106 sneq ⊢ ( 𝑤 = ∪ 𝑧 → { 𝑤 } = { ∪ 𝑧 } )
107 106 eqeq2d ⊢ ( 𝑤 = ∪ 𝑧 → ( 𝑧 = { 𝑤 } ↔ 𝑧 = { ∪ 𝑧 } ) )
108 64 107 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) → ( 𝑤 = ∪ 𝑧 → 𝑧 = { 𝑤 } ) )
109 108 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) ) → ( 𝑤 = ∪ 𝑧 → 𝑧 = { 𝑤 } ) )
110 unieq ⊢ ( 𝑧 = { 𝑤 } → ∪ 𝑧 = ∪ { 𝑤 } )
111 unisnv ⊢ ∪ { 𝑤 } = 𝑤
112 110 111 eqtr2di ⊢ ( 𝑧 = { 𝑤 } → 𝑤 = ∪ 𝑧 )
113 109 112 impbid1 ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑍 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) ) → ( 𝑤 = ∪ 𝑧 ↔ 𝑧 = { 𝑤 } ) )
114 79 99 105 113 f1o2d ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑍 ↦ { 𝑤 } ) : 𝑍 –1-1-onto→ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) )
115 78 114 hasheqf1od ⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) = ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) )
116 115 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) · 1 ) = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) )
117 77 116 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) = ( ( ♯ ‘ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ) · 1 ) )
118 38 70 117 3eqtr4rd ⊢ ( 𝜑 → ( ♯ ‘ 𝑍 ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )
119 118 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∩ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) )
120 31 32 119 3eqtr4rd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( ♯ ‘ 𝑌 ) )
121 hashcl ⊢ ( 𝑌 ∈ Fin → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
122 5 121 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
123 122 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑌 ) ∈ ℂ )
124 diffi ⊢ ( ( 𝑌 / ∼ ) ∈ Fin → ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ∈ Fin )
125 23 124 syl ⊢ ( 𝜑 → ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ∈ Fin )
126 eldifi ⊢ ( 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) → 𝑧 ∈ ( 𝑌 / ∼ ) )
127 126 30 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℂ )
128 125 127 fsumcl ⊢ ( 𝜑 → Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ∈ ℂ )
129 123 76 128 subaddd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ↔ ( ( ♯ ‘ 𝑍 ) + Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) ) = ( ♯ ‘ 𝑌 ) ) )
130 120 129 mpbird ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) = Σ 𝑧 ∈ ( ( 𝑌 / ∼ ) ∖ 𝒫 𝑍 ) ( ♯ ‘ 𝑧 ) )
131 8 130 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ♯ ‘ 𝑌 ) − ( ♯ ‘ 𝑍 ) ) )