let n, m be Nat; :: thesis: for p being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
let p be Point of (TOP-REAL n); :: thesis: for M being Matrix of n,m,F_Real
for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
let M be Matrix of n,m,F_Real; :: thesis: for A being Subset of (TOP-REAL n) holds (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
set MT = Mx2Tran M;
let A be Subset of (TOP-REAL n); :: thesis: (Mx2Tran M) .: (p + A) = ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
A1: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
thus (Mx2Tran M) .: (p + A) c= ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) :: according to XBOOLE_0:def 10 :: thesis: ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) c= (Mx2Tran M) .: (p + A)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (Mx2Tran M) .: (p + A) or y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) )
assume y in (Mx2Tran M) .: (p + A) ; :: thesis: y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A)
then consider x being object such that
x in dom (Mx2Tran M) and
A2: x in p + A and
A3: (Mx2Tran M) . x = y by FUNCT_1:def 6;
x in { (p + w) where w is Element of (TOP-REAL n) : w in A } by A2, RUSUB_4:def 8;
then consider w being Element of (TOP-REAL n) such that
A4: ( x = p + w & w in A ) ;
( (Mx2Tran M) . w in (Mx2Tran M) .: A & (Mx2Tran M) . x = ((Mx2Tran M) . p) + ((Mx2Tran M) . w) ) by A1, A4, Th27, FUNCT_1:def 6;
then (Mx2Tran M) . x in { (((Mx2Tran M) . p) + u) where u is Element of (TOP-REAL m) : u in (Mx2Tran M) .: A } ;
hence y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) by A3, RUSUB_4:def 8; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) or y in (Mx2Tran M) .: (p + A) )
assume y in ((Mx2Tran M) . p) + ((Mx2Tran M) .: A) ; :: thesis: y in (Mx2Tran M) .: (p + A)
then y in { (((Mx2Tran M) . p) + u) where u is Element of (TOP-REAL m) : u in (Mx2Tran M) .: A } by RUSUB_4:def 8;
then consider u being Element of (TOP-REAL m) such that
A5: y = ((Mx2Tran M) . p) + u and
A6: u in (Mx2Tran M) .: A ;
consider w being object such that
w in dom (Mx2Tran M) and
A7: w in A and
A8: (Mx2Tran M) . w = u by A6, FUNCT_1:def 6;
reconsider w = w as Element of (TOP-REAL n) by A7;
p + w in { (p + L) where L is Element of (TOP-REAL n) : L in A } by A7;
then A9: p + w in p + A by RUSUB_4:def 8;
y = (Mx2Tran M) . (p + w) by A5, A8, Th27;
hence y in (Mx2Tran M) .: (p + A) by A1, A9, FUNCT_1:def 6; :: thesis: verum