:: MATRIXR1 semantic presentation begin theorem :: MATRIXR1:1 for r1, r2 being Real for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds r1 + r2 = fr1 + fr2 ; theorem :: MATRIXR1:2 for r1, r2 being Real for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds r1 * r2 = fr1 * fr2 ; theorem Th3: :: MATRIXR1:3 for F being FinSequence of REAL holds ( F + (- F) = 0* (len F) & F - F = 0* (len F) ) proof let F be FinSequence of REAL ; ::_thesis: ( F + (- F) = 0* (len F) & F - F = 0* (len F) ) set n = len F; reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92; A1: R + (- R) = (len F) |-> 0 by RVSUM_1:22; hence F + (- F) = 0* (len F) by EUCLID:def_4; ::_thesis: F - F = 0* (len F) thus F - F = 0* (len F) by A1, EUCLID:def_4; ::_thesis: verum end; theorem :: MATRIXR1:4 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 - F2 = F1 + (- F2) ; theorem :: MATRIXR1:5 for F being FinSequence of REAL holds F - (0* (len F)) = F proof let F be FinSequence of REAL ; ::_thesis: F - (0* (len F)) = F set n = len F; reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92; R - ((len F) |-> 0) = R by RVSUM_1:32; hence F - (0* (len F)) = F by EUCLID:def_4; ::_thesis: verum end; theorem :: MATRIXR1:6 for F being FinSequence of REAL holds (0* (len F)) - F = - F proof let F be FinSequence of REAL ; ::_thesis: (0* (len F)) - F = - F set n = len F; reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92; ((len F) |-> 0) - R = - R by RVSUM_1:33; hence (0* (len F)) - F = - F by EUCLID:def_4; ::_thesis: verum end; theorem :: MATRIXR1:7 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 - (- F2) = F1 + F2 ; theorem :: MATRIXR1:8 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds - (F1 - F2) = F2 - F1 by RVSUM_1:35; theorem :: MATRIXR1:9 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds - (F1 - F2) = (- F1) + F2 by RVSUM_1:36; theorem :: MATRIXR1:10 for F1, F2 being FinSequence of REAL st len F1 = len F2 & F1 - F2 = 0* (len F1) holds F1 = F2 proof let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 & F1 - F2 = 0* (len F1) implies F1 = F2 ) set n = len F1; assume len F1 = len F2 ; ::_thesis: ( not F1 - F2 = 0* (len F1) or F1 = F2 ) then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92; ( R1 - R2 = (len F1) |-> 0 implies R1 = R2 ) by RVSUM_1:38; hence ( not F1 - F2 = 0* (len F1) or F1 = F2 ) by EUCLID:def_4; ::_thesis: verum end; theorem :: MATRIXR1:11 for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds (F1 - F2) - F3 = F1 - (F2 + F3) by RVSUM_1:39; theorem :: MATRIXR1:12 for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds F1 + (F2 - F3) = (F1 + F2) - F3 by RVSUM_1:40; theorem :: MATRIXR1:13 for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds F1 - (F2 - F3) = (F1 - F2) + F3 by RVSUM_1:41; theorem Th14: :: MATRIXR1:14 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 = (F1 + F2) - F2 proof let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies F1 = (F1 + F2) - F2 ) set n = len F1; assume len F1 = len F2 ; ::_thesis: F1 = (F1 + F2) - F2 then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92; R1 = (R1 + R2) - R2 by RVSUM_1:42; hence F1 = (F1 + F2) - F2 ; ::_thesis: verum end; theorem :: MATRIXR1:15 for F1, F2 being FinSequence of REAL st len F1 = len F2 holds F1 = (F1 - F2) + F2 proof let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies F1 = (F1 - F2) + F2 ) set n = len F1; assume len F1 = len F2 ; ::_thesis: F1 = (F1 - F2) + F2 then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92; R1 = (R1 - R2) + R2 by RVSUM_1:43; hence F1 = (F1 - F2) + F2 ; ::_thesis: verum end; begin theorem Th16: :: MATRIXR1:16 for K being non empty multMagma for p being FinSequence of K for a being Element of K holds len (a * p) = len p proof let K be non empty multMagma ; ::_thesis: for p being FinSequence of K for a being Element of K holds len (a * p) = len p let p be FinSequence of K; ::_thesis: for a being Element of K holds len (a * p) = len p let a be Element of K; ::_thesis: len (a * p) = len p reconsider q = p as Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92; a * q in (len p) -tuples_on the carrier of K ; then a * q in { s where s is Element of the carrier of K * : len s = len p } by FINSEQ_2:def_4; then ex s being Element of the carrier of K * st ( a * q = s & len s = len p ) ; hence len (a * p) = len p ; ::_thesis: verum end; theorem Th17: :: MATRIXR1:17 for r being Real for fr being Element of F_Real for p being FinSequence of REAL for fp being FinSequence of F_Real st r = fr & p = fp holds r * p = fr * fp proof let r be Real; ::_thesis: for fr being Element of F_Real for p being FinSequence of REAL for fp being FinSequence of F_Real st r = fr & p = fp holds r * p = fr * fp let fr be Element of F_Real; ::_thesis: for p being FinSequence of REAL for fp being FinSequence of F_Real st r = fr & p = fp holds r * p = fr * fp let p be FinSequence of REAL ; ::_thesis: for fp being FinSequence of F_Real st r = fr & p = fp holds r * p = fr * fp let fp be FinSequence of F_Real; ::_thesis: ( r = fr & p = fp implies r * p = fr * fp ) assume that A1: r = fr and A2: p = fp ; ::_thesis: r * p = fr * fp A3: len (r * p) = len fp by A2, RVSUM_1:117; then A4: len (r * p) = len (fr * fp) by Th16; for i being Nat st 1 <= i & i <= len (r * p) holds (r * p) . i = (fr * fp) . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len (r * p) implies (r * p) . i = (fr * fp) . i ) assume ( 1 <= i & i <= len (r * p) ) ; ::_thesis: (r * p) . i = (fr * fp) . i then i in Seg (len fp) by A3, FINSEQ_1:1; then A5: i in dom (fr * fp) by A3, A4, FINSEQ_1:def_3; reconsider s = fp . i as Element of F_Real ; thus (r * p) . i = fr * s by A1, A2, RVSUM_1:44 .= (fr * fp) . i by A5, FVSUM_1:50 ; ::_thesis: verum end; hence r * p = fr * fp by A4, FINSEQ_1:14; ::_thesis: verum end; theorem :: MATRIXR1:18 for K being Field for a being Element of K for A being Matrix of K holds Indices (a * A) = Indices A proof let K be Field; ::_thesis: for a being Element of K for A being Matrix of K holds Indices (a * A) = Indices A let a be Element of K; ::_thesis: for A being Matrix of K holds Indices (a * A) = Indices A let A be Matrix of K; ::_thesis: Indices (a * A) = Indices A ( len (a * A) = len A & width (a * A) = width A ) by MATRIX_3:def_5; hence Indices (a * A) = Indices A by FINSEQ_3:29; ::_thesis: verum end; theorem Th19: :: MATRIXR1:19 for i being Nat for K being Field for a being Element of K for M being Matrix of K st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) proof let i be Nat; ::_thesis: for K being Field for a being Element of K for M being Matrix of K st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) let K be Field; ::_thesis: for a being Element of K for M being Matrix of K st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) let a be Element of K; ::_thesis: for M being Matrix of K st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) let M be Matrix of K; ::_thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) ) assume A1: ( 1 <= i & i <= width M ) ; ::_thesis: Col ((a * M),i) = a * (Col (M,i)) A2: Seg (len (a * M)) = dom (a * M) by FINSEQ_1:def_3; A3: len (a * M) = len M by MATRIX_3:def_5; then A4: dom M = dom (a * M) by FINSEQ_3:29; A5: ( len (a * (Col (M,i))) = len (Col (M,i)) & len (Col (M,i)) = len M ) by Th16, MATRIX_1:def_8; then A6: dom (a * (Col (M,i))) = Seg (len (a * M)) by A3, FINSEQ_1:def_3; for j being Nat st j in dom (a * M) holds (a * (Col (M,i))) . j = (a * M) * (j,i) proof let j be Nat; ::_thesis: ( j in dom (a * M) implies (a * (Col (M,i))) . j = (a * M) * (j,i) ) assume A7: j in dom (a * M) ; ::_thesis: (a * (Col (M,i))) . j = (a * M) * (j,i) i in Seg (width M) by A1, FINSEQ_1:1; then [j,i] in Indices M by A4, A7, ZFMISC_1:87; then A8: (a * M) * (j,i) = a * (M * (j,i)) by MATRIX_3:def_5; (Col (M,i)) . j = M * (j,i) by A4, A7, MATRIX_1:def_8; hence (a * (Col (M,i))) . j = (a * M) * (j,i) by A6, A2, A7, A8, FVSUM_1:50; ::_thesis: verum end; hence Col ((a * M),i) = a * (Col (M,i)) by A5, A3, MATRIX_1:def_8; ::_thesis: verum end; theorem :: MATRIXR1:20 for K being Field for a being Element of K for M being Matrix of K for i being Nat st 1 <= i & i <= len M holds Line ((a * M),i) = a * (Line (M,i)) proof let K be Field; ::_thesis: for a being Element of K for M being Matrix of K for i being Nat st 1 <= i & i <= len M holds Line ((a * M),i) = a * (Line (M,i)) let a be Element of K; ::_thesis: for M being Matrix of K for i being Nat st 1 <= i & i <= len M holds Line ((a * M),i) = a * (Line (M,i)) let M be Matrix of K; ::_thesis: for i being Nat st 1 <= i & i <= len M holds Line ((a * M),i) = a * (Line (M,i)) let i be Nat; ::_thesis: ( 1 <= i & i <= len M implies Line ((a * M),i) = a * (Line (M,i)) ) assume A1: ( 1 <= i & i <= len M ) ; ::_thesis: Line ((a * M),i) = a * (Line (M,i)) A2: width (a * M) = width M by MATRIX_3:def_5; A3: Seg (width M) = Seg (width (a * M)) by MATRIX_3:def_5; A4: ( len (a * (Line (M,i))) = len (Line (M,i)) & len (Line (M,i)) = width M ) by Th16, MATRIX_1:def_7; then A5: dom (a * (Line (M,i))) = Seg (width (a * M)) by A2, FINSEQ_1:def_3; for j being Nat st j in Seg (width (a * M)) holds (a * (Line (M,i))) . j = (a * M) * (i,j) proof let j be Nat; ::_thesis: ( j in Seg (width (a * M)) implies (a * (Line (M,i))) . j = (a * M) * (i,j) ) assume A6: j in Seg (width (a * M)) ; ::_thesis: (a * (Line (M,i))) . j = (a * M) * (i,j) i in dom M by A1, FINSEQ_3:25; then [i,j] in Indices M by A3, A6, ZFMISC_1:87; then A7: (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def_5; (Line (M,i)) . j = M * (i,j) by A3, A6, MATRIX_1:def_7; hence (a * (Line (M,i))) . j = (a * M) * (i,j) by A5, A6, A7, FVSUM_1:50; ::_thesis: verum end; hence Line ((a * M),i) = a * (Line (M,i)) by A4, A2, MATRIX_1:def_7; ::_thesis: verum end; theorem :: MATRIXR1:21 for K being Field for A, B being Matrix of K st width A = len B holds ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) proof let K be Field; ::_thesis: for A, B being Matrix of K st width A = len B holds ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) let A, B be Matrix of K; ::_thesis: ( width A = len B implies ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) ) assume A1: width A = len B ; ::_thesis: ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) deffunc H1( Nat, Nat) -> Element of the carrier of K = (Line (A,\$1)) "*" (Col (B,\$2)); consider M being Matrix of len A, width B, the carrier of K such that A2: for i, j being Nat st [i,j] in Indices M holds M * (i,j) = H1(i,j) from MATRIX_1:sch_1(); percases ( len A > 0 or len A = 0 ) ; suppose len A > 0 ; ::_thesis: ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) then ( len M = len A & width M = width B ) by MATRIX_1:23; hence ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2; ::_thesis: verum end; supposeA3: len A = 0 ; ::_thesis: ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) then A4: len M = 0 by MATRIX_1:25; len B = 0 by A1, A3, MATRIX_1:def_3; then width B = 0 by MATRIX_1:def_3; then width M = width B by A4, MATRIX_1:def_3; hence ex C being Matrix of K st ( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2, A3, A4; ::_thesis: verum end; end; end; theorem Th22: :: MATRIXR1:22 for K being Field for a being Element of K for A, B being Matrix of K st width A = len B holds A * (a * B) = a * (A * B) proof let K be Field; ::_thesis: for a being Element of K for A, B being Matrix of K st width A = len B holds A * (a * B) = a * (A * B) let a be Element of K; ::_thesis: for A, B being Matrix of K st width A = len B holds A * (a * B) = a * (A * B) let A, B be Matrix of K; ::_thesis: ( width A = len B implies A * (a * B) = a * (A * B) ) set C = a * B; set D = a * (A * B); A1: len (a * (A * B)) = len (A * B) by MATRIX_3:def_5; assume A2: width A = len B ; ::_thesis: A * (a * B) = a * (A * B) then width (A * B) = width B by MATRIX_3:def_4; then A3: width (a * (A * B)) = width B by MATRIX_3:def_5 .= width (a * B) by MATRIX_3:def_5 ; A4: width B = width (a * B) by MATRIX_3:def_5; A5: for i, j being Nat st [i,j] in Indices (a * (A * B)) holds (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) ) reconsider xo = Col (B,j) as Element of (width A) -tuples_on the carrier of K by A2; assume A6: [i,j] in Indices (a * (A * B)) ; ::_thesis: (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) then j in Seg (width B) by A4, A3, ZFMISC_1:87; then A7: ( 1 <= j & j <= width B ) by FINSEQ_1:1; dom (A * B) = dom (a * (A * B)) by A1, FINSEQ_3:29; then A8: [i,j] in Indices (A * B) by A6, MATRIX_3:def_5; then (a * (A * B)) * (i,j) = a * ((A * B) * (i,j)) by MATRIX_3:def_5; then (a * (A * B)) * (i,j) = a * ((Line (A,i)) "*" (Col (B,j))) by A2, A8, MATRIX_3:def_4 .= a * (Sum (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:def_9 .= Sum (a * (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:73 .= Sum (mlt ((Line (A,i)),(a * xo))) by FVSUM_1:69 .= Sum (mlt ((Line (A,i)),(Col ((a * B),j)))) by A7, Th19 ; hence (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) by FVSUM_1:def_9; ::_thesis: verum end; ( len (a * B) = len B & len (A * B) = len A ) by A2, MATRIX_3:def_4, MATRIX_3:def_5; hence A * (a * B) = a * (A * B) by A2, A1, A3, A5, MATRIX_3:def_4; ::_thesis: verum end; definition let A be Matrix of REAL; func MXR2MXF A -> Matrix of F_Real equals :: MATRIXR1:def 1 A; coherence A is Matrix of F_Real ; end; :: deftheorem defines MXR2MXF MATRIXR1:def_1_:_ for A being Matrix of REAL holds MXR2MXF A = A; definition let A be Matrix of F_Real; func MXF2MXR A -> Matrix of REAL equals :: MATRIXR1:def 2 A; coherence A is Matrix of REAL ; end; :: deftheorem defines MXF2MXR MATRIXR1:def_2_:_ for A being Matrix of F_Real holds MXF2MXR A = A; theorem :: MATRIXR1:23 for D1, D2 being set for A being Matrix of D1 for B being Matrix of D2 st A = B holds for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) proof let D1, D2 be set ; ::_thesis: for A being Matrix of D1 for B being Matrix of D2 st A = B holds for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) let A be Matrix of D1; ::_thesis: for B being Matrix of D2 st A = B holds for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) let B be Matrix of D2; ::_thesis: ( A = B implies for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) ) assume A1: A = B ; ::_thesis: for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) ) assume A2: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j) then A3: ex p being FinSequence of D1 st ( p = A . i & A * (i,j) = p . j ) by MATRIX_1:def_5; ex q being FinSequence of D2 st ( q = B . i & B * (i,j) = q . j ) by A1, A2, MATRIX_1:def_5; hence A * (i,j) = B * (i,j) by A1, A3; ::_thesis: verum end; theorem :: MATRIXR1:24 for K being Field for A, B being Matrix of K holds Indices (A + B) = Indices A proof let K be Field; ::_thesis: for A, B being Matrix of K holds Indices (A + B) = Indices A let A, B be Matrix of K; ::_thesis: Indices (A + B) = Indices A ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def_3; hence Indices (A + B) = Indices A by MATRIX_4:55; ::_thesis: verum end; definition let A, B be Matrix of REAL; funcA + B -> Matrix of REAL equals :: MATRIXR1:def 3 MXF2MXR ((MXR2MXF A) + (MXR2MXF B)); coherence MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) is Matrix of REAL ; end; :: deftheorem defines + MATRIXR1:def_3_:_ for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B)); theorem Th25: :: MATRIXR1:25 for A, B being Matrix of REAL holds ( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) proof let A, B be Matrix of REAL; ::_thesis: ( len (A + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) thus ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def_3; ::_thesis: for i, j being Nat st [i,j] in Indices A holds (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) assume [i,j] in Indices A ; ::_thesis: (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) then (A + B) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j)) by MATRIX_3:def_3; hence (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: verum end; theorem Th26: :: MATRIXR1:26 for A, B, C being Matrix of REAL st len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds C = A + B proof let A, B, C be Matrix of REAL; ::_thesis: ( len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) + (B * (i,j)) ) implies C = A + B ) assume that A1: ( len C = len A & width C = width A ) and A2: for i, j being Nat st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: C = A + B set B2 = MXR2MXF B; set A2 = MXR2MXF A; set D = MXR2MXF C; for i, j being Nat st [i,j] in Indices (MXR2MXF A) holds (MXR2MXF C) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j)) by A2; hence C = A + B by A1, MATRIX_3:def_3; ::_thesis: verum end; definition let A be Matrix of REAL; func - A -> Matrix of REAL equals :: MATRIXR1:def 4 MXF2MXR (- (MXR2MXF A)); coherence MXF2MXR (- (MXR2MXF A)) is Matrix of REAL ; end; :: deftheorem defines - MATRIXR1:def_4_:_ for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A)); definition let A, B be Matrix of REAL; funcA - B -> Matrix of REAL equals :: MATRIXR1:def 5 MXF2MXR ((MXR2MXF A) - (MXR2MXF B)); coherence MXF2MXR ((MXR2MXF A) - (MXR2MXF B)) is Matrix of REAL ; funcA * B -> Matrix of REAL equals :: MATRIXR1:def 6 MXF2MXR ((MXR2MXF A) * (MXR2MXF B)); coherence MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) is Matrix of REAL ; end; :: deftheorem defines - MATRIXR1:def_5_:_ for A, B being Matrix of REAL holds A - B = MXF2MXR ((MXR2MXF A) - (MXR2MXF B)); :: deftheorem defines * MATRIXR1:def_6_:_ for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B)); definition let a be real number ; let A be Matrix of REAL; funca * A -> Matrix of REAL means :Def7: :: MATRIXR1:def 7 for ea being Element of F_Real st ea = a holds it = MXF2MXR (ea * (MXR2MXF A)); existence ex b1 being Matrix of REAL st for ea being Element of F_Real st ea = a holds b1 = MXF2MXR (ea * (MXR2MXF A)) proof reconsider aa = a as Element of F_Real by XREAL_0:def_1; set C = MXF2MXR (aa * (MXR2MXF A)); for ea being Element of F_Real st ea = a holds MXF2MXR (aa * (MXR2MXF A)) = MXF2MXR (ea * (MXR2MXF A)) ; hence ex b1 being Matrix of REAL st for ea being Element of F_Real st ea = a holds b1 = MXF2MXR (ea * (MXR2MXF A)) ; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds b1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds b2 = MXF2MXR (ea * (MXR2MXF A)) ) holds b1 = b2 proof reconsider aa = a as Element of F_Real by XREAL_0:def_1; let C1, C2 be Matrix of REAL; ::_thesis: ( ( for ea being Element of F_Real st ea = a holds C1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds C2 = MXF2MXR (ea * (MXR2MXF A)) ) implies C1 = C2 ) assume that A1: for ea being Element of F_Real st ea = a holds C1 = MXF2MXR (ea * (MXR2MXF A)) and A2: for ea being Element of F_Real st ea = a holds C2 = MXF2MXR (ea * (MXR2MXF A)) ; ::_thesis: C1 = C2 C2 = MXF2MXR (aa * (MXR2MXF A)) by A2; hence C1 = C2 by A1; ::_thesis: verum end; end; :: deftheorem Def7 defines * MATRIXR1:def_7_:_ for a being real number for A, b3 being Matrix of REAL holds ( b3 = a * A iff for ea being Element of F_Real st ea = a holds b3 = MXF2MXR (ea * (MXR2MXF A)) ); theorem Th27: :: MATRIXR1:27 for a being Real for A being Matrix of REAL holds ( len (a * A) = len A & width (a * A) = width A ) proof let a be Real; ::_thesis: for A being Matrix of REAL holds ( len (a * A) = len A & width (a * A) = width A ) let A be Matrix of REAL; ::_thesis: ( len (a * A) = len A & width (a * A) = width A ) reconsider ea = a as Element of F_Real ; thus len (a * A) = len (MXF2MXR (ea * (MXR2MXF A))) by Def7 .= len A by MATRIX_3:def_5 ; ::_thesis: width (a * A) = width A thus width (a * A) = width (MXF2MXR (ea * (MXR2MXF A))) by Def7 .= width A by MATRIX_3:def_5 ; ::_thesis: verum end; theorem Th28: :: MATRIXR1:28 for a being Real for A being Matrix of REAL holds Indices (a * A) = Indices A proof let a be Real; ::_thesis: for A being Matrix of REAL holds Indices (a * A) = Indices A let A be Matrix of REAL; ::_thesis: Indices (a * A) = Indices A ( len A = len (a * A) & width (a * A) = width A ) by Th27; hence Indices (a * A) = Indices A by MATRIX_4:55; ::_thesis: verum end; theorem Th29: :: MATRIXR1:29 for a being Real for A being Matrix of REAL for i2, j2 being Nat st [i2,j2] in Indices A holds (a * A) * (i2,j2) = a * (A * (i2,j2)) proof let a be Real; ::_thesis: for A being Matrix of REAL for i2, j2 being Nat st [i2,j2] in Indices A holds (a * A) * (i2,j2) = a * (A * (i2,j2)) let A be Matrix of REAL; ::_thesis: for i2, j2 being Nat st [i2,j2] in Indices A holds (a * A) * (i2,j2) = a * (A * (i2,j2)) let i2, j2 be Nat; ::_thesis: ( [i2,j2] in Indices A implies (a * A) * (i2,j2) = a * (A * (i2,j2)) ) reconsider ea = a as Element of F_Real ; assume [i2,j2] in Indices A ; ::_thesis: (a * A) * (i2,j2) = a * (A * (i2,j2)) then (MXF2MXR (ea * (MXR2MXF A))) * (i2,j2) = ea * ((MXR2MXF A) * (i2,j2)) by MATRIX_3:def_5 .= a * (A * (i2,j2)) ; hence (a * A) * (i2,j2) = a * (A * (i2,j2)) by Def7; ::_thesis: verum end; theorem Th30: :: MATRIXR1:30 for a being Real for A being Matrix of REAL st width A > 0 holds (a * A) @ = a * (A @) proof let a be Real; ::_thesis: for A being Matrix of REAL st width A > 0 holds (a * A) @ = a * (A @) let A be Matrix of REAL; ::_thesis: ( width A > 0 implies (a * A) @ = a * (A @) ) assume width A > 0 ; ::_thesis: (a * A) @ = a * (A @) then A1: len (A @) = width A by MATRIX_2:10; A2: for i, j being Nat holds ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) ) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) ) ( Indices (a * (A @)) = Indices (A @) & Indices (a * A) = Indices A ) by Th28; hence ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) ) by MATRIX_1:def_6; ::_thesis: verum end; A3: for i, j being Nat st [j,i] in Indices (a * A) holds (a * (A @)) * (i,j) = (a * A) * (j,i) proof let i, j be Nat; ::_thesis: ( [j,i] in Indices (a * A) implies (a * (A @)) * (i,j) = (a * A) * (j,i) ) assume [j,i] in Indices (a * A) ; ::_thesis: (a * (A @)) * (i,j) = (a * A) * (j,i) then A4: [j,i] in Indices A by Th28; then [i,j] in Indices (A @) by MATRIX_1:def_6; then (a * (A @)) * (i,j) = a * ((A @) * (i,j)) by Th29; then (a * (A @)) * (i,j) = a * (A * (j,i)) by A4, MATRIX_1:def_6 .= (a * A) * (j,i) by A4, Th29 ; hence (a * (A @)) * (i,j) = (a * A) * (j,i) ; ::_thesis: verum end; ( len (a * (A @)) = len (A @) & width A = width (a * A) ) by Th27; hence (a * A) @ = a * (A @) by A1, A2, A3, MATRIX_1:def_6; ::_thesis: verum end; theorem :: MATRIXR1:31 for a being Real for i being Nat for A being Matrix of REAL st len A > 0 & i in dom A holds ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q ) ) proof let a be Real; ::_thesis: for i being Nat for A being Matrix of REAL st len A > 0 & i in dom A holds ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q ) ) let i be Nat; ::_thesis: for A being Matrix of REAL st len A > 0 & i in dom A holds ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q ) ) let A be Matrix of REAL; ::_thesis: ( len A > 0 & i in dom A implies ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q ) ) ) assume that A1: len A > 0 and A2: i in dom A ; ::_thesis: ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q ) ) consider n3 being Nat such that A3: for x being set st x in rng A holds ex s2 being FinSequence st ( s2 = x & len s2 = n3 ) by MATRIX_1:def_1; A . i in rng A by A2, FUNCT_1:def_3; then A4: ex qq0 being FinSequence st ( qq0 = A . i & len qq0 = n3 ) by A3; len (a * A) = len A by Th27; then consider s being FinSequence such that A5: s in rng (a * A) and A6: len s = width (a * A) by A1, MATRIX_1:def_3; A7: width (a * A) = width A by Th27; consider s3 being FinSequence such that A8: s3 in rng A and A9: len s3 = width A by A1, MATRIX_1:def_3; consider n2 being Nat such that A10: for x being set st x in rng (a * A) holds ex s2 being FinSequence st ( s2 = x & len s2 = n2 ) by MATRIX_1:def_1; len (a * A) = len A by Th27; then A11: dom (a * A) = dom A by FINSEQ_3:29; then (a * A) . i in rng (a * A) by A2, FUNCT_1:def_3; then consider qq being FinSequence such that A12: qq = (a * A) . i and A13: len qq = n2 by A10; consider n being Nat such that A14: for x being set st x in rng A holds ex p being FinSequence of REAL st ( x = p & len p = n ) by MATRIX_1:9; A . i in rng A by A2, FUNCT_1:def_3; then ex p2 being FinSequence of REAL st ( A . i = p2 & len p2 = n ) by A14; hence ex p being FinSequence of REAL st p = A . i ; ::_thesis: for q being FinSequence of REAL st q = A . i holds (a * A) . i = a * q let q be FinSequence of REAL ; ::_thesis: ( q = A . i implies (a * A) . i = a * q ) assume A15: q = A . i ; ::_thesis: (a * A) . i = a * q A16: ex s4 being FinSequence st ( s4 = s3 & len s4 = n3 ) by A8, A3; then A17: len (a * q) = width A by A15, A9, A4, RVSUM_1:117; A18: for j being Nat st 1 <= j & j <= len (a * q) holds qq . j = (a * q) . j proof let j be Nat; ::_thesis: ( 1 <= j & j <= len (a * q) implies qq . j = (a * q) . j ) assume ( 1 <= j & j <= len (a * q) ) ; ::_thesis: qq . j = (a * q) . j then A19: j in Seg (width A) by A17, FINSEQ_1:1; then A20: [i,j] in Indices A by A2, ZFMISC_1:87; reconsider j = j as Element of NAT by ORDINAL1:def_12; [i,j] in Indices (a * A) by A2, A7, A11, A19, ZFMISC_1:87; then A21: ex p being FinSequence of REAL st ( p = (a * A) . i & (a * A) * (i,j) = p . j ) by MATRIX_1:def_5; ex p2 being FinSequence of REAL st ( p2 = A . i & A * (i,j) = p2 . j ) by A20, MATRIX_1:def_5; then qq . j = a * (q . j) by A15, A12, A20, A21, Th29; hence qq . j = (a * q) . j by RVSUM_1:44; ::_thesis: verum end; ex s2 being FinSequence st ( s2 = s & len s2 = n2 ) by A5, A10; then width A = len qq by A6, A13, Th27; hence (a * A) . i = a * q by A15, A9, A16, A12, A4, A18, FINSEQ_1:14, RVSUM_1:117; ::_thesis: verum end; theorem :: MATRIXR1:32 for A being Matrix of REAL holds 1 * A = A proof let A be Matrix of REAL; ::_thesis: 1 * A = A 1 * A = MXF2MXR ((1_ F_Real) * (MXR2MXF A)) by Def7; hence 1 * A = A by MATRIX_5:9; ::_thesis: verum end; theorem :: MATRIXR1:33 for A being Matrix of REAL holds A + A = 2 * A proof set e2 = (1_ F_Real) + (1_ F_Real); let A be Matrix of REAL; ::_thesis: A + A = 2 * A A1: (1_ F_Real) * (MXR2MXF A) = MXR2MXF A by MATRIX_5:9; 2 * A = MXF2MXR (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A)) by Def7 .= MXF2MXR ((MXR2MXF A) + (MXR2MXF A)) by A1, MATRIX_5:12 ; hence A + A = 2 * A ; ::_thesis: verum end; theorem :: MATRIXR1:34 for A being Matrix of REAL holds (A + A) + A = 3 * A proof reconsider e3 = ((1_ F_Real) + (1_ F_Real)) + (1_ F_Real) as Element of F_Real ; let A be Matrix of REAL; ::_thesis: (A + A) + A = 3 * A A1: ( len A = len (MXR2MXF A) & width A = width (MXR2MXF A) ) ; 3 * A = MXF2MXR (e3 * (MXR2MXF A)) by Def7 .= MXF2MXR (((1_ F_Real) * (MXR2MXF A)) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:12 .= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:9 .= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) * (MXR2MXF A)) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:12 .= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:9 .= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + (MXR2MXF A))) by MATRIX_5:9 .= MXF2MXR (((MXR2MXF A) + (MXR2MXF A)) + (MXR2MXF A)) by A1, MATRIX_3:3 ; hence (A + A) + A = 3 * A ; ::_thesis: verum end; definition let n, m be Nat; func 0_Rmatrix (n,m) -> Matrix of REAL equals :: MATRIXR1:def 8 MXF2MXR (0. (F_Real,n,m)); coherence MXF2MXR (0. (F_Real,n,m)) is Matrix of REAL ; end; :: deftheorem defines 0_Rmatrix MATRIXR1:def_8_:_ for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m)); theorem :: MATRIXR1:35 for A, B being Matrix of REAL holds A - (- B) = A + B proof let A, B be Matrix of REAL; ::_thesis: A - (- B) = A + B A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF (- (- B)))) by MATRIX_4:1; hence A - (- B) = A + B by MATRIX_4:def_1; ::_thesis: verum end; theorem Th36: :: MATRIXR1:36 for n, m being Nat for A being Matrix of REAL st len A = n & width A = m & n > 0 holds ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) proof let n, m be Nat; ::_thesis: for A being Matrix of REAL st len A = n & width A = m & n > 0 holds ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) let A be Matrix of REAL; ::_thesis: ( len A = n & width A = m & n > 0 implies ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) ) assume that A1: ( len A = n & width A = m ) and A2: n > 0 ; ::_thesis: ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) reconsider D = MXR2MXF A as Matrix of n,m,F_Real by A1, A2, MATRIX_1:20; ( len (0. (F_Real,n,m)) = n & width (0. (F_Real,n,m)) = m ) by A2, MATRIX_1:23; then A3: (0_Rmatrix (n,m)) + A = MXF2MXR (D + (0. (F_Real,n,m))) by A1, MATRIX_3:2 .= A by MATRIX_3:4 ; MXR2MXF A is Matrix of n,m,F_Real by A1, A2, MATRIX_1:20; hence ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) by A3, MATRIX_3:4; ::_thesis: verum end; theorem :: MATRIXR1:37 for A, B being Matrix of REAL st len A = len B & width A = width B & A = A + B holds B = 0_Rmatrix ((len A),(width A)) proof let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & A = A + B implies B = 0_Rmatrix ((len A),(width A)) ) assume that A1: ( len A = len B & width A = width B ) and A2: A = A + B ; ::_thesis: B = 0_Rmatrix ((len A),(width A)) 0_Rmatrix ((len A),(width A)) = (A + B) + (- A) by A2, MATRIX_4:2 .= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) + (- (MXR2MXF A))) by A1, MATRIX_3:2 .= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) - (MXR2MXF A)) by MATRIX_4:def_1 .= B by A1, MATRIX_4:21 ; hence B = 0_Rmatrix ((len A),(width A)) ; ::_thesis: verum end; theorem :: MATRIXR1:38 for A, B being Matrix of REAL st len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) holds B = - A proof let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) implies B = - A ) assume that A1: ( len A = len B & width A = width B ) and A2: A + B = 0_Rmatrix ((len A),(width A)) ; ::_thesis: B = - A A3: ( len (- (MXR2MXF B)) = len (MXR2MXF B) & width (- (MXR2MXF B)) = width (MXR2MXF B) ) by MATRIX_3:def_2; MXR2MXF (0_Rmatrix ((len A),(width A))) = (MXR2MXF A) + (- (- (MXR2MXF B))) by A2, MATRIX_4:1 .= (MXR2MXF A) - (- (MXR2MXF B)) by MATRIX_4:def_1 ; then MXR2MXF A = - (MXR2MXF B) by A1, A3, MATRIX_4:7; hence B = - A by MATRIX_4:1; ::_thesis: verum end; theorem :: MATRIXR1:39 for A, B being Matrix of REAL st len A = len B & width A = width B & B - A = B holds A = 0_Rmatrix ((len A),(width A)) proof let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & B - A = B implies A = 0_Rmatrix ((len A),(width A)) ) assume that A1: ( len A = len B & width A = width B ) and A2: B - A = B ; ::_thesis: A = 0_Rmatrix ((len A),(width A)) (MXR2MXF B) + (MXR2MXF A) = MXR2MXF B by A1, A2, MATRIX_4:22; hence A = 0_Rmatrix ((len A),(width A)) by A1, MATRIX_4:6; ::_thesis: verum end; theorem Th40: :: MATRIXR1:40 for a being Real for A, B being Matrix of REAL st width A = len B holds A * (a * B) = a * (A * B) proof let a be Real; ::_thesis: for A, B being Matrix of REAL st width A = len B holds A * (a * B) = a * (A * B) let A, B be Matrix of REAL; ::_thesis: ( width A = len B implies A * (a * B) = a * (A * B) ) assume A1: width A = len B ; ::_thesis: A * (a * B) = a * (A * B) reconsider ea = a as Element of F_Real ; thus A * (a * B) = MXF2MXR ((MXR2MXF A) * (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7 .= MXF2MXR (ea * (MXR2MXF (MXF2MXR ((MXR2MXF A) * (MXR2MXF B))))) by A1, Th22 .= a * (A * B) by Def7 ; ::_thesis: verum end; theorem :: MATRIXR1:41 for a being Real for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds (a * A) * B = a * (A * B) proof let a be Real; ::_thesis: for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds (a * A) * B = a * (A * B) let A, B be Matrix of REAL; ::_thesis: ( width A = len B & len A > 0 & len B > 0 & width B > 0 implies (a * A) * B = a * (A * B) ) assume that A1: width A = len B and A2: len A > 0 and A3: len B > 0 and A4: width B > 0 ; ::_thesis: (a * A) * B = a * (A * B) ( len (A @) = width A & width (B @) = len B ) by A1, A3, A4, MATRIX_2:10; then (B @) * (a * (A @)) = a * ((B @) * (A @)) by A1, Th40; then A5: (B @) * (a * (A @)) = a * ((A * B) @) by A1, A4, MATRIX_3:22; A6: width (a * (A * B)) = width (A * B) by Th27 .= width B by A1, MATRIX_3:def_4 ; A7: len (a * (A * B)) = len (A * B) by Th27 .= len A by A1, MATRIX_3:def_4 ; A8: len (a * A) = len A by Th27; A9: width (a * A) = width A by Th27; width (A * B) = width B by A1, MATRIX_3:def_4; then (B @) * (a * (A @)) = (a * (A * B)) @ by A4, A5, Th30; then (B @) * ((a * A) @) = (a * (A * B)) @ by A1, A3, Th30; then A10: ((a * A) * B) @ = (a * (A * B)) @ by A1, A4, A9, MATRIX_3:22; ( len ((a * A) * B) = len (a * A) & width ((a * A) * B) = width B ) by A1, A9, MATRIX_3:def_4; then (a * A) * B = ((a * (A * B)) @) @ by A2, A4, A8, A10, MATRIX_2:13; hence (a * A) * B = a * (A * B) by A2, A4, A7, A6, MATRIX_2:13; ::_thesis: verum end; theorem :: MATRIXR1:42 for M being Matrix of REAL holds M + (0_Rmatrix ((len M),(width M))) = M proof let M be Matrix of REAL; ::_thesis: M + (0_Rmatrix ((len M),(width M))) = M A1: ( len M = len (MXR2MXF M) & width M = width (MXR2MXF M) ) ; M + (0_Rmatrix ((len M),(width M))) = M + (- (0_Rmatrix ((len M),(width M)))) by MATRIX_4:9 .= M + (- (M - M)) by MATRIX_4:3 .= MXF2MXR ((MXR2MXF M) - ((MXR2MXF M) - (MXR2MXF M))) by MATRIX_4:def_1 .= M by A1, MATRIX_4:11 ; hence M + (0_Rmatrix ((len M),(width M))) = M ; ::_thesis: verum end; theorem :: MATRIXR1:43 for a being real number for A, B being Matrix of REAL st len A = len B & width A = width B holds a * (A + B) = (a * A) + (a * B) proof let a be real number ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B holds a * (A + B) = (a * A) + (a * B) let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B implies a * (A + B) = (a * A) + (a * B) ) assume A1: ( len A = len B & width A = width B ) ; ::_thesis: a * (A + B) = (a * A) + (a * B) reconsider ea = a as Element of F_Real by XREAL_0:def_1; A2: (a * A) + (a * B) = MXF2MXR ((MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) + (MXR2MXF (a * B))) by Def7 .= MXF2MXR ((ea * (MXR2MXF A)) + (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7 .= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) ; a * (A + B) = MXF2MXR (ea * (MXR2MXF (A + B))) by Def7 .= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) by A1, MATRIX_5:20 ; hence a * (A + B) = (a * A) + (a * B) by A2; ::_thesis: verum end; theorem :: MATRIXR1:44 for A being Matrix of REAL st len A > 0 holds 0 * A = 0_Rmatrix ((len A),(width A)) proof let A be Matrix of REAL; ::_thesis: ( len A > 0 implies 0 * A = 0_Rmatrix ((len A),(width A)) ) assume A1: len A > 0 ; ::_thesis: 0 * A = 0_Rmatrix ((len A),(width A)) 0 * A = MXF2MXR ((0. F_Real) * (MXR2MXF A)) by Def7 .= 0_Rmatrix ((len A),(width A)) by A1, MATRIX_5:24 ; hence 0 * A = 0_Rmatrix ((len A),(width A)) ; ::_thesis: verum end; definition let x be FinSequence of REAL ; assume A1: len x > 0 ; func ColVec2Mx x -> Matrix of REAL means :Def9: :: MATRIXR1:def 9 ( len it = len x & width it = 1 & ( for j being Nat st j in dom x holds it . j = <*(x . j)*> ) ); existence ex b1 being Matrix of REAL st ( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds b1 . j = <*(x . j)*> ) ) proof reconsider n = len x as Element of NAT ; deffunc H1( Nat) -> FinSequence of REAL = <*(x . \$1)*>; consider C being FinSequence such that A2: ( len C = n & ( for j being Nat st j in dom C holds C . j = H1(j) ) ) from FINSEQ_1:sch_2(); for y being set st y in rng C holds ex p being FinSequence of REAL st ( y = p & len p = 1 ) proof let y be set ; ::_thesis: ( y in rng C implies ex p being FinSequence of REAL st ( y = p & len p = 1 ) ) assume y in rng C ; ::_thesis: ex p being FinSequence of REAL st ( y = p & len p = 1 ) then consider z being set such that A3: z in dom C and A4: y = C . z by FUNCT_1:def_3; reconsider z = z as Element of NAT by A3; len <*(x . z)*> = 1 by FINSEQ_1:39; hence ex p being FinSequence of REAL st ( y = p & len p = 1 ) by A2, A3, A4; ::_thesis: verum end; then reconsider B = C as Matrix of REAL by MATRIX_1:9; for p being FinSequence of REAL st p in rng B holds len p = 1 proof let p be FinSequence of REAL ; ::_thesis: ( p in rng B implies len p = 1 ) assume p in rng B ; ::_thesis: len p = 1 then consider i being Nat such that A5: ( i in dom B & B . i = p ) by FINSEQ_2:10; len <*(x . i)*> = 1 by FINSEQ_1:39; hence len p = 1 by A2, A5; ::_thesis: verum end; then reconsider A = B as Matrix of len B,1, REAL by MATRIX_1:def_2; A6: Seg (len x) = dom x by FINSEQ_1:def_3; ( dom C = Seg n & width A = 1 ) by A1, A2, FINSEQ_1:def_3, MATRIX_1:23; hence ex b1 being Matrix of REAL st ( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds b1 . j = <*(x . j)*> ) ) by A2, A6; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds b2 . j = <*(x . j)*> ) holds b1 = b2 proof let A, B be Matrix of REAL; ::_thesis: ( len A = len x & width A = 1 & ( for j being Nat st j in dom x holds A . j = <*(x . j)*> ) & len B = len x & width B = 1 & ( for j being Nat st j in dom x holds B . j = <*(x . j)*> ) implies A = B ) assume that A7: len A = len x and width A = 1 and A8: for k being Nat st k in dom x holds A . k = <*(x . k)*> and A9: len B = len x and width B = 1 and A10: for k being Nat st k in dom x holds B . k = <*(x . k)*> ; ::_thesis: A = B A11: now__::_thesis:_for_k_being_Nat_st_k_in_dom_x_holds_ A_._k_=_B_._k let k be Nat; ::_thesis: ( k in dom x implies A . k = B . k ) assume A12: k in dom x ; ::_thesis: A . k = B . k hence A . k = <*(x . k)*> by A8 .= B . k by A10, A12 ; ::_thesis: verum end; ( dom A = dom x & dom B = dom x ) by A7, A9, FINSEQ_3:29; hence A = B by A11, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def9 defines ColVec2Mx MATRIXR1:def_9_:_ for x being FinSequence of REAL st len x > 0 holds for b2 being Matrix of REAL holds ( b2 = ColVec2Mx x iff ( len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds b2 . j = <*(x . j)*> ) ) ); theorem :: MATRIXR1:45 for x being FinSequence of REAL for M being Matrix of REAL st len x > 0 holds ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) proof let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x > 0 holds ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) let M be Matrix of REAL; ::_thesis: ( len x > 0 implies ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) ) consider n being Nat such that A1: for x being set st x in rng M holds ex s2 being FinSequence st ( s2 = x & len s2 = n ) by MATRIX_1:def_1; assume A2: len x > 0 ; ::_thesis: ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) thus ( M = ColVec2Mx x implies ( Col (M,1) = x & width M = 1 ) ) ::_thesis: ( Col (M,1) = x & width M = 1 implies M = ColVec2Mx x ) proof assume A3: M = ColVec2Mx x ; ::_thesis: ( Col (M,1) = x & width M = 1 ) then A4: width M = 1 by A2, Def9; A5: len M = len x by A2, A3, Def9; then A6: dom M = dom x by FINSEQ_3:29; for j being Nat st j in dom M holds x . j = M * (j,1) proof let j be Nat; ::_thesis: ( j in dom M implies x . j = M * (j,1) ) assume A7: j in dom M ; ::_thesis: x . j = M * (j,1) then reconsider j = j as Element of NAT ; A8: M . j = <*(x . j)*> by A2, A3, A6, A7, Def9; then reconsider q = M . j as FinSequence of REAL ; A9: q . 1 = x . j by A8, FINSEQ_1:40; 1 in Seg (width M) by A4, FINSEQ_1:1; then [j,1] in Indices M by A7, ZFMISC_1:87; hence x . j = M * (j,1) by A9, MATRIX_1:def_5; ::_thesis: verum end; hence ( Col (M,1) = x & width M = 1 ) by A2, A3, A5, Def9, MATRIX_1:def_8; ::_thesis: verum end; assume that A10: Col (M,1) = x and A11: width M = 1 ; ::_thesis: M = ColVec2Mx x A12: len x = len M by A10, MATRIX_1:def_8; then consider s being FinSequence such that A13: s in rng M and A14: len s = 1 by A2, A11, MATRIX_1:def_3; A15: dom x = dom M by A12, FINSEQ_3:29; A16: ex s2 being FinSequence st ( s2 = s & len s2 = n ) by A13, A1; for j being Nat st j in dom x holds M . j = <*(x . j)*> proof let j be Nat; ::_thesis: ( j in dom x implies M . j = <*(x . j)*> ) assume A17: j in dom x ; ::_thesis: M . j = <*(x . j)*> then M . j in rng M by A15, FUNCT_1:def_3; then A18: ex s3 being FinSequence st ( s3 = M . j & len s3 = 1 ) by A14, A1, A16; 1 in Seg (width M) by A11, FINSEQ_1:1; then [j,1] in Indices M by A15, A17, ZFMISC_1:87; then A19: ex p being FinSequence of REAL st ( p = M . j & M * (j,1) = p . 1 ) by MATRIX_1:def_5; x . j = M * (j,1) by A10, A15, A17, MATRIX_1:def_8; hence M . j = <*(x . j)*> by A19, A18, FINSEQ_1:40; ::_thesis: verum end; hence M = ColVec2Mx x by A2, A11, A12, Def9; ::_thesis: verum end; theorem Th46: :: MATRIXR1:46 for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) proof let x1, x2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 & len x1 > 0 implies ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) ) assume that A1: len x1 = len x2 and A2: len x1 > 0 ; ::_thesis: ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) A3: width (ColVec2Mx x1) = 1 by A2, Def9; A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, Def9; A5: dom x1 = dom x2 by A1, FINSEQ_3:29; A6: len (ColVec2Mx x1) = len x1 by A2, Def9; then A7: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29; ( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, Def9; then A8: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55; A9: len (x1 + x2) = len x1 by A1, RVSUM_1:115; then A10: dom (x1 + x2) = dom x1 by FINSEQ_3:29; A11: ( len (ColVec2Mx (x1 + x2)) = len (x1 + x2) & width (ColVec2Mx (x1 + x2)) = 1 ) by A2, A9, Def9; then A12: Indices (ColVec2Mx (x1 + x2)) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55, RVSUM_1:115; for i, j being Nat st [i,j] in Indices (ColVec2Mx x1) holds (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) ) thus ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) ) ::_thesis: verum proof assume A13: [i,j] in Indices (ColVec2Mx x1) ; ::_thesis: (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) then consider q1 being FinSequence of REAL such that A14: q1 = (ColVec2Mx x1) . i and A15: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5; j in Seg 1 by A4, A13, ZFMISC_1:87; then ( 1 <= j & j <= 1 ) by FINSEQ_1:1; then A16: j = 1 by XXREAL_0:1; A17: i in dom x1 by A7, A13, ZFMISC_1:87; then (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, Def9; then A18: q1 . j = x1 . i by A16, A14, FINSEQ_1:40; consider p being FinSequence of REAL such that A19: p = (ColVec2Mx (x1 + x2)) . i and A20: (ColVec2Mx (x1 + x2)) * (i,j) = p . j by A12, A13, MATRIX_1:def_5; consider q2 being FinSequence of REAL such that A21: q2 = (ColVec2Mx x2) . i and A22: (ColVec2Mx x2) * (i,j) = q2 . j by A8, A13, MATRIX_1:def_5; (ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A17, Def9; then A23: q2 . j = x2 . i by A16, A21, FINSEQ_1:40; (ColVec2Mx (x1 + x2)) . i = <*((x1 + x2) . i)*> by A2, A9, A10, A17, Def9; then p . j = (x1 + x2) . i by A16, A19, FINSEQ_1:40; hence (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) by A10, A17, A20, A15, A18, A22, A23, VALUED_1:def_1; ::_thesis: verum end; end; hence ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) by A1, A6, A11, A3, Th26, RVSUM_1:115; ::_thesis: verum end; theorem Th47: :: MATRIXR1:47 for a being Real for x being FinSequence of REAL st len x > 0 holds ColVec2Mx (a * x) = a * (ColVec2Mx x) proof let a be Real; ::_thesis: for x being FinSequence of REAL st len x > 0 holds ColVec2Mx (a * x) = a * (ColVec2Mx x) let x be FinSequence of REAL ; ::_thesis: ( len x > 0 implies ColVec2Mx (a * x) = a * (ColVec2Mx x) ) assume A1: len x > 0 ; ::_thesis: ColVec2Mx (a * x) = a * (ColVec2Mx x) A2: len (a * (ColVec2Mx x)) = len (ColVec2Mx x) by Th27 .= len x by A1, Def9 ; A3: len (a * x) = len x by RVSUM_1:117; then A4: dom (a * x) = dom x by FINSEQ_3:29; A5: for j being Nat st j in dom (a * x) holds (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> proof len (ColVec2Mx x) = len x by A1, Def9; then A6: dom (ColVec2Mx x) = dom x by FINSEQ_3:29; let j be Nat; ::_thesis: ( j in dom (a * x) implies (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> ) consider n being Nat such that A7: for x2 being set st x2 in rng (a * (ColVec2Mx x)) holds ex s2 being FinSequence st ( s2 = x2 & len s2 = n ) by MATRIX_1:def_1; assume A8: j in dom (a * x) ; ::_thesis: (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> then A9: (ColVec2Mx x) . j = <*(x . j)*> by A1, A4, Def9; A10: j in dom (a * (ColVec2Mx x)) by A2, A3, A8, FINSEQ_3:29; then (a * (ColVec2Mx x)) . j in rng (a * (ColVec2Mx x)) by FUNCT_1:def_3; then reconsider q = (a * (ColVec2Mx x)) . j as FinSequence of REAL by FINSEQ_1:def_11; q in rng (a * (ColVec2Mx x)) by A10, FUNCT_1:def_3; then A11: ex s2 being FinSequence st ( s2 = q & len s2 = n ) by A7; consider s being FinSequence such that A12: s in rng (a * (ColVec2Mx x)) and A13: len s = width (a * (ColVec2Mx x)) by A1, A2, MATRIX_1:def_3; ex s3 being FinSequence st ( s3 = s & len s3 = n ) by A12, A7; then A14: len q = width (ColVec2Mx x) by A13, A11, Th27 .= 1 by A1, Def9 .= len <*((a * x) . j)*> by FINSEQ_1:40 ; width (ColVec2Mx x) = 1 by A1, Def9; then A15: 1 in Seg (width (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:1; j in dom x by A3, A8, FINSEQ_3:29; then A16: [j,1] in Indices (MXR2MXF (ColVec2Mx x)) by A6, A15, ZFMISC_1:87; then A17: ex p3 being FinSequence of REAL st ( p3 = (ColVec2Mx x) . j & (ColVec2Mx x) * (j,1) = p3 . 1 ) by MATRIX_1:def_5; [j,1] in Indices (a * (ColVec2Mx x)) by A16, Th28; then A18: ex p being FinSequence of REAL st ( p = (a * (ColVec2Mx x)) . j & (a * (ColVec2Mx x)) * (j,1) = p . 1 ) by MATRIX_1:def_5; reconsider j = j as Element of NAT by ORDINAL1:def_12; A19: q . 1 = a * ((ColVec2Mx x) * (j,1)) by A16, A18, Th29 .= a * (x . j) by A17, A9, FINSEQ_1:40 .= (a * x) . j by RVSUM_1:44 .= <*((a * x) . j)*> . 1 by FINSEQ_1:40 ; for i being Nat st 1 <= i & i <= len <*((a * x) . j)*> holds q . i = <*((a * x) . j)*> . i proof let i be Nat; ::_thesis: ( 1 <= i & i <= len <*((a * x) . j)*> implies q . i = <*((a * x) . j)*> . i ) A20: len <*((a * x) . j)*> = 1 by FINSEQ_1:40; assume ( 1 <= i & i <= len <*((a * x) . j)*> ) ; ::_thesis: q . i = <*((a * x) . j)*> . i then i = 1 by A20, XXREAL_0:1; hence q . i = <*((a * x) . j)*> . i by A19; ::_thesis: verum end; hence (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> by A14, FINSEQ_1:14; ::_thesis: verum end; width (a * (ColVec2Mx x)) = width (ColVec2Mx x) by Th27 .= 1 by A1, Def9 ; hence ColVec2Mx (a * x) = a * (ColVec2Mx x) by A1, A2, A3, A5, Def9; ::_thesis: verum end; definition let x be FinSequence of REAL ; func LineVec2Mx x -> Matrix of REAL means :Def10: :: MATRIXR1:def 10 ( width it = len x & len it = 1 & ( for j being Nat st j in dom x holds it * (1,j) = x . j ) ); existence ex b1 being Matrix of REAL st ( width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds b1 * (1,j) = x . j ) ) proof set B = <*x*>; A1: rng <*x*> = {x} by FINSEQ_1:39; for y being set st y in rng <*x*> holds ex p being FinSequence of REAL st ( y = p & len p = len x ) proof let y be set ; ::_thesis: ( y in rng <*x*> implies ex p being FinSequence of REAL st ( y = p & len p = len x ) ) assume y in rng <*x*> ; ::_thesis: ex p being FinSequence of REAL st ( y = p & len p = len x ) then y = x by A1, TARSKI:def_1; hence ex p being FinSequence of REAL st ( y = p & len p = len x ) ; ::_thesis: verum end; then reconsider C = <*x*> as Matrix of REAL by MATRIX_1:9; take C ; ::_thesis: ( width C = len x & len C = 1 & ( for j being Nat st j in dom x holds C * (1,j) = x . j ) ) A2: len <*x*> = 1 by FINSEQ_1:39; then dom C = Seg 1 by FINSEQ_1:def_3; then A3: 1 in dom C by FINSEQ_1:1; for p being FinSequence of REAL st p in rng C holds len p = len x by A1, TARSKI:def_1; then ( len <*x*> = 1 & C is Matrix of 1, len x, REAL ) by A2, MATRIX_1:def_2; hence A4: width C = len x by MATRIX_1:20; ::_thesis: ( len C = 1 & ( for j being Nat st j in dom x holds C * (1,j) = x . j ) ) thus len C = 1 by FINSEQ_1:40; ::_thesis: for j being Nat st j in dom x holds C * (1,j) = x . j let j be Nat; ::_thesis: ( j in dom x implies C * (1,j) = x . j ) assume j in dom x ; ::_thesis: C * (1,j) = x . j then j in Seg (len x) by FINSEQ_1:def_3; then ( <*x*> . 1 = x & [1,j] in Indices C ) by A4, A3, FINSEQ_1:40, ZFMISC_1:def_2; hence C * (1,j) = x . j by MATRIX_1:def_5; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of REAL st width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds b1 * (1,j) = x . j ) & width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds b2 * (1,j) = x . j ) holds b1 = b2 proof let A, B be Matrix of REAL; ::_thesis: ( width A = len x & len A = 1 & ( for j being Nat st j in dom x holds A * (1,j) = x . j ) & width B = len x & len B = 1 & ( for j being Nat st j in dom x holds B * (1,j) = x . j ) implies A = B ) assume that A5: width A = len x and A6: len A = 1 and A7: for k being Nat st k in dom x holds A * (1,k) = x . k and A8: ( width B = len x & len B = 1 ) and A9: for k being Nat st k in dom x holds B * (1,k) = x . k ; ::_thesis: A = B A10: dom A = Seg 1 by A6, FINSEQ_1:def_3; for i, j being Nat st [i,j] in Indices A holds A * (i,j) = B * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) ) assume A11: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j) then i in Seg 1 by A10, ZFMISC_1:87; then ( 1 <= i & i <= 1 ) by FINSEQ_1:1; then A12: i = 1 by XXREAL_0:1; j in Seg (len x) by A5, A11, ZFMISC_1:87; then A13: j in dom x by FINSEQ_1:def_3; then A * (i,j) = x . j by A7, A12; hence A * (i,j) = B * (i,j) by A9, A13, A12; ::_thesis: verum end; hence A = B by A5, A6, A8, MATRIX_1:21; ::_thesis: verum end; end; :: deftheorem Def10 defines LineVec2Mx MATRIXR1:def_10_:_ for x being FinSequence of REAL for b2 being Matrix of REAL holds ( b2 = LineVec2Mx x iff ( width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds b2 * (1,j) = x . j ) ) ); theorem :: MATRIXR1:48 for x being FinSequence of REAL for M being Matrix of REAL holds ( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) ) proof let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL holds ( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) ) let M be Matrix of REAL; ::_thesis: ( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) ) thus ( M = LineVec2Mx x implies ( Line (M,1) = x & len M = 1 ) ) ::_thesis: ( Line (M,1) = x & len M = 1 implies M = LineVec2Mx x ) proof assume A1: M = LineVec2Mx x ; ::_thesis: ( Line (M,1) = x & len M = 1 ) then A2: for j being Nat st j in dom x holds M * (1,j) = x . j by Def10; A3: width M = len x by A1, Def10; then dom x = Seg (width M) by FINSEQ_1:def_3; hence ( Line (M,1) = x & len M = 1 ) by A1, A3, A2, Def10, MATRIX_1:def_7; ::_thesis: verum end; assume that A4: Line (M,1) = x and A5: len M = 1 ; ::_thesis: M = LineVec2Mx x A6: for j being Nat st j in Seg (width M) holds x . j = M * (1,j) by A4, MATRIX_1:def_7; A7: len x = width M by A4, MATRIX_1:def_7; then Seg (width M) = dom x by FINSEQ_1:def_3; hence M = LineVec2Mx x by A5, A7, A6, Def10; ::_thesis: verum end; theorem Th49: :: MATRIXR1:49 for x being FinSequence of REAL st len x > 0 holds ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) proof let x be FinSequence of REAL ; ::_thesis: ( len x > 0 implies ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) ) A1: dom (LineVec2Mx x) = Seg (len (LineVec2Mx x)) by FINSEQ_1:def_3; A2: width (LineVec2Mx x) = len x by Def10; assume A3: len x > 0 ; ::_thesis: ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) then A4: len (ColVec2Mx x) = len x by Def9; A5: len (LineVec2Mx x) = 1 by Def10; A6: width (ColVec2Mx x) = 1 by A3, Def9; A7: dom (ColVec2Mx x) = Seg (len (ColVec2Mx x)) by FINSEQ_1:def_3; A8: for i, j being Nat holds ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) ( [i,j] in Indices (ColVec2Mx x) iff ( i in dom (ColVec2Mx x) & j in Seg (width (ColVec2Mx x)) ) ) by ZFMISC_1:87; hence ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) by A2, A5, A4, A6, A7, A1, ZFMISC_1:87; ::_thesis: verum end; A9: for i, j being Nat st [j,i] in Indices (LineVec2Mx x) holds (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) proof let i, j be Nat; ::_thesis: ( [j,i] in Indices (LineVec2Mx x) implies (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) ) assume A10: [j,i] in Indices (LineVec2Mx x) ; ::_thesis: (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) then [i,j] in Indices (ColVec2Mx x) by A8; then A11: ex p being FinSequence of REAL st ( p = (ColVec2Mx x) . i & (ColVec2Mx x) * (i,j) = p . j ) by MATRIX_1:def_5; j in Seg 1 by A5, A1, A10, ZFMISC_1:87; then ( 1 <= j & j <= 1 ) by FINSEQ_1:1; then A12: j = 1 by XXREAL_0:1; i in Seg (len x) by A2, A10, ZFMISC_1:87; then A13: i in dom x by FINSEQ_1:def_3; then (ColVec2Mx x) . i = <*(x . i)*> by A3, Def9; hence (ColVec2Mx x) * (i,j) = x . i by A12, A11, FINSEQ_1:40 .= (LineVec2Mx x) * (j,i) by A12, A13, Def10 ; ::_thesis: verum end; hence (LineVec2Mx x) @ = ColVec2Mx x by A2, A4, A8, MATRIX_1:def_6; ::_thesis: (ColVec2Mx x) @ = LineVec2Mx x A14: for i, j being Nat st [j,i] in Indices (ColVec2Mx x) holds (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) proof let i, j be Nat; ::_thesis: ( [j,i] in Indices (ColVec2Mx x) implies (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) ) assume [j,i] in Indices (ColVec2Mx x) ; ::_thesis: (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) then [i,j] in Indices (LineVec2Mx x) by A8; hence (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) by A9; ::_thesis: verum end; for i, j being Nat holds ( [i,j] in Indices (LineVec2Mx x) iff [j,i] in Indices (ColVec2Mx x) ) by A8; hence (ColVec2Mx x) @ = LineVec2Mx x by A5, A6, A14, MATRIX_1:def_6; ::_thesis: verum end; theorem Th50: :: MATRIXR1:50 for x1, x2 being FinSequence of REAL st len x1 = len x2 holds LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) proof let x1, x2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 implies LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) ) assume A1: len x1 = len x2 ; ::_thesis: LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) then A2: dom x1 = dom x2 by FINSEQ_3:29; len (x1 + x2) = len x1 by A1, RVSUM_1:115; then A3: dom (x1 + x2) = dom x1 by FINSEQ_3:29; A4: ( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 ) by Def10; ( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 ) by Def10; then A5: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55; A6: Seg (width (LineVec2Mx x1)) = Seg (len x1) by Def10 .= dom x1 by FINSEQ_1:def_3 ; A7: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def_3 .= Seg 1 by Def10 ; A8: ( width (LineVec2Mx (x1 + x2)) = len (x1 + x2) & len (LineVec2Mx (x1 + x2)) = 1 ) by Def10; then A9: Indices (LineVec2Mx (x1 + x2)) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55, RVSUM_1:115; for i, j being Nat st [i,j] in Indices (LineVec2Mx x1) holds (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) ) assume A10: [i,j] in Indices (LineVec2Mx x1) ; ::_thesis: (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) then consider q1 being FinSequence of REAL such that q1 = (LineVec2Mx x1) . i and A11: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5; consider p being FinSequence of REAL such that p = (LineVec2Mx (x1 + x2)) . i and A12: (LineVec2Mx (x1 + x2)) * (i,j) = p . j by A9, A10, MATRIX_1:def_5; consider q2 being FinSequence of REAL such that q2 = (LineVec2Mx x2) . i and A13: (LineVec2Mx x2) * (i,j) = q2 . j by A5, A10, MATRIX_1:def_5; A14: j in dom x1 by A6, A10, ZFMISC_1:87; i in Seg 1 by A7, A10, ZFMISC_1:87; then ( 1 <= i & i <= 1 ) by FINSEQ_1:1; then A15: i = 1 by XXREAL_0:1; then A16: q1 . j = x1 . j by A14, A11, Def10; A17: q2 . j = x2 . j by A2, A14, A15, A13, Def10; p . j = (x1 + x2) . j by A3, A14, A15, A12, Def10; hence (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) by A3, A14, A12, A11, A16, A13, A17, VALUED_1:def_1; ::_thesis: verum end; hence LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) by A1, A8, A4, Th26, RVSUM_1:115; ::_thesis: verum end; theorem :: MATRIXR1:51 for a being Real for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x) proof let a be Real; ::_thesis: for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x) let x be FinSequence of REAL ; ::_thesis: LineVec2Mx (a * x) = a * (LineVec2Mx x) A1: len (a * (LineVec2Mx x)) = len (LineVec2Mx x) by Th27 .= 1 by Def10 ; A2: len (a * x) = len x by RVSUM_1:117; then A3: dom (a * x) = dom x by FINSEQ_3:29; A4: for j being Nat st j in dom (a * x) holds (a * (LineVec2Mx x)) * (1,j) = (a * x) . j proof len (LineVec2Mx x) = 1 by Def10; then 1 in Seg (len (LineVec2Mx x)) by FINSEQ_1:1; then A5: 1 in dom (LineVec2Mx x) by FINSEQ_1:def_3; 1 in Seg (len (a * (LineVec2Mx x))) by A1, FINSEQ_1:1; then 1 in dom (a * (LineVec2Mx x)) by FINSEQ_1:def_3; then (a * (LineVec2Mx x)) . 1 in rng (a * (LineVec2Mx x)) by FUNCT_1:def_3; then reconsider q = (a * (LineVec2Mx x)) . 1 as FinSequence of REAL by FINSEQ_1:def_11; let j be Nat; ::_thesis: ( j in dom (a * x) implies (a * (LineVec2Mx x)) * (1,j) = (a * x) . j ) A6: width (LineVec2Mx x) = len x by Def10; A7: Indices (a * (LineVec2Mx x)) = Indices (LineVec2Mx x) by Th28; assume A8: j in dom (a * x) ; ::_thesis: (a * (LineVec2Mx x)) * (1,j) = (a * x) . j then j in Seg (len x) by A2, FINSEQ_1:def_3; then A9: [1,j] in Indices (a * (LineVec2Mx x)) by A6, A5, A7, ZFMISC_1:87; then A10: ex p being FinSequence of REAL st ( p = (a * (LineVec2Mx x)) . 1 & (a * (LineVec2Mx x)) * (1,j) = p . j ) by MATRIX_1:def_5; reconsider j = j as Element of NAT by ORDINAL1:def_12; q . j = a * ((LineVec2Mx x) * (1,j)) by A7, A9, A10, Th29 .= a * (x . j) by A3, A8, Def10 .= (a * x) . j by RVSUM_1:44 ; hence (a * (LineVec2Mx x)) * (1,j) = (a * x) . j by A9, MATRIX_1:def_5; ::_thesis: verum end; width (a * (LineVec2Mx x)) = width (LineVec2Mx x) by Th27 .= len x by Def10 ; hence LineVec2Mx (a * x) = a * (LineVec2Mx x) by A1, A2, A4, Def10; ::_thesis: verum end; definition let M be Matrix of REAL; let x be FinSequence of REAL ; funcM * x -> FinSequence of REAL equals :: MATRIXR1:def 11 Col ((M * (ColVec2Mx x)),1); coherence Col ((M * (ColVec2Mx x)),1) is FinSequence of REAL ; funcx * M -> FinSequence of REAL equals :: MATRIXR1:def 12 Line (((LineVec2Mx x) * M),1); coherence Line (((LineVec2Mx x) * M),1) is FinSequence of REAL ; end; :: deftheorem defines * MATRIXR1:def_11_:_ for M being Matrix of REAL for x being FinSequence of REAL holds M * x = Col ((M * (ColVec2Mx x)),1); :: deftheorem defines * MATRIXR1:def_12_:_ for M being Matrix of REAL for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1); theorem Th52: :: MATRIXR1:52 for x being FinSequence of REAL for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds (A @) * x = x * A proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds (A @) * x = x * A let A be Matrix of REAL; ::_thesis: ( len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) implies (A @) * x = x * A ) assume that A1: len A > 0 and A2: width A > 0 and A3: ( len A = len x or width (A @) = len x ) ; ::_thesis: (A @) * x = x * A A4: len A = len x by A2, A3, MATRIX_2:10; A5: len A = width (A @) by A2, MATRIX_2:10; then len (ColVec2Mx x) = len x by A1, A3, Def9; then A6: width ((A @) * (ColVec2Mx x)) = width (ColVec2Mx x) by A3, A5, MATRIX_3:def_4; width (ColVec2Mx x) = 1 by A1, A3, A5, Def9; then A7: 1 in Seg (width ((A @) * (ColVec2Mx x))) by A6, FINSEQ_1:1; A8: len (LineVec2Mx x) = 1 by Def10; A9: width (LineVec2Mx x) = len x by Def10; then width (LineVec2Mx x) = len A by A2, A3, MATRIX_2:10; then ( len ((LineVec2Mx x) * A) = len (LineVec2Mx x) & width ((LineVec2Mx x) * A) = width A ) by MATRIX_3:def_4; then Line (((LineVec2Mx x) * A),1) = Line (((((LineVec2Mx x) * A) @) @),1) by A2, A8, MATRIX_2:13 .= Line ((((A @) * ((LineVec2Mx x) @)) @),1) by A2, A4, A9, MATRIX_3:22 .= Line ((((A @) * (ColVec2Mx x)) @),1) by A1, A4, Th49 .= Col (((A @) * (ColVec2Mx x)),1) by A7, MATRIX_2:15 ; hence (A @) * x = x * A ; ::_thesis: verum end; theorem Th53: :: MATRIXR1:53 for x being FinSequence of REAL for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds A * x = x * (A @) proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds A * x = x * (A @) let A be Matrix of REAL; ::_thesis: ( len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) implies A * x = x * (A @) ) assume that A1: len A > 0 and A2: width A > 0 and A3: ( width A = len x or len (A @) = len x ) ; ::_thesis: A * x = x * (A @) ( len (A @) = width A & width (A @) = len A ) by A2, MATRIX_2:10; then ((A @) @) * x = x * (A @) by A1, A2, A3, Th52; hence A * x = x * (A @) by A1, A2, MATRIX_2:13; ::_thesis: verum end; theorem Th54: :: MATRIXR1:54 for A, B being Matrix of REAL st len A = len B holds for i being Nat st 1 <= i & i <= width A holds Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) proof let A, B be Matrix of REAL; ::_thesis: ( len A = len B implies for i being Nat st 1 <= i & i <= width A holds Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) ) assume A1: len A = len B ; ::_thesis: for i being Nat st 1 <= i & i <= width A holds Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) then A2: dom A = dom B by FINSEQ_3:29; let i be Nat; ::_thesis: ( 1 <= i & i <= width A implies Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) ) A3: len (Col (A,i)) = len A by MATRIX_1:def_8; len (Col (B,i)) = len B by MATRIX_1:def_8; then A4: len ((Col (A,i)) + (Col (B,i))) = len (Col (A,i)) by A1, A3, RVSUM_1:115; assume ( 1 <= i & i <= width A ) ; ::_thesis: Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) then A5: i in Seg (width A) by FINSEQ_1:1; A6: len (A + B) = len A by Th25; Seg (len (A + B)) = dom (A + B) by FINSEQ_1:def_3; then A7: dom ((Col (A,i)) + (Col (B,i))) = dom (A + B) by A3, A6, A4, FINSEQ_1:def_3; for j being Nat st j in dom (A + B) holds ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) proof let j be Nat; ::_thesis: ( j in dom (A + B) implies ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) ) assume A8: j in dom (A + B) ; ::_thesis: ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) then j in Seg (len (A + B)) by FINSEQ_1:def_3; then A9: j in dom A by A6, FINSEQ_1:def_3; then A10: [j,i] in Indices A by A5, ZFMISC_1:87; reconsider j = j as Element of NAT by ORDINAL1:def_12; ( (Col (A,i)) . j = A * (j,i) & (Col (B,i)) . j = B * (j,i) ) by A2, A9, MATRIX_1:def_8; then ((Col (A,i)) . j) + ((Col (B,i)) . j) = (A + B) * (j,i) by A10, Th25; hence ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) by A7, A8, VALUED_1:def_1; ::_thesis: verum end; hence Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) by A3, A6, A4, MATRIX_1:def_8; ::_thesis: verum end; theorem Th55: :: MATRIXR1:55 for A, B being Matrix of REAL st width A = width B holds for i being Nat st 1 <= i & i <= len A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) proof let A, B be Matrix of REAL; ::_thesis: ( width A = width B implies for i being Nat st 1 <= i & i <= len A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) ) assume A1: width A = width B ; ::_thesis: for i being Nat st 1 <= i & i <= len A holds Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) let i be Nat; ::_thesis: ( 1 <= i & i <= len A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) ) A2: len (Line (A,i)) = width A by MATRIX_1:def_7; assume ( 1 <= i & i <= len A ) ; ::_thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) then A3: i in dom A by FINSEQ_3:25; A4: width (A + B) = width A by Th25; len (Line (B,i)) = width B by MATRIX_1:def_7; then A5: len ((Line (A,i)) + (Line (B,i))) = len (Line (A,i)) by A1, A2, RVSUM_1:115; then A6: dom ((Line (A,i)) + (Line (B,i))) = Seg (width A) by A2, FINSEQ_1:def_3; for j being Nat st j in Seg (width (A + B)) holds ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) proof let j be Nat; ::_thesis: ( j in Seg (width (A + B)) implies ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) ) assume A7: j in Seg (width (A + B)) ; ::_thesis: ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) then A8: j in Seg (width A) by Th25; then A9: ( [i,j] in Indices A & (Line (A,i)) . j = A * (i,j) ) by A3, MATRIX_1:def_7, ZFMISC_1:87; reconsider j = j as Element of NAT by ORDINAL1:def_12; (Line (B,i)) . j = B * (i,j) by A1, A8, MATRIX_1:def_7; then ((Line (A,i)) . j) + ((Line (B,i)) . j) = (A + B) * (i,j) by A9, Th25; hence ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) by A4, A6, A7, VALUED_1:def_1; ::_thesis: verum end; hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A2, A4, A5, MATRIX_1:def_7; ::_thesis: verum end; theorem Th56: :: MATRIXR1:56 for a being Real for M being Matrix of REAL for i being Nat st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) proof let a be Real; ::_thesis: for M being Matrix of REAL for i being Nat st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) let M be Matrix of REAL; ::_thesis: for i being Nat st 1 <= i & i <= width M holds Col ((a * M),i) = a * (Col (M,i)) reconsider ea = a as Element of F_Real ; let i be Nat; ::_thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) ) assume A1: ( 1 <= i & i <= width M ) ; ::_thesis: Col ((a * M),i) = a * (Col (M,i)) Col ((a * M),i) = Col ((MXF2MXR (ea * (MXR2MXF M))),i) by Def7 .= ea * (Col ((MXR2MXF M),i)) by A1, Th19 ; hence Col ((a * M),i) = a * (Col (M,i)) by Th17; ::_thesis: verum end; theorem :: MATRIXR1:57 for x1, x2 being FinSequence of REAL for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds A * (x1 + x2) = (A * x1) + (A * x2) proof let x1, x2 be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds A * (x1 + x2) = (A * x1) + (A * x2) let A be Matrix of REAL; ::_thesis: ( len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 implies A * (x1 + x2) = (A * x1) + (A * x2) ) assume that A1: len x1 = len x2 and A2: width A = len x1 and A3: len x1 > 0 and A4: len A > 0 ; ::_thesis: A * (x1 + x2) = (A * x1) + (A * x2) A5: len (ColVec2Mx x2) = len x2 by A1, A3, Def9; A6: len (ColVec2Mx x1) = len x1 by A3, Def9; then A7: len (A * (ColVec2Mx x1)) = len A by A2, MATRIX_3:def_4 .= len (A * (ColVec2Mx x2)) by A1, A2, A5, MATRIX_3:def_4 ; A8: width (ColVec2Mx x1) = 1 by A3, Def9; then A9: 1 <= width (A * (ColVec2Mx x1)) by A2, A6, MATRIX_3:def_4; A10: width (ColVec2Mx x2) = 1 by A1, A3, Def9; thus A * (x1 + x2) = Col ((A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1) by A1, A3, Th46 .= Col (((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1) by A1, A2, A3, A4, A6, A5, A8, A10, MATRIX_4:62 .= (A * x1) + (A * x2) by A7, A9, Th54 ; ::_thesis: verum end; theorem :: MATRIXR1:58 for x1, x2 being FinSequence of REAL for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds (x1 + x2) * A = (x1 * A) + (x2 * A) proof let x1, x2 be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds (x1 + x2) * A = (x1 * A) + (x2 * A) let A be Matrix of REAL; ::_thesis: ( len x1 = len x2 & len A = len x1 & len x1 > 0 implies (x1 + x2) * A = (x1 * A) + (x2 * A) ) assume that A1: len x1 = len x2 and A2: len A = len x1 and A3: len x1 > 0 ; ::_thesis: (x1 + x2) * A = (x1 * A) + (x2 * A) A4: width (LineVec2Mx x2) = len x2 by Def10; A5: width (LineVec2Mx x1) = len x1 by Def10; then A6: width ((LineVec2Mx x1) * A) = width A by A2, MATRIX_3:def_4 .= width ((LineVec2Mx x2) * A) by A1, A2, A4, MATRIX_3:def_4 ; A7: len (LineVec2Mx x1) = 1 by Def10; then A8: 1 <= len ((LineVec2Mx x1) * A) by A2, A5, MATRIX_3:def_4; A9: len (LineVec2Mx x2) = 1 by Def10; thus (x1 + x2) * A = Line ((((LineVec2Mx x1) + (LineVec2Mx x2)) * A),1) by A1, Th50 .= Line ((((LineVec2Mx x1) * A) + ((LineVec2Mx x2) * A)),1) by A1, A2, A3, A5, A4, A7, A9, MATRIX_4:63 .= (x1 * A) + (x2 * A) by A6, A8, Th55 ; ::_thesis: verum end; theorem Th59: :: MATRIXR1:59 for a being Real for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 holds A * (a * x) = a * (A * x) proof let a be Real; ::_thesis: for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 holds A * (a * x) = a * (A * x) let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 holds A * (a * x) = a * (A * x) let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 implies A * (a * x) = a * (A * x) ) assume that A1: width A = len x and A2: len x > 0 ; ::_thesis: A * (a * x) = a * (A * x) A3: len (ColVec2Mx x) = len x by A2, Def9; width (ColVec2Mx x) = 1 by A2, Def9; then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A3, MATRIX_3:def_4; thus A * (a * x) = Col ((A * (a * (ColVec2Mx x))),1) by A2, Th47 .= Col ((a * (A * (ColVec2Mx x))),1) by A1, A3, Th40 .= a * (A * x) by A4, Th56 ; ::_thesis: verum end; theorem :: MATRIXR1:60 for a being Real for x being FinSequence of REAL for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds (a * x) * A = a * (x * A) proof let a be Real; ::_thesis: for x being FinSequence of REAL for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds (a * x) * A = a * (x * A) let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds (a * x) * A = a * (x * A) let A be Matrix of REAL; ::_thesis: ( len A = len x & len x > 0 & width A > 0 implies (a * x) * A = a * (x * A) ) assume that A1: len A = len x and A2: len x > 0 and A3: width A > 0 ; ::_thesis: (a * x) * A = a * (x * A) A4: (A @) * x = x * A by A1, A2, A3, Th52; A5: width (A @) = len x by A1, A3, MATRIX_2:10; then A6: (A @) * (a * x) = a * ((A @) * x) by A2, Th59; A7: len (a * x) = len x by RVSUM_1:117; len (A @) > 0 by A3, MATRIX_2:10; then (a * x) * ((A @) @) = (A @) * (a * x) by A2, A5, A7, Th53; hence (a * x) * A = a * (x * A) by A1, A2, A3, A6, A4, MATRIX_2:13; ::_thesis: verum end; theorem Th61: :: MATRIXR1:61 for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 holds len (A * x) = len A proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 holds len (A * x) = len A let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 implies len (A * x) = len A ) assume that A1: width A = len x and A2: len x > 0 ; ::_thesis: len (A * x) = len A A3: len (ColVec2Mx x) = len x by A2, Def9; len (Col ((A * (ColVec2Mx x)),1)) = len (A * (ColVec2Mx x)) by MATRIX_1:def_8 .= len A by A1, A3, MATRIX_3:def_4 ; hence len (A * x) = len A ; ::_thesis: verum end; theorem Th62: :: MATRIXR1:62 for x being FinSequence of REAL for A being Matrix of REAL st len A = len x holds len (x * A) = width A proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x holds len (x * A) = width A let A be Matrix of REAL; ::_thesis: ( len A = len x implies len (x * A) = width A ) assume A1: len A = len x ; ::_thesis: len (x * A) = width A A2: width (LineVec2Mx x) = len x by Def10; len (Line (((LineVec2Mx x) * A),1)) = width (MXF2MXR ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) by MATRIX_1:def_7 .= width A by A1, A2, MATRIX_3:def_4 ; hence len (x * A) = width A ; ::_thesis: verum end; theorem Th63: :: MATRIXR1:63 for x being FinSequence of REAL for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 holds (A + B) * x = (A * x) + (B * x) proof let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 holds (A + B) * x = (A * x) + (B * x) let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 implies (A + B) * x = (A * x) + (B * x) ) assume that A1: ( len A = len B & width A = width B ) and A2: width A = len x and A3: len A > 0 and A4: len x > 0 ; ::_thesis: (A + B) * x = (A * x) + (B * x) A5: len (ColVec2Mx x) = len x by A4, Def9; then A6: len (A * (ColVec2Mx x)) = len A by A2, MATRIX_3:def_4 .= len (B * (ColVec2Mx x)) by A1, A2, A5, MATRIX_3:def_4 ; A7: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A2, A5, MATRIX_3:def_4 .= 1 by A4, Def9 ; thus (A + B) * x = Col (((A * (ColVec2Mx x)) + (B * (ColVec2Mx x))),1) by A1, A2, A3, A4, A5, MATRIX_4:63 .= (A * x) + (B * x) by A6, A7, Th54 ; ::_thesis: verum end; theorem Th64: :: MATRIXR1:64 for x being FinSequence of REAL for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 0 holds x * (A + B) = (x * A) + (x * B) proof let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 0 holds x * (A + B) = (x * A) + (x * B) let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A = len x & len x > 0 implies x * (A + B) = (x * A) + (x * B) ) assume that A1: ( len A = len B & width A = width B ) and A2: len A = len x and A3: len x > 0 ; ::_thesis: x * (A + B) = (x * A) + (x * B) A4: width (LineVec2Mx x) = len x by Def10; then A5: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A2, MATRIX_3:def_4 .= 1 by Def10 ; A6: width ((LineVec2Mx x) * A) = width A by A2, A4, MATRIX_3:def_4 .= width ((LineVec2Mx x) * B) by A1, A2, A4, MATRIX_3:def_4 ; len (LineVec2Mx x) = 1 by Def10; hence x * (A + B) = Line ((((LineVec2Mx x) * A) + ((LineVec2Mx x) * B)),1) by A1, A2, A3, A4, MATRIX_4:62 .= (x * A) + (x * B) by A6, A5, Th55 ; ::_thesis: verum end; theorem :: MATRIXR1:65 for n, m being Element of NAT for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds (0_Rmatrix (n,m)) * x = 0* n proof let n, m be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds (0_Rmatrix (n,m)) * x = 0* n let x be FinSequence of REAL ; ::_thesis: ( len x = m & n > 0 & m > 0 implies (0_Rmatrix (n,m)) * x = 0* n ) assume that A1: len x = m and A2: n > 0 and A3: m > 0 ; ::_thesis: (0_Rmatrix (n,m)) * x = 0* n A4: width (0_Rmatrix (n,m)) = m by A2, MATRIX_1:23; then A5: len ((0_Rmatrix (n,m)) * x) = len (0_Rmatrix (n,m)) by A1, A3, Th61; A6: len (0_Rmatrix (n,m)) = n by A2, MATRIX_1:23; then (0_Rmatrix (n,m)) * x = ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) * x by A2, A4, Th36 .= ((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x) by A1, A2, A3, A6, A4, Th63 ; then 0* n = (((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x)) - ((0_Rmatrix (n,m)) * x) by A6, A5, Th3; hence (0_Rmatrix (n,m)) * x = 0* n by A5, Th14; ::_thesis: verum end; theorem :: MATRIXR1:66 for n, m being Element of NAT for x being FinSequence of REAL st len x = n & n > 0 holds x * (0_Rmatrix (n,m)) = 0* m proof let n, m be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n & n > 0 holds x * (0_Rmatrix (n,m)) = 0* m let x be FinSequence of REAL ; ::_thesis: ( len x = n & n > 0 implies x * (0_Rmatrix (n,m)) = 0* m ) assume that A1: len x = n and A2: n > 0 ; ::_thesis: x * (0_Rmatrix (n,m)) = 0* m A3: len (0_Rmatrix (n,m)) = n by A2, MATRIX_1:23; then A4: len (x * (0_Rmatrix (n,m))) = width (0_Rmatrix (n,m)) by A1, Th62; A5: width (0_Rmatrix (n,m)) = m by A2, MATRIX_1:23; then x * (0_Rmatrix (n,m)) = x * ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) by A2, A3, Th36 .= (x * (0_Rmatrix (n,m))) + (x * (0_Rmatrix (n,m))) by A1, A2, A5, A3, Th64 ; then 0* m = ((x * (0_Rmatrix (n,m))) + (x * (0_Rmatrix (n,m)))) - (x * (0_Rmatrix (n,m))) by A5, A4, Th3; hence x * (0_Rmatrix (n,m)) = 0* m by A4, Th14; ::_thesis: verum end;