Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . . . 5
β’ π½ = (MetOpenβπΆ) |
2 | 1 | mopntopon 13913 |
. . . 4
β’ (πΆ β (βMetβπ) β π½ β (TopOnβπ)) |
3 | 2 | 3ad2ant1 1018 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β π½ β (TopOnβπ)) |
4 | | metcn.4 |
. . . . 5
β’ πΎ = (MetOpenβπ·) |
5 | 4 | mopnval 13912 |
. . . 4
β’ (π· β (βMetβπ) β πΎ = (topGenβran (ballβπ·))) |
6 | 5 | 3ad2ant2 1019 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β πΎ = (topGenβran (ballβπ·))) |
7 | 4 | mopntopon 13913 |
. . . 4
β’ (π· β (βMetβπ) β πΎ β (TopOnβπ)) |
8 | 7 | 3ad2ant2 1019 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β πΎ β (TopOnβπ)) |
9 | | simp3 999 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β π β π) |
10 | 3, 6, 8, 9 | tgcnp 13679 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ’ β ran (ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))))) |
11 | | simpll2 1037 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β π· β (βMetβπ)) |
12 | | simplr 528 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β πΉ:πβΆπ) |
13 | | simpll3 1038 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β π β π) |
14 | 12, 13 | ffvelcdmd 5652 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β (πΉβπ) β π) |
15 | | simpr 110 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β π¦ β
β+) |
16 | | blcntr 13886 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π¦ β β+) β (πΉβπ) β ((πΉβπ)(ballβπ·)π¦)) |
17 | 11, 14, 15, 16 | syl3anc 1238 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β (πΉβπ) β ((πΉβπ)(ballβπ·)π¦)) |
18 | | rpxr 9660 |
. . . . . . . . . 10
β’ (π¦ β β+
β π¦ β
β*) |
19 | 18 | adantl 277 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β π¦ β
β*) |
20 | | blelrn 13890 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π¦ β β*) β ((πΉβπ)(ballβπ·)π¦) β ran (ballβπ·)) |
21 | 11, 14, 19, 20 | syl3anc 1238 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β ((πΉβπ)(ballβπ·)π¦) β ran (ballβπ·)) |
22 | | eleq2 2241 |
. . . . . . . . . 10
β’ (π’ = ((πΉβπ)(ballβπ·)π¦) β ((πΉβπ) β π’ β (πΉβπ) β ((πΉβπ)(ballβπ·)π¦))) |
23 | | sseq2 3179 |
. . . . . . . . . . . 12
β’ (π’ = ((πΉβπ)(ballβπ·)π¦) β ((πΉ β π£) β π’ β (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦))) |
24 | 23 | anbi2d 464 |
. . . . . . . . . . 11
β’ (π’ = ((πΉβπ)(ballβπ·)π¦) β ((π β π£ β§ (πΉ β π£) β π’) β (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦)))) |
25 | 24 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π’ = ((πΉβπ)(ballβπ·)π¦) β (βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦)))) |
26 | 22, 25 | imbi12d 234 |
. . . . . . . . 9
β’ (π’ = ((πΉβπ)(ballβπ·)π¦) β (((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦))))) |
27 | 26 | rspcv 2837 |
. . . . . . . 8
β’ (((πΉβπ)(ballβπ·)π¦) β ran (ballβπ·) β (βπ’ β ran (ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦))))) |
28 | 21, 27 | syl 14 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β
(βπ’ β ran
(ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β ((πΉβπ) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦))))) |
29 | 17, 28 | mpid 42 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β
(βπ’ β ran
(ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦)))) |
30 | | simpl1 1000 |
. . . . . . . . . . . 12
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β πΆ β (βMetβπ)) |
31 | 30 | ad2antrr 488 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π£ β π½)) β§ π β π£) β πΆ β (βMetβπ)) |
32 | | simplrr 536 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π£ β π½)) β§ π β π£) β π£ β π½) |
33 | | simpr 110 |
. . . . . . . . . . 11
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π£ β π½)) β§ π β π£) β π β π£) |
34 | 1 | mopni2 13953 |
. . . . . . . . . . 11
β’ ((πΆ β (βMetβπ) β§ π£ β π½ β§ π β π£) β βπ§ β β+ (π(ballβπΆ)π§) β π£) |
35 | 31, 32, 33, 34 | syl3anc 1238 |
. . . . . . . . . 10
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π£ β π½)) β§ π β π£) β βπ§ β β+ (π(ballβπΆ)π§) β π£) |
36 | | sstr2 3162 |
. . . . . . . . . . . 12
β’ ((πΉ β (π(ballβπΆ)π§)) β (πΉ β π£) β ((πΉ β π£) β ((πΉβπ)(ballβπ·)π¦) β (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
37 | | imass2 5004 |
. . . . . . . . . . . 12
β’ ((π(ballβπΆ)π§) β π£ β (πΉ β (π(ballβπΆ)π§)) β (πΉ β π£)) |
38 | 36, 37 | syl11 31 |
. . . . . . . . . . 11
β’ ((πΉ β π£) β ((πΉβπ)(ballβπ·)π¦) β ((π(ballβπΆ)π§) β π£ β (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
39 | 38 | reximdv 2578 |
. . . . . . . . . 10
β’ ((πΉ β π£) β ((πΉβπ)(ballβπ·)π¦) β (βπ§ β β+ (π(ballβπΆ)π§) β π£ β βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
40 | 35, 39 | syl5com 29 |
. . . . . . . . 9
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π£ β π½)) β§ π β π£) β ((πΉ β π£) β ((πΉβπ)(ballβπ·)π¦) β βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
41 | 40 | expimpd 363 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β β+ β§ π£ β π½)) β ((π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦)) β βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
42 | 41 | expr 375 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β (π£ β π½ β ((π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦)) β βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) |
43 | 42 | rexlimdv 2593 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β
(βπ£ β π½ (π β π£ β§ (πΉ β π£) β ((πΉβπ)(ballβπ·)π¦)) β βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
44 | 29, 43 | syld 45 |
. . . . 5
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β
(βπ’ β ran
(ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
45 | 44 | ralrimdva 2557 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ’ β ran (ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
46 | | simpl2 1001 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β π· β (βMetβπ)) |
47 | | blss 13898 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π’ β ran (ballβπ·) β§ (πΉβπ) β π’) β βπ¦ β β+ ((πΉβπ)(ballβπ·)π¦) β π’) |
48 | 47 | 3expib 1206 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β ((π’ β ran (ballβπ·) β§ (πΉβπ) β π’) β βπ¦ β β+ ((πΉβπ)(ballβπ·)π¦) β π’)) |
49 | 46, 48 | syl 14 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β ((π’ β ran (ballβπ·) β§ (πΉβπ) β π’) β βπ¦ β β+ ((πΉβπ)(ballβπ·)π¦) β π’)) |
50 | | r19.29r 2615 |
. . . . . . . . . 10
β’
((βπ¦ β
β+ ((πΉβπ)(ballβπ·)π¦) β π’ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)) β βπ¦ β β+ (((πΉβπ)(ballβπ·)π¦) β π’ β§ βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
51 | 30 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β πΆ β (βMetβπ)) |
52 | 13 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β π β π) |
53 | | rpxr 9660 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β β+
β π§ β
β*) |
54 | 53 | ad2antrl 490 |
. . . . . . . . . . . . . . . 16
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β π§ β β*) |
55 | 1 | blopn 13960 |
. . . . . . . . . . . . . . . 16
β’ ((πΆ β (βMetβπ) β§ π β π β§ π§ β β*) β (π(ballβπΆ)π§) β π½) |
56 | 51, 52, 54, 55 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β (π(ballβπΆ)π§) β π½) |
57 | | simprl 529 |
. . . . . . . . . . . . . . . 16
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β π§ β β+) |
58 | | blcntr 13886 |
. . . . . . . . . . . . . . . 16
β’ ((πΆ β (βMetβπ) β§ π β π β§ π§ β β+) β π β (π(ballβπΆ)π§)) |
59 | 51, 52, 57, 58 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β π β (π(ballβπΆ)π§)) |
60 | | sstr 3163 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β (πΉ β (π(ballβπΆ)π§)) β π’) |
61 | 60 | ad2ant2l 508 |
. . . . . . . . . . . . . . . 16
β’ (((π§ β β+
β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)) β§ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’)) β (πΉ β (π(ballβπΆ)π§)) β π’) |
62 | 61 | ancoms 268 |
. . . . . . . . . . . . . . 15
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β (πΉ β (π(ballβπΆ)π§)) β π’) |
63 | | eleq2 2241 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = (π(ballβπΆ)π§) β (π β π£ β π β (π(ballβπΆ)π§))) |
64 | | imaeq2 4966 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = (π(ballβπΆ)π§) β (πΉ β π£) = (πΉ β (π(ballβπΆ)π§))) |
65 | 64 | sseq1d 3184 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = (π(ballβπΆ)π§) β ((πΉ β π£) β π’ β (πΉ β (π(ballβπΆ)π§)) β π’)) |
66 | 63, 65 | anbi12d 473 |
. . . . . . . . . . . . . . . 16
β’ (π£ = (π(ballβπΆ)π§) β ((π β π£ β§ (πΉ β π£) β π’) β (π β (π(ballβπΆ)π§) β§ (πΉ β (π(ballβπΆ)π§)) β π’))) |
67 | 66 | rspcev 2841 |
. . . . . . . . . . . . . . 15
β’ (((π(ballβπΆ)π§) β π½ β§ (π β (π(ballβπΆ)π§) β§ (πΉ β (π(ballβπΆ)π§)) β π’)) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) |
68 | 56, 59, 62, 67 | syl12anc 1236 |
. . . . . . . . . . . . . 14
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ (π§ β β+ β§ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) |
69 | 68 | expr 375 |
. . . . . . . . . . . . 13
β’
((((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β§ π§ β β+) β ((πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
70 | 69 | rexlimdva 2594 |
. . . . . . . . . . . 12
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ) β§
π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β§ ((πΉβπ)(ballβπ·)π¦) β π’) β (βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
71 | 70 | expimpd 363 |
. . . . . . . . . . 11
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β§ π¦ β β+) β ((((πΉβπ)(ballβπ·)π¦) β π’ β§ βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
72 | 71 | rexlimdva 2594 |
. . . . . . . . . 10
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ (((πΉβπ)(ballβπ·)π¦) β π’ β§ βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
73 | 50, 72 | syl5 32 |
. . . . . . . . 9
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β ((βπ¦ β β+ ((πΉβπ)(ballβπ·)π¦) β π’ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
74 | 73 | expd 258 |
. . . . . . . 8
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ ((πΉβπ)(ballβπ·)π¦) β π’ β (βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)))) |
75 | 49, 74 | syld 45 |
. . . . . . 7
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β ((π’ β ran (ballβπ·) β§ (πΉβπ) β π’) β (βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)))) |
76 | 75 | com23 78 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β ((π’ β ran (ballβπ·) β§ (πΉβπ) β π’) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)))) |
77 | 76 | exp4a 366 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β (π’ β ran (ballβπ·) β ((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))))) |
78 | 77 | ralrimdv 2556 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦) β βπ’ β ran (ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)))) |
79 | 45, 78 | impbid 129 |
. . 3
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ’ β ran (ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) β βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦))) |
80 | 79 | pm5.32da 452 |
. 2
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β ((πΉ:πβΆπ β§ βπ’ β ran (ballβπ·)((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) |
81 | 10, 80 | bitrd 188 |
1
β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) |