Step | Hyp | Ref
| Expression |
1 | | qtopeu.3 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:πβontoβπ) |
2 | | fofn 6759 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβontoβπ β πΉ Fn π) |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ Fn π) |
4 | 3 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β πΉ Fn π) |
5 | | fniniseg 7011 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn π β (π¦ β (β‘πΉ β {(πΉβπ₯)}) β (π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β (π¦ β (β‘πΉ β {(πΉβπ₯)}) β (π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)))) |
7 | | eqcom 2740 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ₯) = (πΉβπ¦) β (πΉβπ¦) = (πΉβπ₯)) |
8 | 7 | 3anbi3i 1160 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦)) β (π₯ β π β§ π¦ β π β§ (πΉβπ¦) = (πΉβπ₯))) |
9 | | 3anass 1096 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β§ π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)) β (π₯ β π β§ (π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)))) |
10 | 8, 9 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦)) β (π₯ β π β§ (π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)))) |
11 | | qtopeu.5 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦))) β (πΊβπ₯) = (πΊβπ¦)) |
12 | 10, 11 | sylan2br 596 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ (π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)))) β (πΊβπ₯) = (πΊβπ¦)) |
13 | 12 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ (π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)))) β (πΊβπ¦) = (πΊβπ₯)) |
14 | 13 | expr 458 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β ((π¦ β π β§ (πΉβπ¦) = (πΉβπ₯)) β (πΊβπ¦) = (πΊβπ₯))) |
15 | 6, 14 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β (π¦ β (β‘πΉ β {(πΉβπ₯)}) β (πΊβπ¦) = (πΊβπ₯))) |
16 | 15 | ralrimiv 3139 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β βπ¦ β (β‘πΉ β {(πΉβπ₯)})(πΊβπ¦) = (πΊβπ₯)) |
17 | | qtopeu.1 |
. . . . . . . . . . . . . . 15
β’ (π β π½ β (TopOnβπ)) |
18 | | qtopeu.4 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ β (π½ Cn πΎ)) |
19 | | cntop2 22608 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β (π½ Cn πΎ) β πΎ β Top) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΎ β Top) |
21 | | toptopon2 22283 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β πΎ β (TopOnββͺ πΎ)) |
23 | | cnf2 22616 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ πΊ β (π½ Cn πΎ)) β πΊ:πβΆβͺ πΎ) |
24 | 17, 22, 18, 23 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:πβΆβͺ πΎ) |
25 | 24 | ffnd 6670 |
. . . . . . . . . . . . 13
β’ (π β πΊ Fn π) |
26 | 25 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β πΊ Fn π) |
27 | | cnvimass 6034 |
. . . . . . . . . . . . 13
β’ (β‘πΉ β {(πΉβπ₯)}) β dom πΉ |
28 | | fof 6757 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβontoβπ β πΉ:πβΆπ) |
29 | 1, 28 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:πβΆπ) |
30 | 29 | fdmd 6680 |
. . . . . . . . . . . . . 14
β’ (π β dom πΉ = π) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β dom πΉ = π) |
32 | 27, 31 | sseqtrid 3997 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β (β‘πΉ β {(πΉβπ₯)}) β π) |
33 | | eqeq1 2737 |
. . . . . . . . . . . . 13
β’ (π€ = (πΊβπ¦) β (π€ = (πΊβπ₯) β (πΊβπ¦) = (πΊβπ₯))) |
34 | 33 | ralima 7189 |
. . . . . . . . . . . 12
β’ ((πΊ Fn π β§ (β‘πΉ β {(πΉβπ₯)}) β π) β (βπ€ β (πΊ β (β‘πΉ β {(πΉβπ₯)}))π€ = (πΊβπ₯) β βπ¦ β (β‘πΉ β {(πΉβπ₯)})(πΊβπ¦) = (πΊβπ₯))) |
35 | 26, 32, 34 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (βπ€ β (πΊ β (β‘πΉ β {(πΉβπ₯)}))π€ = (πΊβπ₯) β βπ¦ β (β‘πΉ β {(πΉβπ₯)})(πΊβπ¦) = (πΊβπ₯))) |
36 | 16, 35 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β βπ€ β (πΊ β (β‘πΉ β {(πΉβπ₯)}))π€ = (πΊβπ₯)) |
37 | 24 | fdmd 6680 |
. . . . . . . . . . . . . . 15
β’ (π β dom πΊ = π) |
38 | 37 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β dom πΊ β π₯ β π)) |
39 | 38 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β π₯ β dom πΊ) |
40 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β π₯ β π) |
41 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β (πΉβπ₯) = (πΉβπ₯)) |
42 | | fniniseg 7011 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π β (π₯ β (β‘πΉ β {(πΉβπ₯)}) β (π₯ β π β§ (πΉβπ₯) = (πΉβπ₯)))) |
43 | 4, 42 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π) β (π₯ β (β‘πΉ β {(πΉβπ₯)}) β (π₯ β π β§ (πΉβπ₯) = (πΉβπ₯)))) |
44 | 40, 41, 43 | mpbir2and 712 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β π₯ β (β‘πΉ β {(πΉβπ₯)})) |
45 | | inelcm 4425 |
. . . . . . . . . . . . 13
β’ ((π₯ β dom πΊ β§ π₯ β (β‘πΉ β {(πΉβπ₯)})) β (dom πΊ β© (β‘πΉ β {(πΉβπ₯)})) β β
) |
46 | 39, 44, 45 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β (dom πΊ β© (β‘πΉ β {(πΉβπ₯)})) β β
) |
47 | | imadisj 6033 |
. . . . . . . . . . . . 13
β’ ((πΊ β (β‘πΉ β {(πΉβπ₯)})) = β
β (dom πΊ β© (β‘πΉ β {(πΉβπ₯)})) = β
) |
48 | 47 | necon3bii 2993 |
. . . . . . . . . . . 12
β’ ((πΊ β (β‘πΉ β {(πΉβπ₯)})) β β
β (dom πΊ β© (β‘πΉ β {(πΉβπ₯)})) β β
) |
49 | 46, 48 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (πΊ β (β‘πΉ β {(πΉβπ₯)})) β β
) |
50 | | eqsn 4790 |
. . . . . . . . . . 11
β’ ((πΊ β (β‘πΉ β {(πΉβπ₯)})) β β
β ((πΊ β (β‘πΉ β {(πΉβπ₯)})) = {(πΊβπ₯)} β βπ€ β (πΊ β (β‘πΉ β {(πΉβπ₯)}))π€ = (πΊβπ₯))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β ((πΊ β (β‘πΉ β {(πΉβπ₯)})) = {(πΊβπ₯)} β βπ€ β (πΊ β (β‘πΉ β {(πΉβπ₯)}))π€ = (πΊβπ₯))) |
52 | 36, 51 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (πΊ β (β‘πΉ β {(πΉβπ₯)})) = {(πΊβπ₯)}) |
53 | 52 | unieqd 4880 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) = βͺ {(πΊβπ₯)}) |
54 | | fvex 6856 |
. . . . . . . . 9
β’ (πΊβπ₯) β V |
55 | 54 | unisn 4888 |
. . . . . . . 8
β’ βͺ {(πΊβπ₯)} = (πΊβπ₯) |
56 | 53, 55 | eqtr2di 2790 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πΊβπ₯) = βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)}))) |
57 | 56 | mpteq2dva 5206 |
. . . . . 6
β’ (π β (π₯ β π β¦ (πΊβπ₯)) = (π₯ β π β¦ βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})))) |
58 | 24 | feqmptd 6911 |
. . . . . 6
β’ (π β πΊ = (π₯ β π β¦ (πΊβπ₯))) |
59 | 29 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πΉβπ₯) β π) |
60 | 29 | feqmptd 6911 |
. . . . . . 7
β’ (π β πΉ = (π₯ β π β¦ (πΉβπ₯))) |
61 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) = (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€})))) |
62 | | sneq 4597 |
. . . . . . . . . 10
β’ (π€ = (πΉβπ₯) β {π€} = {(πΉβπ₯)}) |
63 | 62 | imaeq2d 6014 |
. . . . . . . . 9
β’ (π€ = (πΉβπ₯) β (β‘πΉ β {π€}) = (β‘πΉ β {(πΉβπ₯)})) |
64 | 63 | imaeq2d 6014 |
. . . . . . . 8
β’ (π€ = (πΉβπ₯) β (πΊ β (β‘πΉ β {π€})) = (πΊ β (β‘πΉ β {(πΉβπ₯)}))) |
65 | 64 | unieqd 4880 |
. . . . . . 7
β’ (π€ = (πΉβπ₯) β βͺ (πΊ β (β‘πΉ β {π€})) = βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)}))) |
66 | 59, 60, 61, 65 | fmptco 7076 |
. . . . . 6
β’ (π β ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ) = (π₯ β π β¦ βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})))) |
67 | 57, 58, 66 | 3eqtr4d 2783 |
. . . . 5
β’ (π β πΊ = ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ)) |
68 | 67, 18 | eqeltrrd 2835 |
. . . 4
β’ (π β ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ) β (π½ Cn πΎ)) |
69 | 24 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (πΊβπ₯) β βͺ πΎ) |
70 | 56, 69 | eqeltrrd 2835 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) β βͺ
πΎ) |
71 | 70 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ₯ β π βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) β βͺ
πΎ) |
72 | 65 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π€ = (πΉβπ₯) β βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) = βͺ (πΊ β (β‘πΉ β {π€}))) |
73 | 72 | eqcoms 2741 |
. . . . . . . . . 10
β’ ((πΉβπ₯) = π€ β βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) = βͺ (πΊ β (β‘πΉ β {π€}))) |
74 | 73 | eleq1d 2819 |
. . . . . . . . 9
β’ ((πΉβπ₯) = π€ β (βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) β βͺ
πΎ β βͺ (πΊ
β (β‘πΉ β {π€})) β βͺ πΎ)) |
75 | 74 | cbvfo 7236 |
. . . . . . . 8
β’ (πΉ:πβontoβπ β (βπ₯ β π βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) β βͺ
πΎ β βπ€ β π βͺ (πΊ β (β‘πΉ β {π€})) β βͺ πΎ)) |
76 | 1, 75 | syl 17 |
. . . . . . 7
β’ (π β (βπ₯ β π βͺ (πΊ β (β‘πΉ β {(πΉβπ₯)})) β βͺ
πΎ β βπ€ β π βͺ (πΊ β (β‘πΉ β {π€})) β βͺ πΎ)) |
77 | 71, 76 | mpbid 231 |
. . . . . 6
β’ (π β βπ€ β π βͺ (πΊ β (β‘πΉ β {π€})) β βͺ πΎ) |
78 | | eqid 2733 |
. . . . . . 7
β’ (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) = (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) |
79 | 78 | fmpt 7059 |
. . . . . 6
β’
(βπ€ β
π βͺ (πΊ
β (β‘πΉ β {π€})) β βͺ πΎ β (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))):πβΆβͺ πΎ) |
80 | 77, 79 | sylib 217 |
. . . . 5
β’ (π β (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))):πβΆβͺ πΎ) |
81 | | qtopcn 23081 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ))
β§ (πΉ:πβontoβπ β§ (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))):πβΆβͺ πΎ)) β ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β ((π½ qTop πΉ) Cn πΎ) β ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ) β (π½ Cn πΎ))) |
82 | 17, 22, 1, 80, 81 | syl22anc 838 |
. . . 4
β’ (π β ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β ((π½ qTop πΉ) Cn πΎ) β ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ) β (π½ Cn πΎ))) |
83 | 68, 82 | mpbird 257 |
. . 3
β’ (π β (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β ((π½ qTop πΉ) Cn πΎ)) |
84 | | coeq1 5814 |
. . . 4
β’ (π = (π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β (π β πΉ) = ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ)) |
85 | 84 | rspceeqv 3596 |
. . 3
β’ (((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β ((π½ qTop πΉ) Cn πΎ) β§ πΊ = ((π€ β π β¦ βͺ (πΊ β (β‘πΉ β {π€}))) β πΉ)) β βπ β ((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ)) |
86 | 83, 67, 85 | syl2anc 585 |
. 2
β’ (π β βπ β ((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ)) |
87 | | eqtr2 2757 |
. . . 4
β’ ((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β (π β πΉ) = (π β πΉ)) |
88 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β πΉ:πβontoβπ) |
89 | | qtoptopon 23071 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) |
90 | 17, 1, 89 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½ qTop πΉ) β (TopOnβπ)) |
91 | 90 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β (π½ qTop πΉ) β (TopOnβπ)) |
92 | 22 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β πΎ β (TopOnββͺ πΎ)) |
93 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β π β ((π½ qTop πΉ) Cn πΎ)) |
94 | | cnf2 22616 |
. . . . . . 7
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ π β ((π½ qTop πΉ) Cn πΎ)) β π:πβΆβͺ πΎ) |
95 | 91, 92, 93, 94 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β π:πβΆβͺ πΎ) |
96 | 95 | ffnd 6670 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β π Fn π) |
97 | | simprr 772 |
. . . . . . 7
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β π β ((π½ qTop πΉ) Cn πΎ)) |
98 | | cnf2 22616 |
. . . . . . 7
β’ (((π½ qTop πΉ) β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ π β ((π½ qTop πΉ) Cn πΎ)) β π:πβΆβͺ πΎ) |
99 | 91, 92, 97, 98 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β π:πβΆβͺ πΎ) |
100 | 99 | ffnd 6670 |
. . . . 5
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β π Fn π) |
101 | | cocan2 7239 |
. . . . 5
β’ ((πΉ:πβontoβπ β§ π Fn π β§ π Fn π) β ((π β πΉ) = (π β πΉ) β π = π)) |
102 | 88, 96, 100, 101 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β ((π β πΉ) = (π β πΉ) β π = π)) |
103 | 87, 102 | imbitrid 243 |
. . 3
β’ ((π β§ (π β ((π½ qTop πΉ) Cn πΎ) β§ π β ((π½ qTop πΉ) Cn πΎ))) β ((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β π = π)) |
104 | 103 | ralrimivva 3194 |
. 2
β’ (π β βπ β ((π½ qTop πΉ) Cn πΎ)βπ β ((π½ qTop πΉ) Cn πΎ)((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β π = π)) |
105 | | coeq1 5814 |
. . . 4
β’ (π = π β (π β πΉ) = (π β πΉ)) |
106 | 105 | eqeq2d 2744 |
. . 3
β’ (π = π β (πΊ = (π β πΉ) β πΊ = (π β πΉ))) |
107 | 106 | reu4 3690 |
. 2
β’
(β!π β
((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ) β (βπ β ((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ) β§ βπ β ((π½ qTop πΉ) Cn πΎ)βπ β ((π½ qTop πΉ) Cn πΎ)((πΊ = (π β πΉ) β§ πΊ = (π β πΉ)) β π = π))) |
108 | 86, 104, 107 | sylanbrc 584 |
1
β’ (π β β!π β ((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ)) |