let R be Element of (ProjectiveSpace (TOP-REAL 3)); for P, Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3)
for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model
let P, Q be Element of BK_model ; for u, v, w being non zero Element of (TOP-REAL 3)
for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model
let u, v, w be non zero Element of (TOP-REAL 3); for r being Real st 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) holds
R is Element of BK_model
let r be Real; ( 0 <= r & r <= 1 & P = Dir u & Q = Dir v & R = Dir w & u . 3 = 1 & v . 3 = 1 & w = (r * u) + ((1 - r) * v) implies R is Element of BK_model )
assume that
A1:
( 0 <= r & r <= 1 )
and
A2:
( P = Dir u & Q = Dir v & R = Dir w )
and
A3:
( u . 3 = 1 & v . 3 = 1 )
and
A4:
w = (r * u) + ((1 - r) * v)
; R is Element of BK_model
reconsider ru = r * u, rv = (1 - r) * v as Element of REAL 3 by EUCLID:22;
A5: w . 3 =
(ru . 3) + (rv . 3)
by A4, RVSUM_1:11
.=
(r * (u . 3)) + (rv . 3)
by RVSUM_1:44
.=
r + ((1 - r) * 1)
by A3, RVSUM_1:44
.=
1
;
consider u2 being non zero Element of (TOP-REAL 3) such that
A6:
( Dir u2 = P & u2 . 3 = 1 & BK_to_REAL2 P = |[(u2 . 1),(u2 . 2)]| )
by BKMODEL2:def 2;
A7:
u = u2
by A2, A3, A6, Th16;
reconsider ru2 = |[(u2 . 1),(u2 . 2)]| as Element of (TOP-REAL 2) ;
consider v2 being non zero Element of (TOP-REAL 3) such that
A8:
( Dir v2 = Q & v2 . 3 = 1 & BK_to_REAL2 Q = |[(v2 . 1),(v2 . 2)]| )
by BKMODEL2:def 2;
A9:
v = v2
by A2, A3, A8, Th16;
reconsider rv2 = |[(v2 . 1),(v2 . 2)]| as Element of (TOP-REAL 2) ;
reconsider rw = |[(w . 1),(w . 2)]| as Element of (TOP-REAL 2) ;
rw = (r * ru2) + ((1 - r) * rv2)
proof
A10:
w . 1 =
(ru . 1) + (rv . 1)
by A4, RVSUM_1:11
.=
(r * (u . 1)) + (rv . 1)
by RVSUM_1:44
.=
(r * (u2 . 1)) + ((1 - r) * (v2 . 1))
by A7, A9, RVSUM_1:44
;
A13:
w . 2 =
(ru . 2) + (rv . 2)
by A4, RVSUM_1:11
.=
(r * (u . 2)) + (rv . 2)
by RVSUM_1:44
.=
(r * (u2 . 2)) + ((1 - r) * (v2 . 2))
by A7, A9, RVSUM_1:44
;
(r * ru2) + ((1 - r) * rv2) =
|[(r * (u2 . 1)),(r * (u2 . 2))]| + ((1 - r) * |[(v2 . 1),(v2 . 2)]|)
by EUCLID:58
.=
|[(r * (u2 . 1)),(r * (u2 . 2))]| + |[((1 - r) * (v2 . 1)),((1 - r) * (v2 . 2))]|
by EUCLID:58
;
hence
rw = (r * ru2) + ((1 - r) * rv2)
by A10, A13, EUCLID:56;
verum
end;
then
rw = ((1 - r) * rv2) + (r * ru2)
;
then
rw in { (((1 - r) * rv2) + (r * ru2)) where r is Real : ( 0 <= r & r <= 1 ) }
by A1;
then
rw in LSeg (rv2,ru2)
by RLTOPSP1:def 2;
then reconsider rw = rw as Element of inside_of_circle (0,0,1) by A6, A8, Th15;
consider RW2 being Element of (TOP-REAL 2) such that
A11:
( RW2 = rw & REAL2_to_BK rw = Dir |[(RW2 `1),(RW2 `2),1]| )
by BKMODEL2:def 3;
A12:
( rw `1 = w . 1 & rw `2 = w . 2 )
by EUCLID:52;
w =
|[(w `1),(w `2),(w `3)]|
by EUCLID_5:3
.=
|[(w . 1),(w `2),(w `3)]|
by EUCLID_5:def 1
.=
|[(w . 1),(w . 2),(w `3)]|
by EUCLID_5:def 2
.=
|[(w . 1),(w . 2),(w . 3)]|
by EUCLID_5:def 3
;
hence
R is Element of BK_model
by A2, A11, A5, A12; verum