let RNS1, RNS2 be RealLinearSpace; ( RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) implies for X being set holds
( X is Basis of RNS1 iff X is Basis of RNS2 ) )
assume A1:
RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #)
; for X being set holds
( X is Basis of RNS1 iff X is Basis of RNS2 )
let X be set ; ( X is Basis of RNS1 iff X is Basis of RNS2 )
set V = RNS1;
set W = RNS2;
hereby ( X is Basis of RNS2 implies X is Basis of RNS1 )
assume
X is
Basis of
RNS1
;
X is Basis of RNS2then reconsider A =
X as
Basis of
RNS1 ;
reconsider B =
A as
Subset of
RNS2 by A1;
(
A is
linearly-independent &
Lin A = RLSStruct(# the
carrier of
RNS1, the
ZeroF of
RNS1, the
addF of
RNS1, the
Mult of
RNS1 #) )
by RLVECT_3:def 3;
then A3:
B is
linearly-independent
by A1, Th17;
set W0 =
(Omega). RNS2;
A4:
(Omega). RNS2 = RLSStruct(# the
carrier of
RNS2, the
ZeroF of
RNS2, the
addF of
RNS2, the
Mult of
RNS2 #)
by RLSUB_1:def 4;
A5:
Lin B is
strict Subspace of
(Omega). RNS2
by REAL_NS2:49;
A6:
[#] (Lin A) = the
carrier of
RNS2
by A1, RLVECT_3:def 3;
the
carrier of
(Lin B) =
[#] (Lin B)
.=
the
carrier of
((Omega). RNS2)
by Th16, A1, A6, A4
;
then Lin B =
(Omega). RNS2
by A5, RLSUB_1:32
.=
RLSStruct(# the
carrier of
RNS2, the
ZeroF of
RNS2, the
addF of
RNS2, the
Mult of
RNS2 #)
by RLSUB_1:def 4
;
hence
X is
Basis of
RNS2
by A3, RLVECT_3:def 3;
verum
end;
assume
X is Basis of RNS2
; X is Basis of RNS1
then reconsider A = X as Basis of RNS2 ;
reconsider B = A as Subset of RNS1 by A1;
( A is linearly-independent & Lin A = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) )
by RLVECT_3:def 3;
then A8:
B is linearly-independent
by A1, Th17;
set V0 = (Omega). RNS1;
A9:
(Omega). RNS1 = RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #)
by RLSUB_1:def 4;
A10:
Lin B is strict Subspace of (Omega). RNS1
by REAL_NS2:49;
A11:
[#] (Lin A) = the carrier of RNS1
by A1, RLVECT_3:def 3;
the carrier of (Lin B) =
[#] (Lin B)
.=
the carrier of ((Omega). RNS1)
by A9, Th16, A11, A1
;
then Lin B =
(Omega). RNS1
by A10, RLSUB_1:32
.=
RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #)
by RLSUB_1:def 4
;
hence
X is Basis of RNS1
by A8, RLVECT_3:def 3; verum