let n be Nat; 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; 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; 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; ( 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 )
( ( 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
set a = the
Point of
RAS;
assume A1:
RAS has_property_of_zero_in m
;
for x being Tuple of (n + 1),W holds Phi (x +* (m,(0. W))) = 0. W
set b = ( the
Point of
RAS,
(0. W))
. W;
let x be
Tuple of
(n + 1),
W;
Phi (x +* (m,(0. W))) = 0. W
set p9 =
(( the Point of RAS,x) . W) +* (
m, the
Point of
RAS);
A2:
( the
Point of
RAS,
(0. W))
. W = the
Point of
RAS
by MIDSP_2:34;
then A3:
( the
Point of
RAS,
(x +* (m,(0. W))))
. W = (( the Point of RAS,x) . W) +* (
m, the
Point of
RAS)
by Th26;
*' ( the
Point of
RAS,
((( the Point of RAS,x) . W) +* (m, the Point of RAS)))
= ( the
Point of
RAS,
(0. W))
. W
by A1, A2;
hence
Phi (x +* (m,(0. W))) = 0. W
by A3, Th24;
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 )
verumproof
assume A4:
for
x being
Tuple of
(n + 1),
W holds
Phi (x +* (m,(0. W))) = 0. W
;
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;
for p being Tuple of (n + 1),RAS holds *' (a,(p +* (m,a))) = alet p be
Tuple of
(n + 1),
RAS;
*' (a,(p +* (m,a))) = a
set v =
W . (
a,
a);
set x9 =
(W . (a,p)) +* (
m,
(0. W));
W . (
a,
a)
= 0. W
by MIDSP_2:33;
then
(
W . (
a,
(p +* (m,a)))
= (W . (a,p)) +* (
m,
(0. W)) &
Phi ((W . (a,p)) +* (m,(0. W))) = W . (
a,
a) )
by A4, Th25;
hence
*' (
a,
(p +* (m,a)))
= a
by Th23;
verum
end;
hence
RAS has_property_of_zero_in m
;
verum
end;