let n be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: ( 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 )
:: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* (m + 1),(x . m)) = 0. W ) implies RAS is_alternative_in m )proof
assume A2:
RAS is_alternative_in m
;
:: thesis: 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;
:: thesis: Phi (x +* (m + 1),(x . m)) = 0. W
consider a being
Point of
RAS;
set p =
a,
x . W;
set b =
a,
(0. W) . W;
set p' =
(a,x . W) +* (m + 1),
((a,x . W) . m);
A3:
a,
(0. W) . W = a
by MIDSP_2:40;
A4:
a,
(x +* (m + 1),(x . m)) . W = (a,x . W) +* (m + 1),
((a,x . W) . m)
by A1, Th35;
*' a,
((a,x . W) +* (m + 1),((a,x . W) . m)) = a,
(0. W) . W
by A2, A3, Def9;
hence
Phi (x +* (m + 1),(x . m)) = 0. W
by A4, Th27;
:: thesis: verum
end;
thus
( ( for x being Tuple of (n + 1),W holds Phi (x +* (m + 1),(x . m)) = 0. W ) implies RAS is_alternative_in m )
:: thesis: verumproof
assume A5:
for
x being
Tuple of
(n + 1),
W holds
Phi (x +* (m + 1),(x . m)) = 0. W
;
:: thesis: 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;
:: thesis: 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;
:: thesis: for pm being Point of RAS st p . m = pm holds
*' a,(p +* (m + 1),pm) = alet pm be
Point of
RAS;
:: thesis: ( p . m = pm implies *' a,(p +* (m + 1),pm) = a )
assume A6:
p . m = pm
;
:: thesis: *' a,(p +* (m + 1),pm) = a
set x =
W . a,
p;
set v =
W . a,
a;
set x' =
(W . a,p) +* (m + 1),
((W . a,p) . m);
A7:
W . a,
a = 0. W
by MIDSP_2:39;
A8:
W . a,
(p +* (m + 1),(p . m)) = (W . a,p) +* (m + 1),
((W . a,p) . m)
by A1, Th34;
Phi ((W . a,p) +* (m + 1),((W . a,p) . m)) = W . a,
a
by A5, A7;
hence
*' a,
(p +* (m + 1),pm) = a
by A6, A8, Th26;
:: thesis: verum
end;
hence
RAS is_alternative_in m
by Def9;
:: thesis: verum
end;