let X, Y be RealLinearSpace; :: thesis: for T being LinearOperator of X,Y st T is bijective holds

( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

let T be LinearOperator of X,Y; :: thesis: ( T is bijective implies ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X ) )

assume A1: T is bijective ; :: thesis: ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

A2: rng T = the carrier of Y by A1, FUNCT_2:def 3;

A3: dom T = the carrier of X by FUNCT_2:def 1;

T " is LinearOperator of Y,X

( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

let T be LinearOperator of X,Y; :: thesis: ( T is bijective implies ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X ) )

assume A1: T is bijective ; :: thesis: ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )

A2: rng T = the carrier of Y by A1, FUNCT_2:def 3;

A3: dom T = the carrier of X by FUNCT_2:def 1;

T " is LinearOperator of Y,X

proof

hence
( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )
by A1, FUNCT_1:33, A3; :: thesis: verum
reconsider T1 = T " as Function of Y,X by A1, A2, FUNCT_2:25;

A4: T1 is additive

end;A4: T1 is additive

proof

T1 is homogeneous
let y1, y2 be Point of Y; :: according to VECTSP_1:def 19 :: thesis: T1 . (y1 + y2) = (T1 . y1) + (T1 . y2)

consider x1, x2 being Point of X such that

A5: ( T1 . y1 = x1 & T1 . y2 = x2 ) ;

A6: ( T . x1 = y1 & T . x2 = y2 ) by A5, A1, A2, FUNCT_1:32;

x1 + x2 = T1 . (T . (x1 + x2)) by A1, FUNCT_1:32, A3

.= T1 . (y1 + y2) by A6, VECTSP_1:def 20 ;

hence T1 . (y1 + y2) = (T1 . y1) + (T1 . y2) by A5; :: thesis: verum

end;consider x1, x2 being Point of X such that

A5: ( T1 . y1 = x1 & T1 . y2 = x2 ) ;

A6: ( T . x1 = y1 & T . x2 = y2 ) by A5, A1, A2, FUNCT_1:32;

x1 + x2 = T1 . (T . (x1 + x2)) by A1, FUNCT_1:32, A3

.= T1 . (y1 + y2) by A6, VECTSP_1:def 20 ;

hence T1 . (y1 + y2) = (T1 . y1) + (T1 . y2) by A5; :: thesis: verum

proof

hence
T " is LinearOperator of Y,X
by A4; :: thesis: verum
let y1 be Point of Y; :: according to LOPBAN_1:def 5 :: thesis: for b_{1} being object holds T1 . (b_{1} * y1) = b_{1} * (T1 . y1)

let r be Real; :: thesis: T1 . (r * y1) = r * (T1 . y1)

set x1 = T1 . y1;

r * (T1 . y1) = T1 . (T . (r * (T1 . y1))) by A1, FUNCT_1:32, A3

.= T1 . (r * (T . (T1 . y1))) by LOPBAN_1:def 5

.= T1 . (r * y1) by A1, A2, FUNCT_1:32 ;

hence T1 . (r * y1) = r * (T1 . y1) ; :: thesis: verum

end;let r be Real; :: thesis: T1 . (r * y1) = r * (T1 . y1)

set x1 = T1 . y1;

r * (T1 . y1) = T1 . (T . (r * (T1 . y1))) by A1, FUNCT_1:32, A3

.= T1 . (r * (T . (T1 . y1))) by LOPBAN_1:def 5

.= T1 . (r * y1) by A1, A2, FUNCT_1:32 ;

hence T1 . (r * y1) = r * (T1 . y1) ; :: thesis: verum