let n be Nat; for m being Nat of n
for RAS being ReperAlgebra of n
for W being ATLAS of RAS st m <= n holds
( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
let m be Nat of n; for RAS being ReperAlgebra of n
for W being ATLAS of RAS st m <= n holds
( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
let RAS be ReperAlgebra of n; for W being ATLAS of RAS st m <= n holds
( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
let W be ATLAS of RAS; ( m <= n implies ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) )
assume A1:
m <= n
; ( RAS is_alternative_in m iff for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
thus
( RAS is_alternative_in m implies for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W )
( ( for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W ) implies RAS is_alternative_in m )proof
set a = the
Point of
RAS;
assume A2:
RAS is_alternative_in m
;
for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W
let x be
Tuple of
(n + 1),
W;
Phi (x +* ((m + 1),(x . m))) = 0. W
set p = ( the
Point of
RAS,
x)
. W;
set b = ( the
Point of
RAS,
(0. W))
. W;
set p9 =
(( the Point of RAS,x) . W) +* (
(m + 1),
((( the Point of RAS,x) . W) . m));
( the
Point of
RAS,
(0. W))
. W = the
Point of
RAS
by MIDSP_2:34;
then A3:
*' ( the
Point of
RAS,
((( the Point of RAS,x) . W) +* ((m + 1),((( the Point of RAS,x) . W) . m))))
= ( the
Point of
RAS,
(0. W))
. W
by A2;
( the
Point of
RAS,
(x +* ((m + 1),(x . m))))
. W = (( the Point of RAS,x) . W) +* (
(m + 1),
((( the Point of RAS,x) . W) . m))
by A1, Th32;
hence
Phi (x +* ((m + 1),(x . m))) = 0. W
by A3, Th24;
verum
end;
assume A4:
for x being Tuple of (n + 1),W holds Phi (x +* ((m + 1),(x . m))) = 0. W
; RAS is_alternative_in m
for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pm being Point of RAS st p . m = pm holds
*' (a,(p +* ((m + 1),pm))) = a
proof
let a be
Point of
RAS;
for p being Tuple of (n + 1),RAS
for pm being Point of RAS st p . m = pm holds
*' (a,(p +* ((m + 1),pm))) = alet p be
Tuple of
(n + 1),
RAS;
for pm being Point of RAS st p . m = pm holds
*' (a,(p +* ((m + 1),pm))) = alet pm be
Point of
RAS;
( p . m = pm implies *' (a,(p +* ((m + 1),pm))) = a )
assume A5:
p . m = pm
;
*' (a,(p +* ((m + 1),pm))) = a
set x =
W . (
a,
p);
set v =
W . (
a,
a);
set x9 =
(W . (a,p)) +* (
(m + 1),
((W . (a,p)) . m));
W . (
a,
a)
= 0. W
by MIDSP_2:33;
then A6:
Phi ((W . (a,p)) +* ((m + 1),((W . (a,p)) . m))) = W . (
a,
a)
by A4;
W . (
a,
(p +* ((m + 1),(p . m))))
= (W . (a,p)) +* (
(m + 1),
((W . (a,p)) . m))
by A1, Th31;
hence
*' (
a,
(p +* ((m + 1),pm)))
= a
by A5, A6, Th23;
verum
end;
hence
RAS is_alternative_in m
; verum