Step | Hyp | Ref
| Expression |
1 | | lmss.4 |
. . . . . 6
β’ (π β π½ β Top) |
2 | | toptopon2 22807 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
3 | 1, 2 | sylib 217 |
. . . . 5
β’ (π β π½ β (TopOnββͺ π½)) |
4 | | lmcl 23188 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ(βπ‘βπ½)π) β π β βͺ π½) |
5 | 3, 4 | sylan 579 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπ½)π) β π β βͺ π½) |
6 | | lmfss 23187 |
. . . . . . 7
β’ ((π½ β (TopOnββͺ π½)
β§ πΉ(βπ‘βπ½)π) β πΉ β (β Γ βͺ π½)) |
7 | 3, 6 | sylan 579 |
. . . . . 6
β’ ((π β§ πΉ(βπ‘βπ½)π) β πΉ β (β Γ βͺ π½)) |
8 | | rnss 5935 |
. . . . . 6
β’ (πΉ β (β Γ βͺ π½)
β ran πΉ β ran
(β Γ βͺ π½)) |
9 | 7, 8 | syl 17 |
. . . . 5
β’ ((π β§ πΉ(βπ‘βπ½)π) β ran πΉ β ran (β Γ βͺ π½)) |
10 | | rnxpss 6170 |
. . . . 5
β’ ran
(β Γ βͺ π½) β βͺ π½ |
11 | 9, 10 | sstrdi 3990 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπ½)π) β ran πΉ β βͺ π½) |
12 | 5, 11 | jca 511 |
. . 3
β’ ((π β§ πΉ(βπ‘βπ½)π) β (π β βͺ π½ β§ ran πΉ β βͺ π½)) |
13 | 12 | ex 412 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (π β βͺ π½ β§ ran πΉ β βͺ π½))) |
14 | | lmss.1 |
. . . . . . 7
β’ πΎ = (π½ βΎt π) |
15 | | lmss.3 |
. . . . . . . 8
β’ (π β π β π) |
16 | | resttopon2 23059 |
. . . . . . . 8
β’ ((π½ β (TopOnββͺ π½)
β§ π β π) β (π½ βΎt π) β (TopOnβ(π β© βͺ π½))) |
17 | 3, 15, 16 | syl2anc 583 |
. . . . . . 7
β’ (π β (π½ βΎt π) β (TopOnβ(π β© βͺ π½))) |
18 | 14, 17 | eqeltrid 2832 |
. . . . . 6
β’ (π β πΎ β (TopOnβ(π β© βͺ π½))) |
19 | | lmcl 23188 |
. . . . . 6
β’ ((πΎ β (TopOnβ(π β© βͺ π½))
β§ πΉ(βπ‘βπΎ)π) β π β (π β© βͺ π½)) |
20 | 18, 19 | sylan 579 |
. . . . 5
β’ ((π β§ πΉ(βπ‘βπΎ)π) β π β (π β© βͺ π½)) |
21 | 20 | elin2d 4195 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπΎ)π) β π β βͺ π½) |
22 | | lmfss 23187 |
. . . . . . . 8
β’ ((πΎ β (TopOnβ(π β© βͺ π½))
β§ πΉ(βπ‘βπΎ)π) β πΉ β (β Γ (π β© βͺ π½))) |
23 | 18, 22 | sylan 579 |
. . . . . . 7
β’ ((π β§ πΉ(βπ‘βπΎ)π) β πΉ β (β Γ (π β© βͺ π½))) |
24 | | rnss 5935 |
. . . . . . 7
β’ (πΉ β (β Γ (π β© βͺ π½))
β ran πΉ β ran
(β Γ (π β©
βͺ π½))) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’ ((π β§ πΉ(βπ‘βπΎ)π) β ran πΉ β ran (β Γ (π β© βͺ π½))) |
26 | | rnxpss 6170 |
. . . . . 6
β’ ran
(β Γ (π β©
βͺ π½)) β (π β© βͺ π½) |
27 | 25, 26 | sstrdi 3990 |
. . . . 5
β’ ((π β§ πΉ(βπ‘βπΎ)π) β ran πΉ β (π β© βͺ π½)) |
28 | | inss2 4225 |
. . . . 5
β’ (π β© βͺ π½)
β βͺ π½ |
29 | 27, 28 | sstrdi 3990 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπΎ)π) β ran πΉ β βͺ π½) |
30 | 21, 29 | jca 511 |
. . 3
β’ ((π β§ πΉ(βπ‘βπΎ)π) β (π β βͺ π½ β§ ran πΉ β βͺ π½)) |
31 | 30 | ex 412 |
. 2
β’ (π β (πΉ(βπ‘βπΎ)π β (π β βͺ π½ β§ ran πΉ β βͺ π½))) |
32 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π β βͺ π½) |
33 | | lmss.5 |
. . . . . . . 8
β’ (π β π β π) |
34 | 33 | adantr 480 |
. . . . . . 7
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π β π) |
35 | 34, 32 | elind 4190 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π β (π β© βͺ π½)) |
36 | 32, 35 | 2thd 265 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (π β βͺ π½ β π β (π β© βͺ π½))) |
37 | 14 | eleq2i 2820 |
. . . . . . . . 9
β’ (π£ β πΎ β π£ β (π½ βΎt π)) |
38 | 1 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π½ β Top) |
39 | 15 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π β π) |
40 | | elrest 17400 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π) β (π£ β (π½ βΎt π) β βπ’ β π½ π£ = (π’ β© π))) |
41 | 38, 39, 40 | syl2anc 583 |
. . . . . . . . . 10
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (π£ β (π½ βΎt π) β βπ’ β π½ π£ = (π’ β© π))) |
42 | 41 | biimpa 476 |
. . . . . . . . 9
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π£ β (π½ βΎt π)) β βπ’ β π½ π£ = (π’ β© π)) |
43 | 37, 42 | sylan2b 593 |
. . . . . . . 8
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π£ β πΎ) β βπ’ β π½ π£ = (π’ β© π)) |
44 | | r19.29r 3111 |
. . . . . . . . . 10
β’
((βπ’ β
π½ π£ = (π’ β© π) β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β βπ’ β π½ (π£ = (π’ β© π) β§ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
45 | 34 | biantrud 531 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (π β π’ β (π β π’ β§ π β π))) |
46 | | elin 3960 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π’ β© π) β (π β π’ β§ π β π)) |
47 | 45, 46 | bitr4di 289 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (π β π’ β π β (π’ β© π))) |
48 | | lmss.2 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π =
(β€β₯βπ) |
49 | 48 | uztrn2 12863 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
50 | | lmss.7 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΉ:πβΆπ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β πΉ:πβΆπ) |
52 | 51 | ffvelcdmda 7088 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π β π) β (πΉβπ) β π) |
53 | 52 | biantrud 531 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π β π) β ((πΉβπ) β π’ β ((πΉβπ) β π’ β§ (πΉβπ) β π))) |
54 | | elin 3960 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉβπ) β (π’ β© π) β ((πΉβπ) β π’ β§ (πΉβπ) β π)) |
55 | 53, 54 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π β π) β ((πΉβπ) β π’ β (πΉβπ) β (π’ β© π))) |
56 | 49, 55 | sylan2 592 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ (π β π β§ π β (β€β₯βπ))) β ((πΉβπ) β π’ β (πΉβπ) β (π’ β© π))) |
57 | 56 | anassrs 467 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π β π) β§ π β (β€β₯βπ)) β ((πΉβπ) β π’ β (πΉβπ) β (π’ β© π))) |
58 | 57 | ralbidva 3170 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π β π) β (βπ β (β€β₯βπ)(πΉβπ) β π’ β βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π))) |
59 | 58 | rexbidva 3171 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π))) |
60 | 47, 59 | imbi12d 344 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β ((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π)))) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β ((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π)))) |
62 | 61 | biimpd 228 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β ((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π)))) |
63 | | eleq2 2817 |
. . . . . . . . . . . . . . 15
β’ (π£ = (π’ β© π) β (π β π£ β π β (π’ β© π))) |
64 | | eleq2 2817 |
. . . . . . . . . . . . . . . 16
β’ (π£ = (π’ β© π) β ((πΉβπ) β π£ β (πΉβπ) β (π’ β© π))) |
65 | 64 | rexralbidv 3215 |
. . . . . . . . . . . . . . 15
β’ (π£ = (π’ β© π) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π))) |
66 | 63, 65 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π£ = (π’ β© π) β ((π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π)))) |
67 | 66 | imbi2d 340 |
. . . . . . . . . . . . 13
β’ (π£ = (π’ β© π) β (((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£)) β ((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π))))) |
68 | 62, 67 | syl5ibrcom 246 |
. . . . . . . . . . . 12
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β (π£ = (π’ β© π) β ((π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£)))) |
69 | 68 | impd 410 |
. . . . . . . . . . 11
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β ((π£ = (π’ β© π) β§ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
70 | 69 | rexlimdva 3150 |
. . . . . . . . . 10
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (βπ’ β π½ (π£ = (π’ β© π) β§ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
71 | 44, 70 | syl5 34 |
. . . . . . . . 9
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β ((βπ’ β π½ π£ = (π’ β© π) β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
72 | 71 | expdimp 452 |
. . . . . . . 8
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ βπ’ β π½ π£ = (π’ β© π)) β (βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
73 | 43, 72 | syldan 590 |
. . . . . . 7
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π£ β πΎ) β (βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
74 | 73 | ralrimdva 3149 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
75 | 38 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β π½ β Top) |
76 | 39 | adantr 480 |
. . . . . . . . . . 11
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β π β π) |
77 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β π’ β π½) |
78 | | elrestr 17401 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β π β§ π’ β π½) β (π’ β© π) β (π½ βΎt π)) |
79 | 75, 76, 77, 78 | syl3anc 1369 |
. . . . . . . . . 10
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β (π’ β© π) β (π½ βΎt π)) |
80 | 79, 14 | eleqtrrdi 2839 |
. . . . . . . . 9
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β (π’ β© π) β πΎ) |
81 | 66 | rspcv 3603 |
. . . . . . . . 9
β’ ((π’ β© π) β πΎ β (βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π)))) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β (βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£) β (π β (π’ β© π) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π’ β© π)))) |
83 | 82, 61 | sylibrd 259 |
. . . . . . 7
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π’ β π½) β (βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£) β (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
84 | 83 | ralrimdva 3149 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£) β βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’))) |
85 | 74, 84 | impbid 211 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’) β βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£))) |
86 | 36, 85 | anbi12d 630 |
. . . 4
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β ((π β βͺ π½ β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)) β (π β (π β© βͺ π½) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£)))) |
87 | 38, 2 | sylib 217 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π½ β (TopOnββͺ π½)) |
88 | | lmss.6 |
. . . . . 6
β’ (π β π β β€) |
89 | 88 | adantr 480 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β π β β€) |
90 | 51 | ffnd 6717 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β πΉ Fn π) |
91 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β ran πΉ β βͺ π½) |
92 | | df-f 6546 |
. . . . . 6
β’ (πΉ:πβΆβͺ π½ β (πΉ Fn π β§ ran πΉ β βͺ π½)) |
93 | 90, 91, 92 | sylanbrc 582 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β πΉ:πβΆβͺ π½) |
94 | | eqidd 2728 |
. . . . 5
β’ (((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β§ π β π) β (πΉβπ) = (πΉβπ)) |
95 | 87, 48, 89, 93, 94 | lmbrf 23151 |
. . . 4
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (πΉ(βπ‘βπ½)π β (π β βͺ π½ β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π’)))) |
96 | 18 | adantr 480 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β πΎ β (TopOnβ(π β© βͺ π½))) |
97 | 51 | frnd 6724 |
. . . . . . 7
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β ran πΉ β π) |
98 | 97, 91 | ssind 4228 |
. . . . . 6
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β ran πΉ β (π β© βͺ π½)) |
99 | | df-f 6546 |
. . . . . 6
β’ (πΉ:πβΆ(π β© βͺ π½) β (πΉ Fn π β§ ran πΉ β (π β© βͺ π½))) |
100 | 90, 98, 99 | sylanbrc 582 |
. . . . 5
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β πΉ:πβΆ(π β© βͺ π½)) |
101 | 96, 48, 89, 100, 94 | lmbrf 23151 |
. . . 4
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (πΉ(βπ‘βπΎ)π β (π β (π β© βͺ π½) β§ βπ£ β πΎ (π β π£ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π£)))) |
102 | 86, 95, 101 | 3bitr4d 311 |
. . 3
β’ ((π β§ (π β βͺ π½ β§ ran πΉ β βͺ π½)) β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) |
103 | 102 | ex 412 |
. 2
β’ (π β ((π β βͺ π½ β§ ran πΉ β βͺ π½) β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π))) |
104 | 13, 31, 103 | pm5.21ndd 379 |
1
β’ (π β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) |