Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π· β (βMetβπ)) |
2 | | simprl 770 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π΅ β ran (ballβπ·)) |
3 | | simplr 768 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β (π΅ β© πΆ)) |
4 | 3 | elin1d 4162 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β π΅) |
5 | | blss 23801 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·) β§ π β π΅) β βπ¦ β β+ (π(ballβπ·)π¦) β π΅) |
6 | 1, 2, 4, 5 | syl3anc 1372 |
. 2
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ¦ β β+ (π(ballβπ·)π¦) β π΅) |
7 | | simprr 772 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β πΆ β ran (ballβπ·)) |
8 | 3 | elin2d 4163 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β πΆ) |
9 | | blss 23801 |
. . 3
β’ ((π· β (βMetβπ) β§ πΆ β ran (ballβπ·) β§ π β πΆ) β βπ§ β β+ (π(ballβπ·)π§) β πΆ) |
10 | 1, 7, 8, 9 | syl3anc 1372 |
. 2
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ§ β β+ (π(ballβπ·)π§) β πΆ) |
11 | | reeanv 3216 |
. . 3
β’
(βπ¦ β
β+ βπ§ β β+ ((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β (βπ¦ β β+ (π(ballβπ·)π¦) β π΅ β§ βπ§ β β+ (π(ballβπ·)π§) β πΆ)) |
12 | | ss2in 4200 |
. . . . 5
β’ (((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β ((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) β (π΅ β© πΆ)) |
13 | | inss1 4192 |
. . . . . . . . . . 11
β’ (π΅ β© πΆ) β π΅ |
14 | | blf 23783 |
. . . . . . . . . . . . . 14
β’ (π· β (βMetβπ) β (ballβπ·):(π Γ
β*)βΆπ« π) |
15 | | frn 6679 |
. . . . . . . . . . . . . 14
β’
((ballβπ·):(π Γ
β*)βΆπ« π β ran (ballβπ·) β π« π) |
16 | 1, 14, 15 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β ran (ballβπ·) β π« π) |
17 | 16, 2 | sseldd 3949 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π΅ β π« π) |
18 | 17 | elpwid 4573 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π΅ β π) |
19 | 13, 18 | sstrid 3959 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β (π΅ β© πΆ) β π) |
20 | 19, 3 | sseldd 3949 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β π) |
21 | 1, 20 | jca 513 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β (π· β (βMetβπ) β§ π β π)) |
22 | | rpxr 12932 |
. . . . . . . . 9
β’ (π¦ β β+
β π¦ β
β*) |
23 | | rpxr 12932 |
. . . . . . . . 9
β’ (π§ β β+
β π§ β
β*) |
24 | 22, 23 | anim12i 614 |
. . . . . . . 8
β’ ((π¦ β β+
β§ π§ β
β+) β (π¦ β β* β§ π§ β
β*)) |
25 | | blin 23797 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π) β§ (π¦ β β* β§ π§ β β*))
β ((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) = (π(ballβπ·)if(π¦ β€ π§, π¦, π§))) |
26 | 21, 24, 25 | syl2an 597 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β ((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) = (π(ballβπ·)if(π¦ β€ π§, π¦, π§))) |
27 | 26 | sseq1d 3979 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β (((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) β (π΅ β© πΆ) β (π(ballβπ·)if(π¦ β€ π§, π¦, π§)) β (π΅ β© πΆ))) |
28 | | ifcl 4535 |
. . . . . . . 8
β’ ((π¦ β β+
β§ π§ β
β+) β if(π¦ β€ π§, π¦, π§) β
β+) |
29 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β (π(ballβπ·)π₯) = (π(ballβπ·)if(π¦ β€ π§, π¦, π§))) |
30 | 29 | sseq1d 3979 |
. . . . . . . . . 10
β’ (π₯ = if(π¦ β€ π§, π¦, π§) β ((π(ballβπ·)π₯) β (π΅ β© πΆ) β (π(ballβπ·)if(π¦ β€ π§, π¦, π§)) β (π΅ β© πΆ))) |
31 | 30 | rspcev 3583 |
. . . . . . . . 9
β’
((if(π¦ β€ π§, π¦, π§) β β+ β§ (π(ballβπ·)if(π¦ β€ π§, π¦, π§)) β (π΅ β© πΆ)) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ)) |
32 | 31 | ex 414 |
. . . . . . . 8
β’ (if(π¦ β€ π§, π¦, π§) β β+ β ((π(ballβπ·)if(π¦ β€ π§, π¦, π§)) β (π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
33 | 28, 32 | syl 17 |
. . . . . . 7
β’ ((π¦ β β+
β§ π§ β
β+) β ((π(ballβπ·)if(π¦ β€ π§, π¦, π§)) β (π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
34 | 33 | adantl 483 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β ((π(ballβπ·)if(π¦ β€ π§, π¦, π§)) β (π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
35 | 27, 34 | sylbid 239 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β (((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) β (π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
36 | 12, 35 | syl5 34 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β (((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
37 | 36 | rexlimdvva 3202 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β (βπ¦ β β+ βπ§ β β+
((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
38 | 11, 37 | biimtrrid 242 |
. 2
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β ((βπ¦ β β+ (π(ballβπ·)π¦) β π΅ β§ βπ§ β β+ (π(ballβπ·)π§) β πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
39 | 6, 10, 38 | mp2and 698 |
1
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ)) |