let n be Nat; for A being Subset of (REAL n)
for x being Element of REAL n st A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) holds
0* n in A
let A be Subset of (REAL n); for x being Element of REAL n st A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) holds
0* n in A
let x be Element of REAL n; ( A is being_plane & x in A & ex a being Real st
( a <> 1 & a * x in A ) implies 0* n in A )
assume that
A1:
A is being_plane
and
A2:
x in A
and
A3:
ex a being Real st
( a <> 1 & a * x in A )
; 0* n in A
consider a being Real such that
A4:
a <> 1
and
A5:
a * x in A
by A3;
A6:
1 - a <> 0
by A4;
A7: (1 - (1 / (1 - a))) + ((1 / (1 - a)) * a) =
(1 - (1 / (1 - a))) + (a / (1 - a))
by XCMPLX_1:99
.=
1 + ((- (1 / (1 - a))) + (a / (1 - a)))
.=
1 + (((- 1) / (1 - a)) + (a / (1 - a)))
by XCMPLX_1:187
.=
1 + (((- 1) + a) / (1 - a))
by XCMPLX_1:62
.=
1 + ((- ((- a) - (- 1))) / (1 - a))
.=
1 + (- ((1 - a) / (1 - a)))
by XCMPLX_1:187
.=
1 - ((1 - a) / (1 - a))
.=
1 - 1
by A6, XCMPLX_1:60
.=
0
;
0* n =
0 * x
by EUCLID_4:3
.=
((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x)
by A7, EUCLID_4:7
.=
((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x))
by EUCLID_4:4
;
then A8:
0* n in Line (x,(a * x))
;
ex x1, x2, x3 being Element of REAL n st
( x2 - x1,x3 - x1 are_lindependent2 & A = plane (x1,x2,x3) )
by A1;
then
Line (x,(a * x)) c= A
by A2, A5, Th85;
hence
0* n in A
by A8; verum