let n be Nat; for r being Real
for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y}
let r be Real; for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y}
let y, z, x be Point of (TOP-REAL n); ( y in Sphere (x,r) & z in Ball (x,r) implies (LSeg (y,z)) /\ (Sphere (x,r)) = {y} )
set s = y;
set t = z;
assume that
A1:
y in Sphere (x,r)
and
A2:
z in Ball (x,r)
; (LSeg (y,z)) /\ (Sphere (x,r)) = {y}
hereby TARSKI:def 3,
XBOOLE_0:def 10 {y} c= (LSeg (y,z)) /\ (Sphere (x,r))
let m be
object ;
( m in (LSeg (y,z)) /\ (Sphere (x,r)) implies b1 in {y} )assume A3:
m in (LSeg (y,z)) /\ (Sphere (x,r))
;
b1 in {y}then reconsider w =
m as
Point of
(TOP-REAL n) ;
w in LSeg (
y,
z)
by A3, XBOOLE_0:def 4;
then consider d being
Real such that A4:
0 <= d
and A5:
d <= 1
and A6:
w = ((1 - d) * y) + (d * z)
by RLTOPSP1:76;
A7:
|.(d * (z - x)).| =
|.d.| * |.(z - x).|
by TOPRNS_1:7
.=
d * |.(z - x).|
by A4, ABSVALUE:def 1
;
d - 1
<= 1
- 1
by A5, XREAL_1:9;
then A8:
- 0 <= - (d - 1)
;
A9:
|.((1 - d) * (y - x)).| =
|.(1 - d).| * |.(y - x).|
by TOPRNS_1:7
.=
(1 - d) * |.(y - x).|
by A8, ABSVALUE:def 1
.=
(1 - d) * r
by A1, Th7
;
m in Sphere (
x,
r)
by A3, XBOOLE_0:def 4;
then A10:
r =
|.(w - x).|
by Th7
.=
|.((((1 - d) * y) + (d * z)) - (((1 - d) + d) * x)).|
by A6, RLVECT_1:def 8
.=
|.((((1 - d) * y) + (d * z)) - (((1 - d) * x) + (d * x))).|
by RLVECT_1:def 6
.=
|.(((((1 - d) * y) + (d * z)) - ((1 - d) * x)) - (d * x)).|
by RLVECT_1:27
.=
|.(((((1 - d) * y) - ((1 - d) * x)) + (d * z)) - (d * x)).|
by RLVECT_1:def 3
.=
|.((((1 - d) * (y - x)) + (d * z)) - (d * x)).|
by RLVECT_1:34
.=
|.(((1 - d) * (y - x)) + ((d * z) - (d * x))).|
by RLVECT_1:def 3
.=
|.(((1 - d) * (y - x)) + (d * (z - x))).|
by RLVECT_1:34
;
end;
let m be object ; TARSKI:def 3 ( not m in {y} or m in (LSeg (y,z)) /\ (Sphere (x,r)) )
A12:
y in LSeg (y,z)
by RLTOPSP1:68;
assume
m in {y}
; m in (LSeg (y,z)) /\ (Sphere (x,r))
then
m = y
by TARSKI:def 1;
hence
m in (LSeg (y,z)) /\ (Sphere (x,r))
by A1, A12, XBOOLE_0:def 4; verum