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 holds
( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W )
let m be Nat of n; :: thesis: for RAS being ReperAlgebra of n
for W being ATLAS of RAS holds
( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W )
let RAS be ReperAlgebra of n; :: thesis: for W being ATLAS of RAS holds
( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W )
let W be ATLAS of RAS; :: thesis: ( RAS has_property_of_zero_in m iff for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W )
thus
( RAS has_property_of_zero_in m implies for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W )
:: thesis: ( ( for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W ) implies RAS has_property_of_zero_in m )proof
assume A1:
RAS has_property_of_zero_in m
;
:: thesis: for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W
let x be
Tuple of
(n + 1),
W;
:: thesis: Phi (x +* m,(0. W)) = 0. W
consider a being
Point of
RAS;
set b =
a,
(0. W) . W;
set p' =
(a,x . W) +* m,
a;
A2:
a,
(0. W) . W = a
by MIDSP_2:40;
then A3:
a,
(x +* m,(0. W)) . W = (a,x . W) +* m,
a
by Th29;
*' a,
((a,x . W) +* m,a) = a,
(0. W) . W
by A1, A2, Def6;
hence
Phi (x +* m,(0. W)) = 0. W
by A3, Th27;
:: thesis: verum
end;
thus
( ( for x being Tuple of (n + 1),W holds Phi (x +* m,(0. W)) = 0. W ) implies RAS has_property_of_zero_in m )
:: thesis: verumproof
assume A4:
for
x being
Tuple of
(n + 1),
W holds
Phi (x +* m,(0. W)) = 0. W
;
:: thesis: RAS has_property_of_zero_in m
for
a being
Point of
RAS for
p being
Tuple of
(n + 1),
RAS holds
*' a,
(p +* m,a) = a
proof
let a be
Point of
RAS;
:: thesis: for p being Tuple of (n + 1),RAS holds *' a,(p +* m,a) = alet p be
Tuple of
(n + 1),
RAS;
:: thesis: *' a,(p +* m,a) = a
set v =
W . a,
a;
set x' =
(W . a,p) +* m,
(0. W);
A5:
W . a,
a = 0. W
by MIDSP_2:39;
then A6:
W . a,
(p +* m,a) = (W . a,p) +* m,
(0. W)
by Th28;
Phi ((W . a,p) +* m,(0. W)) = W . a,
a
by A4, A5;
hence
*' a,
(p +* m,a) = a
by A6, Th26;
:: thesis: verum
end;
hence
RAS has_property_of_zero_in m
by Def6;
:: thesis: verum
end;