:: MATRIXR2 semantic presentation begin Lm1: for F1, F2 being FinSequence of REAL for j being Element of NAT st len F1 = len F2 holds (F1 - F2) . j = (F1 . j) - (F2 . j) proof let F1, F2 be FinSequence of REAL ; ::_thesis: for j being Element of NAT st len F1 = len F2 holds (F1 - F2) . j = (F1 . j) - (F2 . j) let j be Element of NAT ; ::_thesis: ( len F1 = len F2 implies (F1 - F2) . j = (F1 . j) - (F2 . j) ) reconsider n = len F1 as Element of NAT ; reconsider G1 = F1 as Element of n -tuples_on REAL by FINSEQ_2:92; assume len F1 = len F2 ; ::_thesis: (F1 - F2) . j = (F1 . j) - (F2 . j) then reconsider G2 = F2 as Element of n -tuples_on REAL by FINSEQ_2:92; (G1 - G2) . j = (G1 . j) - (G2 . j) by RVSUM_1:27; hence (F1 - F2) . j = (F1 . j) - (F2 . j) ; ::_thesis: verum end; theorem Th1: :: MATRIXR2:1 for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds ( x = - y & y = - x ) proof let x, y be FinSequence of REAL ; ::_thesis: ( len x = len y & x + y = 0* (len x) implies ( x = - y & y = - x ) ) assume that A1: len x = len y and A2: x + y = 0* (len x) ; ::_thesis: ( x = - y & y = - x ) A3: x = (0* (len x)) - y by A1, A2, MATRIXR1:14; hence x = - y by A1, MATRIXR1:6; ::_thesis: y = - x thus - x = - (- y) by A1, A3, MATRIXR1:6 .= y ; ::_thesis: verum end; Lm2: for D being non empty set for i being Element of NAT for A being Matrix of D st 1 <= i & i <= len A holds Line (A,i) = A . i proof let D be non empty set ; ::_thesis: for i being Element of NAT for A being Matrix of D st 1 <= i & i <= len A holds Line (A,i) = A . i let i be Element of NAT ; ::_thesis: for A being Matrix of D st 1 <= i & i <= len A holds Line (A,i) = A . i let A be Matrix of D; ::_thesis: ( 1 <= i & i <= len A implies Line (A,i) = A . i ) assume ( 1 <= i & i <= len A ) ; ::_thesis: Line (A,i) = A . i then i in dom A by FINSEQ_3:25; hence Line (A,i) = A . i by MATRIX_2:16; ::_thesis: verum end; theorem Th2: :: MATRIXR2:2 for D being non empty set for i, j being Element of NAT for A being Matrix of D for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds A * (i,j) = p . j proof let D be non empty set ; ::_thesis: for i, j being Element of NAT for A being Matrix of D for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds A * (i,j) = p . j let i, j be Element of NAT ; ::_thesis: for A being Matrix of D for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds A * (i,j) = p . j let A be Matrix of D; ::_thesis: for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds A * (i,j) = p . j let p be FinSequence of D; ::_thesis: ( p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A implies A * (i,j) = p . j ) assume that A1: p = A . i and A2: ( 1 <= i & i <= len A ) and A3: ( 1 <= j & j <= width A ) and A4: len p = width A ; ::_thesis: A * (i,j) = p . j A5: j in Seg (width A) by A3; then j in dom p by A4, FINSEQ_1:def_3; then ( rng p c= D & p . j in rng p ) by FINSEQ_1:def_4, FUNCT_1:def_3; then reconsider xp = p . j as Element of D ; A6: xp = p . j ; i in dom A by A2, FINSEQ_3:25; then [i,j] in Indices A by A5, ZFMISC_1:87; hence A * (i,j) = p . j by A1, A6, MATRIX_1:def_5; ::_thesis: verum end; theorem Th3: :: MATRIXR2:3 for i, j being Element of NAT for a being real number for A being Matrix of REAL st [i,j] in Indices A holds (a * A) * (i,j) = a * (A * (i,j)) proof let i, j be Element of NAT ; ::_thesis: for a being real number for A being Matrix of REAL st [i,j] in Indices A holds (a * A) * (i,j) = a * (A * (i,j)) let a be real number ; ::_thesis: for A being Matrix of REAL st [i,j] in Indices A holds (a * A) * (i,j) = a * (A * (i,j)) let A be Matrix of REAL; ::_thesis: ( [i,j] in Indices A implies (a * A) * (i,j) = a * (A * (i,j)) ) assume A1: [i,j] in Indices A ; ::_thesis: (a * A) * (i,j) = a * (A * (i,j)) reconsider aa = a as Element of F_Real by XREAL_0:def_1; (a * A) * (i,j) = (MXF2MXR (aa * (MXR2MXF A))) * (i,j) by MATRIXR1:def_7 .= aa * ((MXR2MXF A) * (i,j)) by A1, MATRIX_3:def_5 .= a * (A * (i,j)) ; hence (a * A) * (i,j) = a * (A * (i,j)) ; ::_thesis: verum end; theorem Th4: :: MATRIXR2:4 for n being Element of NAT for A, B being Matrix of n, REAL holds ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) proof let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL holds ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) let A, B be Matrix of n, REAL ; ::_thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) A1: len B = n by MATRIX_1:25; A2: len A = n by MATRIX_1:25; percases ( n > 0 or n <= 0 ) ; supposeA3: n > 0 ; ::_thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) then width (MXR2MXF A) = n by MATRIX_1:23 .= len (MXR2MXF B) by MATRIX_1:25 ; then ( len (A * B) = len A & width (A * B) = width B ) by MATRIX_3:def_4; hence ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) by A1, A3, MATRIX_1:20, MATRIX_1:25; ::_thesis: verum end; supposeA4: n <= 0 ; ::_thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) then A5: width (MXR2MXF A) = 0 by A2, MATRIX_1:def_3 .= len (MXR2MXF B) by A4, MATRIX_1:25 ; then len (A * B) = len A by MATRIX_3:def_4; hence ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) by A2, A4, A5, MATRIX_1:def_3, MATRIX_3:def_4; ::_thesis: verum end; end; end; theorem Th5: :: MATRIXR2:5 for a being real number for A being Matrix of REAL holds ( len (a * A) = len A & width (a * A) = width A ) proof let a be real number ; ::_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 by XREAL_0:def_1; A1: width (a * A) = width (MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) by MATRIXR1:def_7 .= width A by MATRIX_3:def_5 ; len (a * A) = len (MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) by MATRIXR1:def_7 .= len A by MATRIX_3:def_5 ; hence ( len (a * A) = len A & width (a * A) = width A ) by A1; ::_thesis: verum end; begin theorem Th6: :: MATRIXR2:6 for A, B being Matrix of REAL st len A = len B & width A = width B holds ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of 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 = len B & width A = width B implies ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds (A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) ) ) assume A1: ( len A = len B & width A = width B ) ; ::_thesis: ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds (A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) ) thus len (A - B) = len (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF B)))) by MATRIX_4:def_1 .= len A by MATRIX_3:def_3 ; ::_thesis: ( width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds (A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) ) thus width (A - B) = width (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF B)))) by MATRIX_4:def_1 .= width A by MATRIX_3:def_3 ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices A holds (A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) thus for i, j being Element of NAT st [i,j] in Indices A holds (A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) by A1, MATRIX10:3; ::_thesis: verum end; definition let n be Element of NAT ; let A, B be Matrix of n, REAL ; :: original: * redefine funcA * B -> Matrix of n, REAL ; coherence A * B is Matrix of n, REAL proof A1: ( len A = n & width B = n ) by MATRIX_1:24; ( len (A * B) = len A & width (A * B) = width B ) by Th4; hence A * B is Matrix of n, REAL by A1, MATRIX_2:7; ::_thesis: verum end; end; theorem Th7: :: MATRIXR2:7 for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds A + (B - B) = A proof let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A > 0 implies A + (B - B) = A ) assume ( len A = len B & width A = width B & len A > 0 ) ; ::_thesis: A + (B - B) = A hence A = A + (0_Rmatrix ((len B),(width B))) by MATRIXR1:36 .= (MXF2MXR (MXR2MXF A)) + (MXF2MXR ((MXR2MXF B) + (- (MXR2MXF B)))) by MATRIX_4:2 .= A + (B - B) by MATRIX_4:def_1 ; ::_thesis: verum end; theorem :: MATRIXR2:8 for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds (A + B) - B = A proof let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A > 0 implies (A + B) - B = A ) assume that A1: ( len A = len B & width A = width B ) and A2: len A > 0 ; ::_thesis: (A + B) - B = A thus (A + B) - B = (A + B) + (- B) by MATRIX_4:def_1 .= A + (B + (- B)) by A1, MATRIX_3:3 .= A + (B - B) by MATRIX_4:def_1 .= A by A1, A2, Th7 ; ::_thesis: verum end; Lm3: for i, j being Element of NAT for A being Matrix of REAL st [i,j] in Indices A holds (- A) * (i,j) = - (A * (i,j)) proof let i, j be Element of NAT ; ::_thesis: for A being Matrix of REAL st [i,j] in Indices A holds (- A) * (i,j) = - (A * (i,j)) let A be Matrix of REAL; ::_thesis: ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) ) assume [i,j] in Indices A ; ::_thesis: (- A) * (i,j) = - (A * (i,j)) then (- A) * (i,j) = - ((MXR2MXF A) * (i,j)) by MATRIX_3:def_2; hence (- A) * (i,j) = - (A * (i,j)) ; ::_thesis: verum end; theorem Th9: :: MATRIXR2:9 for A being Matrix of REAL holds (- 1) * A = - A proof let A be Matrix of REAL; ::_thesis: (- 1) * A = - A A1: width ((- 1) * A) = width A by Th5; A2: len ((- 1) * A) = len A by Th5; A3: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((-_1)_*_A)_holds_ ((-_1)_*_A)_*_(i,j)_=_(-_A)_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices ((- 1) * A) implies ((- 1) * A) * (i,j) = (- A) * (i,j) ) reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; assume A4: [i,j] in Indices ((- 1) * A) ; ::_thesis: ((- 1) * A) * (i,j) = (- A) * (i,j) then A5: ( 1 <= j0 & j0 <= width A ) by A1, MATRIXC1:1; ( 1 <= i0 & i0 <= len A ) by A2, A4, MATRIXC1:1; then A6: [i0,j0] in Indices A by A5, MATRIXC1:1; hence ((- 1) * A) * (i,j) = (- 1) * (A * (i0,j0)) by Th3 .= - (A * (i,j)) .= (- A) * (i,j) by A6, Lm3 ; ::_thesis: verum end; ( len (- A) = len A & width (- A) = width A ) by MATRIX_3:def_2; hence (- 1) * A = - A by A2, A1, A3, MATRIX_1:21; ::_thesis: verum end; theorem Th10: :: MATRIXR2:10 for A being Matrix of REAL for i, j being Element of NAT st [i,j] in Indices A holds (- A) * (i,j) = - (A * (i,j)) proof let A be Matrix of REAL; ::_thesis: for i, j being Element of NAT st [i,j] in Indices A holds (- A) * (i,j) = - (A * (i,j)) let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) ) assume A1: [i,j] in Indices A ; ::_thesis: (- A) * (i,j) = - (A * (i,j)) - A = (- 1) * A by Th9; then (- A) * (i,j) = (- 1) * (A * (i,j)) by A1, MATRIXR1:29; hence (- A) * (i,j) = - (A * (i,j)) ; ::_thesis: verum end; theorem :: MATRIXR2:11 for a, b being Real for A being Matrix of REAL holds (a * b) * A = a * (b * A) proof let a, b be Real; ::_thesis: for A being Matrix of REAL holds (a * b) * A = a * (b * A) let A be Matrix of REAL; ::_thesis: (a * b) * A = a * (b * A) A1: ( len ((a * b) * A) = len A & width ((a * b) * A) = width A ) by Th5; A2: len (a * (b * A)) = len (b * A) by Th5; A3: width (a * (b * A)) = width (b * A) by Th5; then A4: width (a * (b * A)) = width A by Th5; A5: ( len (b * A) = len A & width (b * A) = width A ) by Th5; A6: for i, j being Nat st [i,j] in Indices (a * (b * A)) holds (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (b * A)) implies (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) ) assume A7: [i,j] in Indices (a * (b * A)) ; ::_thesis: (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) A8: Indices (b * A) = Indices A by A5, MATRIX_4:55; reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; A9: Indices (a * (b * A)) = Indices (b * A) by A2, A3, MATRIX_4:55; then (a * (b * A)) * (i,j) = a * ((b * A) * (i0,j0)) by A7, Th3 .= a * (b * (A * (i0,j0))) by A7, A9, A8, Th3 .= (a * b) * (A * (i0,j0)) .= ((a * b) * A) * (i,j) by A7, A9, A8, Th3 ; hence (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) ; ::_thesis: verum end; len (a * (b * A)) = len A by A2, Th5; hence (a * b) * A = a * (b * A) by A1, A4, A6, MATRIX_1:21; ::_thesis: verum end; theorem Th12: :: MATRIXR2:12 for a, b being Real for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A) proof let a, b be Real; ::_thesis: for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A) let A be Matrix of REAL; ::_thesis: (a + b) * A = (a * A) + (b * A) A1: ( len (a * A) = len A & width (a * A) = width A ) by MATRIXR1:27; A2: ( len ((a + b) * A) = len A & width ((a + b) * A) = width A ) by MATRIXR1:27; A3: for i, j being Nat st [i,j] in Indices ((a + b) * A) holds ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a + b) * A) implies ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) ) assume A4: [i,j] in Indices ((a + b) * A) ; ::_thesis: ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; A5: Indices ((a + b) * A) = Indices A by A2, MATRIX_4:55; Indices (a * A) = Indices A by A1, MATRIX_4:55; then ((a * A) + (b * A)) * (i,j) = ((a * A) * (i0,j0)) + ((b * A) * (i0,j0)) by A4, A5, MATRIXR1:25 .= (a * (A * (i0,j0))) + ((b * A) * (i0,j0)) by A4, A5, MATRIXR1:29 .= (a * (A * (i0,j0))) + (b * (A * (i0,j0))) by A4, A5, MATRIXR1:29 .= (a + b) * (A * (i,j)) ; hence ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) by A4, A5, MATRIXR1:29; ::_thesis: verum end; ( len ((a * A) + (b * A)) = len (a * A) & width ((a * A) + (b * A)) = width (a * A) ) by MATRIX_3:def_3; hence (a + b) * A = (a * A) + (b * A) by A2, A1, A3, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIXR2:13 for a, b being Real for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A) proof let a, b be Real; ::_thesis: for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A) let A be Matrix of REAL; ::_thesis: (a - b) * A = (a * A) - (b * A) A1: ( len ((a - b) * A) = len A & width ((a - b) * A) = width A ) by MATRIXR1:27; A2: ( len (a * A) = len A & width (a * A) = width A ) by MATRIXR1:27; A3: ( len (b * A) = len A & width (b * A) = width A ) by MATRIXR1:27; A4: for i, j being Nat st [i,j] in Indices ((a - b) * A) holds ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a - b) * A) implies ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j) ) assume A5: [i,j] in Indices ((a - b) * A) ; ::_thesis: ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j) reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; A6: Indices ((a - b) * A) = Indices A by A1, MATRIX_4:55; Indices (a * A) = Indices A by A2, MATRIX_4:55; then ((a * A) - (b * A)) * (i,j) = ((a * A) * (i0,j0)) - ((b * A) * (i0,j0)) by A2, A3, A5, A6, Th6 .= (a * (A * (i0,j0))) - ((b * A) * (i0,j0)) by A5, A6, MATRIXR1:29 .= (a * (A * (i0,j0))) - (b * (A * (i0,j0))) by A5, A6, MATRIXR1:29 .= (a - b) * (A * (i,j)) ; hence ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j) by A5, A6, MATRIXR1:29; ::_thesis: verum end; A7: width ((a * A) - (b * A)) = width (MXF2MXR ((MXR2MXF (a * A)) + (- (MXR2MXF (b * A))))) by MATRIX_4:def_1 .= width (a * A) by MATRIX_3:def_3 ; len ((a * A) - (b * A)) = len (MXF2MXR ((MXR2MXF (a * A)) + (- (MXR2MXF (b * A))))) by MATRIX_4:def_1 .= len (a * A) by MATRIX_3:def_3 ; hence (a - b) * A = (a * A) - (b * A) by A1, A7, A2, A4, MATRIX_1:21; ::_thesis: verum end; theorem Th14: :: MATRIXR2:14 for n being Element of NAT for K being Field for A being Matrix of K st n > 0 & len A > 0 holds (0. (K,n,(len A))) * A = 0. (K,n,(width A)) proof let n be Element of NAT ; ::_thesis: for K being Field for A being Matrix of K st n > 0 & len A > 0 holds (0. (K,n,(len A))) * A = 0. (K,n,(width A)) let K be Field; ::_thesis: for A being Matrix of K st n > 0 & len A > 0 holds (0. (K,n,(len A))) * A = 0. (K,n,(width A)) let A be Matrix of K; ::_thesis: ( n > 0 & len A > 0 implies (0. (K,n,(len A))) * A = 0. (K,n,(width A)) ) assume that A1: n > 0 and A2: len A > 0 ; ::_thesis: (0. (K,n,(len A))) * A = 0. (K,n,(width A)) A3: len (0. (K,n,(len A))) = n by MATRIX_1:def_2; then A4: width (0. (K,n,(len A))) = len A by A1, MATRIX_1:20; then A5: len ((0. (K,n,(len A))) * A) = n by A3, MATRIX_3:def_4; A6: width ((0. (K,n,(len A))) * A) = width A by A4, MATRIX_3:def_4; ((0. (K,n,(len A))) * A) + ((0. (K,n,(len A))) * A) = ((0. (K,n,(len A))) + (0. (K,n,(len A)))) * A by A1, A2, A3, A4, MATRIX_4:63 .= (0. (K,n,(len A))) * A by MATRIX_3:4 ; hence (0. (K,n,(len A))) * A = 0. (K,n,(width A)) by A5, A6, MATRIX_4:6; ::_thesis: verum end; theorem Th15: :: MATRIXR2:15 for K being Field for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds (- C) * A = - (C * A) proof let K be Field; ::_thesis: for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds (- C) * A = - (C * A) let A, C be Matrix of K; ::_thesis: ( len A = width C & len C > 0 & len A > 0 implies (- C) * A = - (C * A) ) assume that A1: len A = width C and A2: len C > 0 and A3: len A > 0 ; ::_thesis: (- C) * A = - (C * A) A4: len C = len (- C) by MATRIX_3:def_2; A5: width (- C) = width C by MATRIX_3:def_2; then width ((- C) * A) = width A by A1, MATRIX_3:def_4; then A6: width (C * A) = width ((- C) * A) by A1, MATRIX_3:def_4; reconsider D = C as Matrix of len C, width C,K by A2, MATRIX_1:20; A7: width (- C) = width C by MATRIX_3:def_2; then A8: ( len ((- C) * A) = len (- C) & width ((- C) * A) = width A ) by A1, MATRIX_3:def_4; len (- C) = len ((- C) * A) by A1, A5, MATRIX_3:def_4; then A9: len (C * A) = len ((- C) * A) by A1, A4, MATRIX_3:def_4; len C = len (- C) by MATRIX_3:def_2; then (C * A) + ((- C) * A) = (D + (- D)) * A by A1, A2, A3, A7, MATRIX_4:63 .= (0. (K,(len C),(width C))) * A by MATRIX_3:5 .= 0. (K,(len C),(width A)) by A1, A2, A3, Th14 ; hence (- C) * A = - (C * A) by A4, A8, A9, A6, MATRIX_4:8; ::_thesis: verum end; theorem Th16: :: MATRIXR2:16 for K being Field for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds (B - C) * A = (B * A) - (C * A) proof let K be Field; ::_thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds (B - C) * A = (B * A) - (C * A) let A, B, C be Matrix of K; ::_thesis: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B - C) * A = (B * A) - (C * A) ) assume A1: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 ) ; ::_thesis: (B - C) * A = (B * A) - (C * A) A2: ( width (- C) = width C & len C = len (- C) ) by MATRIX_3:def_2; thus (B - C) * A = (B + (- C)) * A by MATRIX_4:def_1 .= (B * A) + ((- C) * A) by A1, A2, MATRIX_4:63 .= (B * A) + (- (C * A)) by A1, Th15 .= (B * A) - (C * A) by MATRIX_4:def_1 ; ::_thesis: verum end; theorem :: MATRIXR2:17 for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = width A & len A > 0 & len C > 0 holds (A - B) * C = (A * C) - (B * C) by Th16; theorem Th18: :: MATRIXR2:18 for K being Field for m being Element of NAT for A, C being Matrix of K st width A > 0 & len A > 0 holds A * (0. (K,(width A),m)) = 0. (K,(len A),m) proof let K be Field; ::_thesis: for m being Element of NAT for A, C being Matrix of K st width A > 0 & len A > 0 holds A * (0. (K,(width A),m)) = 0. (K,(len A),m) let m be Element of NAT ; ::_thesis: for A, C being Matrix of K st width A > 0 & len A > 0 holds A * (0. (K,(width A),m)) = 0. (K,(len A),m) let A, C be Matrix of K; ::_thesis: ( width A > 0 & len A > 0 implies A * (0. (K,(width A),m)) = 0. (K,(len A),m) ) assume that A1: width A > 0 and A2: len A > 0 ; ::_thesis: A * (0. (K,(width A),m)) = 0. (K,(len A),m) A3: len (0. (K,(width A),m)) = width A by MATRIX_1:def_2; then m = width (0. (K,(width A),m)) by A1, MATRIX_1:20; then A4: width (A * (0. (K,(width A),m))) = m by A3, MATRIX_3:def_4; width (0. (K,(width A),m)) = m by A1, A3, MATRIX_1:20; then A5: (A * (0. (K,(width A),m))) + (A * (0. (K,(width A),m))) = A * ((0. (K,(width A),m)) + (0. (K,(width A),m))) by A1, A2, A3, MATRIX_4:62 .= A * (0. (K,(width A),m)) by MATRIX_3:4 ; len (A * (0. (K,(width A),m))) = len A by A3, MATRIX_3:def_4; hence A * (0. (K,(width A),m)) = 0. (K,(len A),m) by A4, A5, MATRIX_4:6; ::_thesis: verum end; theorem Th19: :: MATRIXR2:19 for K being Field for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds A * (- C) = - (A * C) proof let K be Field; ::_thesis: for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds A * (- C) = - (A * C) let A, C be Matrix of K; ::_thesis: ( width A = len C & len A > 0 & len C > 0 implies A * (- C) = - (A * C) ) assume that A1: width A = len C and A2: len A > 0 and A3: len C > 0 ; ::_thesis: A * (- C) = - (A * C) A4: len C = len (- C) by MATRIX_3:def_2; then A5: len A = len (A * (- C)) by A1, MATRIX_3:def_4; width (- C) = width C by MATRIX_3:def_2; then A6: width (A * (- C)) = width C by A1, A4, MATRIX_3:def_4; reconsider D = C as Matrix of len C, width C,K by A3, MATRIX_1:20; A7: ( len (A * C) = len A & width (A * C) = width C ) by A1, MATRIX_3:def_4; ( len C = len (- C) & width (- C) = width C ) by MATRIX_3:def_2; then (A * C) + (A * (- C)) = A * (D + (- D)) by A1, A2, A3, MATRIX_4:62 .= A * (0. (K,(len C),(width C))) by MATRIX_3:5 .= 0. (K,(len A),(width C)) by A1, A2, A3, Th18 ; hence A * (- C) = - (A * C) by A7, A5, A6, MATRIX_4:8; ::_thesis: verum end; theorem Th20: :: MATRIXR2:20 for K being Field for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds A * (B - C) = (A * B) - (A * C) proof let K be Field; ::_thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds A * (B - C) = (A * B) - (A * C) let A, B, C be Matrix of K; ::_thesis: ( len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 implies A * (B - C) = (A * B) - (A * C) ) assume that A1: len B = len C and A2: width B = width C and A3: ( len B = width A & len B > 0 & len A > 0 ) ; ::_thesis: A * (B - C) = (A * B) - (A * C) A4: ( width (- C) = width C & len C = len (- C) ) by MATRIX_3:def_2; thus A * (B - C) = A * (B + (- C)) by MATRIX_4:def_1 .= (A * B) + (A * (- C)) by A1, A2, A3, A4, MATRIX_4:62 .= (A * B) + (- (A * C)) by A1, A3, Th19 .= (A * B) - (A * C) by MATRIX_4:def_1 ; ::_thesis: verum end; theorem :: MATRIXR2:21 for A, B, C being Matrix of REAL st len A = len B & width A = width B & width C = len A & len C > 0 & len A > 0 holds C * (A - B) = (C * A) - (C * B) by Th20; theorem Th22: :: MATRIXR2:22 for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Element of 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 A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Element of 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 A = len B & width A = width B ) and A2: ( len C = len A & width C = width A ) and A3: for i, j being Element of NAT st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) - (B * (i,j)) ; ::_thesis: C = A - B A4: Indices B = Indices A by A1, MATRIX_4:55; for i, j being Nat st [i,j] in Indices A holds C * (i,j) = (A * (i,j)) + ((- B) * (i,j)) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies C * (i,j) = (A * (i,j)) + ((- B) * (i,j)) ) reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; assume A5: [i,j] in Indices A ; ::_thesis: C * (i,j) = (A * (i,j)) + ((- B) * (i,j)) hence C * (i,j) = (A * (i0,j0)) - (B * (i0,j0)) by A3 .= (A * (i0,j0)) + (- (B * (i0,j0))) .= (A * (i,j)) + ((- B) * (i,j)) by A4, A5, Th10 ; ::_thesis: verum end; then C = A + (- B) by A2, MATRIXR1:26; hence C = A - B by MATRIX_4:def_1; ::_thesis: verum end; theorem Th23: :: MATRIXR2:23 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) ) A1: ( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 ) by MATRIXR1:def_10; A2: Seg (width (LineVec2Mx x1)) = Seg (len x1) by MATRIXR1:def_10 .= dom x1 by FINSEQ_1:def_3 ; A3: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def_3 .= Seg 1 by MATRIXR1:def_10 ; assume A4: len x1 = len x2 ; ::_thesis: LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) then A5: dom x1 = dom x2 by FINSEQ_3:29; A6: ( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 ) by MATRIXR1:def_10; then A7: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A4, A1, MATRIX_4:55; A8: len (x1 - x2) = len x1 by A4, RVSUM_1:116; then A9: dom (x1 - x2) = dom x1 by FINSEQ_3:29; A10: ( width (LineVec2Mx (x1 - x2)) = len (x1 - x2) & len (LineVec2Mx (x1 - x2)) = 1 ) by MATRIXR1:def_10; then A11: Indices (LineVec2Mx (x1 - x2)) = Indices (LineVec2Mx x1) by A4, A1, MATRIX_4:55, RVSUM_1:116; for i, j being Element of 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 Element of NAT ; ::_thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j)) ) assume A12: [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 A13: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5; i in Seg 1 by A3, A12, ZFMISC_1:87; then ( 1 <= i & i <= 1 ) by FINSEQ_1:1; then A14: i = 1 by XXREAL_0:1; A15: j in dom x1 by A2, A12, ZFMISC_1:87; then A16: q1 . j = x1 . j by A14, A13, MATRIXR1:def_10; consider p being FinSequence of REAL such that p = (LineVec2Mx (x1 - x2)) . i and A17: (LineVec2Mx (x1 - x2)) * (i,j) = p . j by A11, A12, MATRIX_1:def_5; consider q2 being FinSequence of REAL such that q2 = (LineVec2Mx x2) . i and A18: (LineVec2Mx x2) * (i,j) = q2 . j by A7, A12, MATRIX_1:def_5; A19: q2 . j = x2 . j by A5, A15, A14, A18, MATRIXR1:def_10; p . j = (x1 - x2) . j by A9, A15, A14, A17, MATRIXR1:def_10; hence (LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j)) by A4, A17, A13, A16, A18, A19, Lm1; ::_thesis: verum end; hence LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) by A4, A8, A10, A1, A6, Th22; ::_thesis: verum end; theorem Th24: :: MATRIXR2:24 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, MATRIXR1:def_9; A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, MATRIXR1:def_9; A5: dom x1 = dom x2 by A1, FINSEQ_3:29; A6: len (x1 - x2) = len x1 by A1, RVSUM_1:116; then A7: dom (x1 - x2) = dom x1 by FINSEQ_3:29; A8: len (ColVec2Mx x1) = len x1 by A2, MATRIXR1:def_9; then A9: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29; A10: ( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, MATRIXR1:def_9; then A11: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A8, A3, MATRIX_4:55; A12: ( len (ColVec2Mx (x1 - x2)) = len (x1 - x2) & width (ColVec2Mx (x1 - x2)) = 1 ) by A2, A6, MATRIXR1:def_9; then A13: Indices (ColVec2Mx (x1 - x2)) = Indices (ColVec2Mx x1) by A1, A8, A3, MATRIX_4:55, RVSUM_1:116; for i, j being Element of 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 Element of NAT ; ::_thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j)) ) assume A14: [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 A15: q1 = (ColVec2Mx x1) . i and A16: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5; j in Seg 1 by A4, A14, ZFMISC_1:87; then ( 1 <= j & j <= 1 ) by FINSEQ_1:1; then A17: j = 1 by XXREAL_0:1; A18: i in dom x1 by A9, A14, ZFMISC_1:87; then (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, MATRIXR1:def_9; then A19: q1 . j = x1 . i by A17, A15, FINSEQ_1:40; consider p being FinSequence of REAL such that A20: p = (ColVec2Mx (x1 - x2)) . i and A21: (ColVec2Mx (x1 - x2)) * (i,j) = p . j by A13, A14, MATRIX_1:def_5; consider q2 being FinSequence of REAL such that A22: q2 = (ColVec2Mx x2) . i and A23: (ColVec2Mx x2) * (i,j) = q2 . j by A11, A14, MATRIX_1:def_5; (ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A18, MATRIXR1:def_9; then A24: q2 . j = x2 . i by A17, A22, FINSEQ_1:40; (ColVec2Mx (x1 - x2)) . i = <*((x1 - x2) . i)*> by A2, A6, A7, A18, MATRIXR1:def_9; then p . j = (x1 - x2) . i by A17, A20, FINSEQ_1:40; hence (ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j)) by A1, A21, A16, A19, A23, A24, Lm1; ::_thesis: verum end; hence ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2) by A1, A6, A8, A12, A3, A10, Th22; ::_thesis: verum end; theorem Th25: :: MATRIXR2:25 for A, B being Matrix of REAL st len A = len B & 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: ( len A = len B & 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 that A1: len A = len B and A2: 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)) A3: width (A - B) = width A by A1, A2, Th6; let i be Nat; ::_thesis: ( 1 <= i & i <= len A implies Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) ) A4: len (Line (A,i)) = width A by MATRIX_1:def_7; A5: len (Line (B,i)) = width B by MATRIX_1:def_7; assume ( 1 <= i & i <= len A ) ; ::_thesis: Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) then A6: i in dom A by FINSEQ_3:25; A7: for j being Nat st j in Seg (width (A - B)) holds ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) proof reconsider i2 = i as Element of NAT by ORDINAL1:def_12; let j be Nat; ::_thesis: ( j in Seg (width (A - B)) implies ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) ) reconsider j2 = j as Element of NAT by ORDINAL1:def_12; A8: ((Line (A,i2)) - (Line (B,i2))) . j = ((Line (A,i2)) . j2) - ((Line (B,i2)) . j2) by A2, A4, A5, Lm1; assume A9: j in Seg (width (A - B)) ; ::_thesis: ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) then [i,j] in Indices A by A6, A3, ZFMISC_1:87; then A10: (A - B) * (i2,j2) = (A * (i2,j2)) - (B * (i2,j2)) by A1, A2, Th6; A11: j in Seg (width A) by A1, A2, A9, Th6; then (Line (A,i)) . j = A * (i,j) by MATRIX_1:def_7; hence ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) by A2, A11, A10, A8, MATRIX_1:def_7; ::_thesis: verum end; len ((Line (A,i)) - (Line (B,i))) = len (Line (A,i)) by A2, A4, A5, RVSUM_1:116; hence Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) by A4, A3, A7, MATRIX_1:def_7; ::_thesis: verum end; theorem Th26: :: MATRIXR2:26 for A, B being Matrix of REAL st len A = len B & width A = width 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 & width A = width B implies for i being Nat st 1 <= i & i <= width A holds Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) ) assume that A1: len A = len B and A2: width A = width B ; ::_thesis: for i being Nat st 1 <= i & i <= width A holds Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) A3: len (A - B) = len A by A1, A2, Th6; let i be Nat; ::_thesis: ( 1 <= i & i <= width A implies Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) ) A4: len (Col (A,i)) = len A by MATRIX_1:def_8; 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 (Col (B,i)) = len B by MATRIX_1:def_8; A7: dom A = dom B by A1, FINSEQ_3:29; A8: 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 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 A3, 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 A7, A9, MATRIX_1:def_8; then ((Col (A,i)) . j) - ((Col (B,i)) . j) = (A - B) * (j,i) by A1, A2, A5, A10, Th6; hence ((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i) by A1, A4, A6, Lm1; ::_thesis: verum end; len ((Col (A,i)) - (Col (B,i))) = len (Col (A,i)) by A1, A4, A6, RVSUM_1:116; hence Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) by A4, A3, A8, MATRIX_1:def_8; ::_thesis: verum end; theorem :: MATRIXR2:27 for n, k, m, l being Element of NAT for A being Matrix of n,k, REAL for B being Matrix of k,m, REAL for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds (A * B) * C = A * (B * C) proof let n, k, m, l be Element of NAT ; ::_thesis: for A being Matrix of n,k, REAL for B being Matrix of k,m, REAL for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds (A * B) * C = A * (B * C) let A be Matrix of n,k, REAL ; ::_thesis: for B being Matrix of k,m, REAL for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds (A * B) * C = A * (B * C) let B be Matrix of k,m, REAL ; ::_thesis: for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds (A * B) * C = A * (B * C) let C be Matrix of m,l, REAL ; ::_thesis: ( n > 0 & k > 0 & m > 0 implies (A * B) * C = A * (B * C) ) assume that A1: n > 0 and A2: k > 0 and A3: m > 0 ; ::_thesis: (A * B) * C = A * (B * C) A4: ( width B = m & len C = m ) by A2, A3, MATRIX_1:23; ( width A = k & len B = k ) by A1, A2, MATRIX_1:23; hence (A * B) * C = A * (B * C) by A4, MATRIX_3:33; ::_thesis: verum end; theorem Th28: :: MATRIXR2:28 for n being Element of NAT for A, B, C being Matrix of n, REAL holds (A * B) * C = A * (B * C) proof let n be Element of NAT ; ::_thesis: for A, B, C being Matrix of n, REAL holds (A * B) * C = A * (B * C) let A, B, C be Matrix of n, REAL ; ::_thesis: (A * B) * C = A * (B * C) A1: ( width B = n & len C = n ) by MATRIX_1:24; ( width A = n & len B = n ) by MATRIX_1:24; hence (A * B) * C = A * (B * C) by A1, MATRIX_3:33; ::_thesis: verum end; theorem Th29: :: MATRIXR2:29 for D being non empty set for n being Element of NAT for A being Matrix of n,D holds (A @) @ = A proof let D be non empty set ; ::_thesis: for n being Element of NAT for A being Matrix of n,D holds (A @) @ = A let n be Element of NAT ; ::_thesis: for A being Matrix of n,D holds (A @) @ = A let A be Matrix of n,D; ::_thesis: (A @) @ = A reconsider N = A @ as Matrix of n,D ; A1: ( len A = n & width A = n ) by MATRIX_1:24; A2: Indices (N @) = [:(Seg n),(Seg n):] by MATRIX_1:24 .= Indices A by MATRIX_1:24 ; A3: for i, j being Nat st [i,j] in Indices (N @) holds (N @) * (i,j) = A * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (N @) implies (N @) * (i,j) = A * (i,j) ) assume A4: [i,j] in Indices (N @) ; ::_thesis: (N @) * (i,j) = A * (i,j) then [j,i] in Indices N by MATRIX_1:def_6; then (N @) * (i,j) = N * (j,i) by MATRIX_1:def_6; hence (N @) * (i,j) = A * (i,j) by A2, A4, MATRIX_1:def_6; ::_thesis: verum end; ( len (N @) = n & width (N @) = n ) by MATRIX_1:24; hence (A @) @ = A by A1, A3, MATRIX_1:21; ::_thesis: verum end; theorem Th30: :: MATRIXR2:30 for n being Element of NAT for A, B being Matrix of n, REAL holds (A * B) @ = (B @) * (A @) proof let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL holds (A * B) @ = (B @) * (A @) let A, B be Matrix of n, REAL ; ::_thesis: (A * B) @ = (B @) * (A @) A1: len A = n by MATRIX_1:24; A2: ( width A = n & len B = n ) by MATRIX_1:24; A3: len (A * B) = n by MATRIX_1:24; A4: width B = n by MATRIX_1:24; A5: len (B @) = n by MATRIX_1:24; then A6: len ((B @) * (A @)) = len (B @) by MATRIX_1:24; A7: width (B @) = n by MATRIX_1:24 .= len (A @) by MATRIX_1:24 ; A8: width (A * B) = n by MATRIX_1:24; A9: width (A @) = n by MATRIX_1:24; then A10: width ((B @) * (A @)) = width (A @) by MATRIX_1:24; A11: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((A_*_B)_@)_holds_ ((B_@)_*_(A_@))_*_(i,j)_=_((A_*_B)_@)_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices ((A * B) @) implies ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j) ) A12: Indices ((A * B) @) = [:(Seg n),(Seg n):] by MATRIX_1:24; assume A13: [i,j] in Indices ((A * B) @) ; ::_thesis: ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j) then j in Seg (len (A * B)) by A3, A12, ZFMISC_1:87; then A14: j in dom (A * B) by FINSEQ_1:def_3; i in Seg (width (A * B)) by A8, A13, A12, ZFMISC_1:87; then A15: [j,i] in Indices (A * B) by A14, ZFMISC_1:87; Seg (width (A @)) = dom A by A1, A9, FINSEQ_1:def_3; then j in dom A by A9, A13, A12, ZFMISC_1:87; then A16: Col ((A @),j) = Line (A,j) by MATRIX_2:14; reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; A17: Seg (width B) = dom (B @) by A4, A5, FINSEQ_1:def_3; A18: Indices ((B @) * (A @)) = [:(Seg n),(Seg n):] by MATRIX_1:24; then [i,j] in [:(dom (B @)),(Seg (width (A @))):] by A6, A10, A13, A12, FINSEQ_3:29; then i in Seg (width B) by A17, ZFMISC_1:87; then Line ((B @),i) = Col (B,i) by MATRIX_2:15; hence ((B @) * (A @)) * (i,j) = (Col (B,i0)) "*" (Line (A,j0)) by A7, A13, A12, A18, A16, MATRPROB:39 .= (A * B) * (j0,i0) by A2, A15, MATRPROB:39 .= ((A * B) @) * (i,j) by A15, MATRIX_1:def_6 ; ::_thesis: verum end; A19: ( len ((B @) * (A @)) = n & width ((B @) * (A @)) = n ) by MATRIX_1:24; ( len ((A * B) @) = n & width ((A * B) @) = n ) by MATRIX_1:24; hence (A * B) @ = (B @) * (A @) by A19, A11, MATRIX_1:21; ::_thesis: verum end; theorem Th31: :: MATRIXR2:31 for n, m being Element of NAT for A being Matrix of REAL st len A = n & width A = m holds (- A) + A = 0_Rmatrix (n,m) proof let n, m be Element of NAT ; ::_thesis: for A being Matrix of REAL st len A = n & width A = m holds (- A) + A = 0_Rmatrix (n,m) let A be Matrix of REAL; ::_thesis: ( len A = n & width A = m implies (- A) + A = 0_Rmatrix (n,m) ) assume A1: ( len A = n & width A = m ) ; ::_thesis: (- A) + A = 0_Rmatrix (n,m) ( len (- (MXR2MXF A)) = len A & width (- (MXR2MXF A)) = width A ) by MATRIX_3:def_2; hence (- A) + A = MXF2MXR ((MXR2MXF A) + (- (MXR2MXF A))) by MATRIX_3:2 .= 0_Rmatrix (n,m) by A1, MATRIX_4:2 ; ::_thesis: verum end; begin definition let n be Element of NAT ; let A be Matrix of n, REAL ; :: original: MXR2MXF redefine func MXR2MXF A -> Matrix of n,F_Real; coherence MXR2MXF A is Matrix of n,F_Real ; end; definition let n be Element of NAT ; let A be Matrix of n, REAL ; func Det A -> Real equals :: MATRIXR2:def 1 Det (MXR2MXF A); coherence Det (MXR2MXF A) is Real ; end; :: deftheorem defines Det MATRIXR2:def_1_:_ for n being Element of NAT for A being Matrix of n, REAL holds Det A = Det (MXR2MXF A); theorem :: MATRIXR2:32 for A being Matrix of 2, REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1))) proof let A be Matrix of 2, REAL ; ::_thesis: Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1))) reconsider N = MXR2MXF A as Matrix of 2,F_Real ; Det A = ((N * (1,1)) * (N * (2,2))) - ((N * (1,2)) * (N * (2,1))) by MATRIX_7:12; hence Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1))) ; ::_thesis: verum end; theorem Th33: :: MATRIXR2:33 for n being Element of NAT for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds <*s1,s2,s3*> is tabular proof let n be Element of NAT ; ::_thesis: for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds <*s1,s2,s3*> is tabular let s1, s2, s3 be FinSequence; ::_thesis: ( len s1 = n & len s2 = n & len s3 = n implies <*s1,s2,s3*> is tabular ) assume A1: ( len s1 = n & len s2 = n & len s3 = n ) ; ::_thesis: <*s1,s2,s3*> is tabular now__::_thesis:_ex_n_being_Element_of_NAT_st_ for_x_being_set_st_x_in_rng_<*s1,s2,s3*>_holds_ ex_r_being_FinSequence_st_ (_x_=_r_&_len_r_=_n_) take n = n; ::_thesis: for x being set st x in rng <*s1,s2,s3*> holds ex r being FinSequence st ( x = r & len r = n ) let x be set ; ::_thesis: ( x in rng <*s1,s2,s3*> implies ex r being FinSequence st ( x = r & len r = n ) ) assume x in rng <*s1,s2,s3*> ; ::_thesis: ex r being FinSequence st ( x = r & len r = n ) then A2: x in {s1,s2,s3} by FINSEQ_2:128; then reconsider r = x as FinSequence by ENUMSET1:def_1; take r = r; ::_thesis: ( x = r & len r = n ) thus ( x = r & len r = n ) by A1, A2, ENUMSET1:def_1; ::_thesis: verum end; hence <*s1,s2,s3*> is tabular by MATRIX_1:def_1; ::_thesis: verum end; theorem Th34: :: MATRIXR2:34 for D being non empty set for n being Element of NAT for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds <*p1,p2,p3*> is Matrix of 3,n,D proof let D be non empty set ; ::_thesis: for n being Element of NAT for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds <*p1,p2,p3*> is Matrix of 3,n,D let n be Element of NAT ; ::_thesis: for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds <*p1,p2,p3*> is Matrix of 3,n,D let p1, p2, p3 be FinSequence of D; ::_thesis: ( len p1 = n & len p2 = n & len p3 = n implies <*p1,p2,p3*> is Matrix of 3,n,D ) reconsider q1 = p1, q2 = p2, q3 = p3 as Element of D * by FINSEQ_1:def_11; reconsider M = <*q1,q2,q3*> as FinSequence of D * ; assume A1: ( len p1 = n & len p2 = n & len p3 = n ) ; ::_thesis: <*p1,p2,p3*> is Matrix of 3,n,D then reconsider M = M as Matrix of D by Th33; M is Matrix of 3,n,D proof thus len M = 3 by FINSEQ_1:45; :: according to MATRIX_1:def_2 ::_thesis: for b1 being FinSequence of D holds ( not b1 in rng M or len b1 = n ) let r be FinSequence of D; ::_thesis: ( not r in rng M or len r = n ) assume r in rng M ; ::_thesis: len r = n then r in {p1,p2,p3} by FINSEQ_2:128; hence len r = n by A1, ENUMSET1:def_1; ::_thesis: verum end; hence <*p1,p2,p3*> is Matrix of 3,n,D ; ::_thesis: verum end; theorem Th35: :: MATRIXR2:35 for D being non empty set for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D proof let D be non empty set ; ::_thesis: for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D let a1, a2, a3, b1, b2, b3, c1, c2, c3 be Element of D; ::_thesis: <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D A1: len <*c1,c2,c3*> = 3 by FINSEQ_1:45; ( len <*a1,a2,a3*> = 3 & len <*b1,b2,b3*> = 3 ) by FINSEQ_1:45; hence <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D by A1, Th34; ::_thesis: verum end; theorem Th36: :: MATRIXR2:36 for D being non empty set for n being Element of NAT for A being Matrix of n,D for p being FinSequence of D for i being Nat st p = A . i & i in Seg n holds len p = n proof let D be non empty set ; ::_thesis: for n being Element of NAT for A being Matrix of n,D for p being FinSequence of D for i being Nat st p = A . i & i in Seg n holds len p = n let n be Element of NAT ; ::_thesis: for A being Matrix of n,D for p being FinSequence of D for i being Nat st p = A . i & i in Seg n holds len p = n let A be Matrix of n,D; ::_thesis: for p being FinSequence of D for i being Nat st p = A . i & i in Seg n holds len p = n let p be FinSequence of D; ::_thesis: for i being Nat st p = A . i & i in Seg n holds len p = n let i be Nat; ::_thesis: ( p = A . i & i in Seg n implies len p = n ) assume that A1: p = A . i and A2: i in Seg n ; ::_thesis: len p = n consider n2 being Nat such that A3: for x being set st x in rng A holds ex s being FinSequence of D st ( s = x & len s = n2 ) by MATRIX_1:9; len A = n by MATRIX_1:24; then A4: i in dom A by A2, FINSEQ_1:def_3; then A . i in rng A by FUNCT_1:def_3; then consider s being FinSequence of D such that A5: s = A . i and len s = n2 by A3; s in rng A by A4, A5, FUNCT_1:def_3; hence len p = n by A1, A5, MATRIX_1:def_2; ::_thesis: verum end; theorem Th37: :: MATRIXR2:37 for D being non empty set for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> proof let D be non empty set ; ::_thesis: for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> let A be Matrix of 3,D; ::_thesis: A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> reconsider B = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> as Matrix of 3,D by Th35; A1: ( len A = 3 & width A = 3 ) by MATRIX_1:24; A2: 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) ) A3: Indices B = [:(Seg 3),(Seg 3):] by MATRIX_1:24; A4: Indices A = [:(Seg 3),(Seg 3):] by MATRIX_1:24; assume A5: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j) then A6: i in Seg 3 by A4, ZFMISC_1:87; 2 in Seg 3 ; then A7: [i,2] in Indices A by A4, A6, ZFMISC_1:87; 1 in Seg 3 ; then A8: [i,1] in Indices A by A4, A6, ZFMISC_1:87; 3 in Seg 3 ; then A9: [i,3] in Indices A by A4, A6, ZFMISC_1:87; A10: i in {1,2,3} by A5, A4, FINSEQ_3:1, ZFMISC_1:87; now__::_thesis:_(_(_i_=_1_&_ex_p_being_FinSequence_of_D_st_ (_p_=_A_._i_&_B_*_(i,j)_=_p_._j_)_)_or_(_i_=_2_&_ex_p_being_FinSequence_of_D_st_ (_p_=_A_._i_&_B_*_(i,j)_=_p_._j_)_)_or_(_i_=_3_&_ex_p_being_FinSequence_of_D_st_ (_p_=_A_._i_&_B_*_(i,j)_=_p_._j_)_)_) percases ( i = 1 or i = 2 or i = 3 ) by A10, ENUMSET1:def_1; caseA11: i = 1 ; ::_thesis: ex p being FinSequence of D st ( p = A . i & B * (i,j) = p . j ) reconsider p0 = <*(A * (1,1)),(A * (1,2)),(A * (1,3))*> as FinSequence of D ; A12: len p0 = 3 by FINSEQ_1:45; A13: ex p23 being FinSequence of D st ( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_1:def_5; consider p2 being FinSequence of D such that A14: p2 = A . i and A15: A * (i,1) = p2 . 1 by A8, MATRIX_1:def_5; A16: ex p22 being FinSequence of D st ( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_1:def_5; A17: for k being Nat st 1 <= k & k <= len p0 holds p0 . k = p2 . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k ) assume A18: ( 1 <= k & k <= len p0 ) ; ::_thesis: p0 . k = p2 . k k in NAT by ORDINAL1:def_12; then A19: k in Seg 3 by A12, A18; percases ( k = 1 or k = 2 or k = 3 ) by A19, ENUMSET1:def_1, FINSEQ_3:1; suppose k = 1 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A11, A15, FINSEQ_1:45; ::_thesis: verum end; suppose k = 2 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A11, A14, A16, FINSEQ_1:45; ::_thesis: verum end; suppose k = 3 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A11, A14, A13, FINSEQ_1:45; ::_thesis: verum end; end; end; ex p being FinSequence of D st ( p = B . i & B * (i,j) = p . j ) by A5, A3, A4, MATRIX_1:def_5; then A20: B * (i,j) = p0 . j by A11, FINSEQ_1:45; len p2 = 3 by A6, A14, Th36; hence ex p being FinSequence of D st ( p = A . i & B * (i,j) = p . j ) by A12, A14, A17, A20, FINSEQ_1:14; ::_thesis: verum end; caseA21: i = 2 ; ::_thesis: ex p being FinSequence of D st ( p = A . i & B * (i,j) = p . j ) reconsider p0 = <*(A * (2,1)),(A * (2,2)),(A * (2,3))*> as FinSequence of D ; A22: len p0 = 3 by FINSEQ_1:45; A23: ex p23 being FinSequence of D st ( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_1:def_5; consider p2 being FinSequence of D such that A24: p2 = A . i and A25: A * (i,1) = p2 . 1 by A8, MATRIX_1:def_5; A26: ex p22 being FinSequence of D st ( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_1:def_5; A27: for k being Nat st 1 <= k & k <= len p0 holds p0 . k = p2 . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k ) assume A28: ( 1 <= k & k <= len p0 ) ; ::_thesis: p0 . k = p2 . k k in NAT by ORDINAL1:def_12; then A29: k in {1,2,3} by A22, A28, FINSEQ_3:1; percases ( k = 1 or k = 2 or k = 3 ) by A29, ENUMSET1:def_1; suppose k = 1 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A21, A25, FINSEQ_1:45; ::_thesis: verum end; suppose k = 2 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A21, A24, A26, FINSEQ_1:45; ::_thesis: verum end; suppose k = 3 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A21, A24, A23, FINSEQ_1:45; ::_thesis: verum end; end; end; ex p being FinSequence of D st ( p = B . i & B * (i,j) = p . j ) by A5, A3, A4, MATRIX_1:def_5; then A30: B * (i,j) = p0 . j by A21, FINSEQ_1:45; len p2 = 3 by A6, A24, Th36; hence ex p being FinSequence of D st ( p = A . i & B * (i,j) = p . j ) by A22, A24, A27, A30, FINSEQ_1:14; ::_thesis: verum end; caseA31: i = 3 ; ::_thesis: ex p being FinSequence of D st ( p = A . i & B * (i,j) = p . j ) reconsider p0 = <*(A * (3,1)),(A * (3,2)),(A * (3,3))*> as FinSequence of D ; A32: len p0 = 3 by FINSEQ_1:45; A33: ex p23 being FinSequence of D st ( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_1:def_5; consider p2 being FinSequence of D such that A34: p2 = A . i and A35: A * (i,1) = p2 . 1 by A8, MATRIX_1:def_5; A36: ex p22 being FinSequence of D st ( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_1:def_5; A37: for k being Nat st 1 <= k & k <= len p0 holds p0 . k = p2 . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k ) assume A38: ( 1 <= k & k <= len p0 ) ; ::_thesis: p0 . k = p2 . k k in NAT by ORDINAL1:def_12; then A39: k in {1,2,3} by A32, A38, FINSEQ_3:1; percases ( k = 1 or k = 2 or k = 3 ) by A39, ENUMSET1:def_1; suppose k = 1 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A31, A35, FINSEQ_1:45; ::_thesis: verum end; suppose k = 2 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A31, A34, A36, FINSEQ_1:45; ::_thesis: verum end; suppose k = 3 ; ::_thesis: p0 . k = p2 . k hence p0 . k = p2 . k by A31, A34, A33, FINSEQ_1:45; ::_thesis: verum end; end; end; ex p being FinSequence of D st ( p = B . i & B * (i,j) = p . j ) by A5, A3, A4, MATRIX_1:def_5; then A40: B * (i,j) = p0 . j by A31, FINSEQ_1:45; len p2 = 3 by A6, A34, Th36; hence ex p being FinSequence of D st ( p = A . i & B * (i,j) = p . j ) by A32, A34, A37, A40, FINSEQ_1:14; ::_thesis: verum end; end; end; hence A * (i,j) = B * (i,j) by A5, MATRIX_1:def_5; ::_thesis: verum end; ( len B = 3 & width B = 3 ) by MATRIX_1:24; hence A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> by A1, A2, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIXR2:38 for A being Matrix of 3, REAL holds Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))) proof let A be Matrix of 3, REAL ; ::_thesis: Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))) reconsider N = MXR2MXF A as Matrix of 3,F_Real ; reconsider N2 = <*<*(N * (1,1)),(N * (1,2)),(N * (1,3))*>,<*(N * (2,1)),(N * (2,2)),(N * (2,3))*>,<*(N * (3,1)),(N * (3,2)),(N * (3,3))*>*> as Matrix of 3,F_Real by Th35; Det A = Det N2 by Th37 .= (((((((N * (1,1)) * (N * (2,2))) * (N * (3,3))) - (((N * (1,3)) * (N * (2,2))) * (N * (3,1)))) - (((N * (1,1)) * (N * (2,3))) * (N * (3,2)))) + (((N * (1,2)) * (N * (2,3))) * (N * (3,1)))) - (((N * (1,2)) * (N * (2,1))) * (N * (3,3)))) + (((N * (1,3)) * (N * (2,1))) * (N * (3,2))) by MATRIX_9:46 ; hence Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))) ; ::_thesis: verum end; theorem :: MATRIXR2:39 for f being Permutation of (Seg 0) holds f = <*> NAT ; Lm4: idseq 0 is Permutation of (Seg 0) by FINSEQ_2:55; theorem Th40: :: MATRIXR2:40 Permutations 0 = {(<*> NAT)} proof now__::_thesis:_for_p_being_set_st_p_in_Permutations_0_holds_ p_in_{(<*>_NAT)} let p be set ; ::_thesis: ( p in Permutations 0 implies p in {(<*> NAT)} ) assume p in Permutations 0 ; ::_thesis: p in {(<*> NAT)} then reconsider q = p as Permutation of (Seg 0) by MATRIX_2:def_9; q = <*> NAT ; hence p in {(<*> NAT)} by TARSKI:def_1; ::_thesis: verum end; then A1: Permutations 0 c= {(<*> NAT)} by TARSKI:def_3; {(<*> NAT)} c= Permutations 0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(<*> NAT)} or x in Permutations 0 ) assume x in {(<*> NAT)} ; ::_thesis: x in Permutations 0 then x is Permutation of (Seg 0) by Lm4, TARSKI:def_1; hence x in Permutations 0 by MATRIX_2:def_9; ::_thesis: verum end; hence Permutations 0 = {(<*> NAT)} by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th41: :: MATRIXR2:41 for K being Field for A being Matrix of 0 ,K holds Det A = 1. K proof let K be Field; ::_thesis: for A being Matrix of 0 ,K holds Det A = 1. K reconsider kk = idseq 0 as Element of Permutations 0 by Th40, TARSKI:def_1; let A be Matrix of 0 ,K; ::_thesis: Det A = 1. K A1: (Path_product A) . (idseq 0) = 1. K proof reconsider p = idseq 0 as Element of Permutations 0 by Lm4, MATRIX_2:def_9; A2: - ((1_ K),p) = 1_ K proof reconsider q = id (Seg 0) as Element of Permutations 0 by Lm4, MATRIX_2:def_9; len (Permutations 0) = 0 by MATRIX_2:18; then q is even by MATRIX_2:25; hence - ((1_ K),p) = 1_ K by MATRIX_2:def_13; ::_thesis: verum end; 1_ K is_a_unity_wrt the multF of K by GROUP_1:21; then ( len (Path_matrix (p,A)) = 0 & the multF of K is having_a_unity ) by MATRIX_3:def_7, SETWISEO:def_2; then the multF of K $$ (Path_matrix (p,A)) = the_unity_wrt the multF of K by FINSOP_1:def_1 .= 1_ K by GROUP_1:22 ; hence (Path_product A) . (idseq 0) = 1. K by A2, MATRIX_3:def_8; ::_thesis: verum end; A3: FinOmega (Permutations 0) = Permutations 0 by Th40, MATRIX_2:def_14 .= {.kk.} by Th40 ; Det A = the addF of K $$ ((FinOmega (Permutations 0)),(Path_product A)) by MATRIX_3:def_9 .= 1. K by A1, A3, SETWISEO:17 ; hence Det A = 1. K ; ::_thesis: verum end; theorem :: MATRIXR2:42 for A being Matrix of 0 , REAL holds Det A = 1 proof let A be Matrix of 0 , REAL ; ::_thesis: Det A = 1 thus Det A = 1. F_Real by Th41 .= 1 ; ::_thesis: verum end; theorem Th43: :: MATRIXR2:43 for K being Field for n being Nat for A being Matrix of n,K holds Det A = Det (A @) proof let K be Field; ::_thesis: for n being Nat for A being Matrix of n,K holds Det A = Det (A @) let n be Nat; ::_thesis: for A being Matrix of n,K holds Det A = Det (A @) let A be Matrix of n,K; ::_thesis: Det A = Det (A @) ( n = 0 or ( n >= 1 & n is Element of NAT ) ) by NAT_1:14, ORDINAL1:def_12; then ( ( Det A = 1_ K & Det (A @) = 1_ K ) or Det A = Det (A @) ) by Th41, MATRIX_7:37; hence Det A = Det (A @) ; ::_thesis: verum end; theorem :: MATRIXR2:44 for n being Element of NAT for A being Matrix of n, REAL holds Det A = Det (A @) proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL holds Det A = Det (A @) let A be Matrix of n, REAL ; ::_thesis: Det A = Det (A @) reconsider N1 = MXR2MXF A, N2 = MXR2MXF (A @) as Matrix of n,F_Real ; reconsider N3 = MXF2MXR (N1 @) as Matrix of n, REAL ; reconsider N4 = MXR2MXF N3 as Matrix of n,F_Real ; thus Det A = Det (A @) by Th43; ::_thesis: verum end; theorem Th45: :: MATRIXR2:45 for n being Element of NAT for K being Field for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B) proof let n be Element of NAT ; ::_thesis: for K being Field for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B) let K be Field; ::_thesis: for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B) let A, B be Matrix of n,K; ::_thesis: Det (A * B) = (Det A) * (Det B) percases ( n > 0 or n <= 0 ) ; suppose n > 0 ; ::_thesis: Det (A * B) = (Det A) * (Det B) hence Det (A * B) = (Det A) * (Det B) by MATRIX11:62; ::_thesis: verum end; suppose n <= 0 ; ::_thesis: Det (A * B) = (Det A) * (Det B) then A1: n = 0 ; hence Det (A * B) = 1. K by Th41 .= (1. K) * (1. K) by VECTSP_1:def_6 .= (Det A) * (1. K) by A1, Th41 .= (Det A) * (Det B) by A1, Th41 ; ::_thesis: verum end; end; end; theorem Th46: :: MATRIXR2:46 for n being Element of NAT for A, B being Matrix of n, REAL holds Det (A * B) = (Det A) * (Det B) proof let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL holds Det (A * B) = (Det A) * (Det B) set K = F_Real ; let A, B be Matrix of n, REAL ; ::_thesis: Det (A * B) = (Det A) * (Det B) reconsider Na = MXR2MXF A, Nb = MXR2MXF B as Matrix of n,F_Real ; Det (A * B) = (Det Na) * (Det Nb) by Th45 .= (Det A) * (Det B) ; hence Det (A * B) = (Det A) * (Det B) ; ::_thesis: verum end; begin theorem :: MATRIXR2:47 for x, y being FinSequence of REAL for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds (x - y) * A = (x * A) - (y * A) proof let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds (x - y) * A = (x * A) - (y * A) let A be Matrix of REAL; ::_thesis: ( len x = len A & len y = len x & len x > 0 implies (x - y) * A = (x * A) - (y * A) ) assume that A1: len x = len A and A2: len y = len x and A3: len x > 0 ; ::_thesis: (x - y) * A = (x * A) - (y * A) A4: width (LineVec2Mx y) = len y by MATRIXR1:def_10; A5: width (LineVec2Mx x) = len x by MATRIXR1:def_10; then A6: width ((LineVec2Mx x) * A) = width A by A1, MATRIX_3:def_4 .= width ((LineVec2Mx y) * A) by A1, A2, A4, MATRIX_3:def_4 ; A7: len (LineVec2Mx y) = 1 by MATRIXR1:def_10; A8: len (LineVec2Mx x) = 1 by MATRIXR1:def_10; then A9: 1 <= len ((LineVec2Mx x) * A) by A1, A5, MATRIX_3:def_4; A10: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A5, MATRIX_3:def_4 .= len (LineVec2Mx y) by A7, MATRIXR1:def_10 .= len ((LineVec2Mx y) * A) by A1, A2, A4, MATRIX_3:def_4 ; thus (x - y) * A = Line ((((LineVec2Mx x) - (LineVec2Mx y)) * A),1) by A2, Th23 .= Line ((((LineVec2Mx x) * A) - ((LineVec2Mx y) * A)),1) by A1, A2, A3, A5, A4, A8, A7, Th16 .= (x * A) - (y * A) by A6, A10, A9, Th25 ; ::_thesis: verum end; theorem :: MATRIXR2:48 for x, y being FinSequence of REAL for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds A * (x - y) = (A * x) - (A * y) proof let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds A * (x - y) = (A * x) - (A * y) let A be Matrix of REAL; ::_thesis: ( len x = width A & len y = len x & len x > 0 & len A > 0 implies A * (x - y) = (A * x) - (A * y) ) assume that A1: len x = width A and A2: len y = len x and A3: len x > 0 and A4: len A > 0 ; ::_thesis: A * (x - y) = (A * x) - (A * y) A5: len (ColVec2Mx y) = len y by A2, A3, MATRIXR1:def_9; A6: width (ColVec2Mx y) = 1 by A2, A3, MATRIXR1:def_9; A7: len (ColVec2Mx x) = len x by A3, MATRIXR1:def_9; then A8: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def_4 .= len (A * (ColVec2Mx y)) by A1, A2, A5, MATRIX_3:def_4 ; A9: width (ColVec2Mx x) = 1 by A3, MATRIXR1:def_9; then A10: 1 <= width (A * (ColVec2Mx x)) by A1, A7, MATRIX_3:def_4; A11: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A7, MATRIX_3:def_4 .= width (ColVec2Mx y) by A3, A6, MATRIXR1:def_9 .= width (A * (ColVec2Mx y)) by A1, A2, A5, MATRIX_3:def_4 ; thus A * (x - y) = Col ((A * ((ColVec2Mx x) - (ColVec2Mx y))),1) by A2, A3, Th24 .= Col (((A * (ColVec2Mx x)) - (A * (ColVec2Mx y))),1) by A1, A2, A3, A4, A7, A5, A9, A6, Th20 .= (A * x) - (A * y) by A8, A11, A10, Th26 ; ::_thesis: verum end; theorem :: MATRIXR2:49 for x being FinSequence of REAL for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds (- x) * A = - (x * A) proof 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 (- x) * A = - (x * A) let A be Matrix of REAL; ::_thesis: ( len A = len x & len x > 0 & width A > 0 implies (- x) * A = - (x * A) ) assume that A1: len A = len x and A2: len x > 0 and A3: width A > 0 ; ::_thesis: (- x) * A = - (x * A) A4: (A @) * x = x * A by A1, A2, A3, MATRIXR1:52; A5: width (A @) = len x by A1, A3, MATRIX_2:10; then A6: (A @) * (- x) = (- 1) * ((A @) * x) by A2, MATRIXR1:59; A7: len (- x) = len x by RVSUM_1:114; len (A @) > 0 by A3, MATRIX_2:10; then (- x) * ((A @) @) = (A @) * (- x) by A2, A5, A7, MATRIXR1:53; hence (- x) * A = - (x * A) by A1, A2, A3, A6, A4, MATRIX_2:13; ::_thesis: verum end; theorem :: MATRIXR2:50 for x being FinSequence of REAL for A being Matrix of REAL st len x = width A & len x > 0 holds A * (- x) = - (A * x) proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = width A & len x > 0 holds A * (- x) = - (A * x) let A be Matrix of REAL; ::_thesis: ( len x = width A & len x > 0 implies A * (- x) = - (A * x) ) assume that A1: len x = width A and A2: len x > 0 ; ::_thesis: A * (- x) = - (A * x) A3: len (ColVec2Mx x) = len x by A2, MATRIXR1:def_9; width (ColVec2Mx x) = 1 by A2, MATRIXR1:def_9; then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A3, MATRIX_3:def_4; thus A * (- x) = Col ((A * ((- 1) * (ColVec2Mx x))),1) by A2, MATRIXR1:47 .= Col (((- 1) * (A * (ColVec2Mx x))),1) by A1, A3, MATRIXR1:40 .= - (A * x) by A4, MATRIXR1:56 ; ::_thesis: verum end; theorem :: MATRIXR2:51 for x being FinSequence of REAL for A being Matrix of REAL st len x = len A & len x > 0 holds x * (- A) = - (x * A) proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = len A & len x > 0 holds x * (- A) = - (x * A) let A be Matrix of REAL; ::_thesis: ( len x = len A & len x > 0 implies x * (- A) = - (x * A) ) assume that A1: len x = len A and A2: len x > 0 ; ::_thesis: x * (- A) = - (x * A) A3: width A = len (x * A) by A1, MATRIXR1:62; A4: ( len A = len (- A) & width A = width (- A) ) by MATRIX_3:def_2; then A5: len (x * (- A)) = width A by A1, MATRIXR1:62; (x * (- A)) + (x * A) = x * ((- A) + A) by A1, A2, A4, MATRIXR1:64 .= x * (0_Rmatrix ((len A),(width A))) by Th31 .= 0* (width A) by A1, A2, MATRIXR1:66 ; hence x * (- A) = - (x * A) by A5, A3, Th1; ::_thesis: verum end; theorem :: MATRIXR2:52 for x being FinSequence of REAL for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds (- A) * x = - (A * x) proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds (- A) * x = - (A * x) let A be Matrix of REAL; ::_thesis: ( len x = width A & len A > 0 & len x > 0 implies (- A) * x = - (A * x) ) assume that A1: len x = width A and A2: len A > 0 and A3: len x > 0 ; ::_thesis: (- A) * x = - (A * x) A4: ( len (ColVec2Mx x) = len x & width (ColVec2Mx x) = 1 ) by A3, MATRIXR1:def_9; then A5: 1 <= width (A * (ColVec2Mx x)) by A1, MATRIX_3:def_4; thus (- A) * x = Col ((((- 1) * A) * (ColVec2Mx x)),1) by Th9 .= Col (((- 1) * (A * (ColVec2Mx x))),1) by A1, A2, A3, A4, MATRIXR1:41 .= - (A * x) by A5, MATRIXR1:56 ; ::_thesis: verum end; theorem :: MATRIXR2:53 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, MATRIXR1:def_9; width (ColVec2Mx x) = 1 by A2, MATRIXR1:def_9; 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, MATRIXR1:47 .= Col ((a * (A * (ColVec2Mx x))),1) by A1, A3, MATRIXR1:40 .= a * (A * x) by A4, MATRIXR1:56 ; ::_thesis: verum end; theorem :: MATRIXR2:54 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 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 x = len A & len A = len B & width A = width B & len A > 0 holds x * (A - B) = (x * A) - (x * B) let A, B be Matrix of REAL; ::_thesis: ( len x = len A & len A = len B & width A = width B & len A > 0 implies x * (A - B) = (x * A) - (x * B) ) assume that A1: len x = len A and A2: len A = len B and A3: width A = width B and A4: len A > 0 ; ::_thesis: x * (A - B) = (x * A) - (x * B) A5: width (LineVec2Mx x) = len x by MATRIXR1:def_10; then A6: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, MATRIX_3:def_4 .= 1 by MATRIXR1:def_10 ; A7: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A5, MATRIX_3:def_4 .= len ((LineVec2Mx x) * B) by A1, A2, A5, MATRIX_3:def_4 ; A8: width ((LineVec2Mx x) * A) = width A by A1, A5, MATRIX_3:def_4 .= width ((LineVec2Mx x) * B) by A1, A2, A3, A5, MATRIX_3:def_4 ; len (LineVec2Mx x) = 1 by MATRIXR1:def_10; hence x * (A - B) = Line ((((LineVec2Mx x) * A) - ((LineVec2Mx x) * B)),1) by A1, A2, A3, A4, A5, Th20 .= (x * A) - (x * B) by A8, A7, A6, Th25 ; ::_thesis: verum end; theorem :: MATRIXR2:55 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 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 x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds (A - B) * x = (A * x) - (B * x) let A, B be Matrix of REAL; ::_thesis: ( len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 implies (A - B) * x = (A * x) - (B * x) ) assume that A1: len x = width A and A2: len A = len B and A3: width A = width B and A4: len x > 0 and A5: len A > 0 ; ::_thesis: (A - B) * x = (A * x) - (B * x) A6: len (ColVec2Mx x) = len x by A4, MATRIXR1:def_9; then A7: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def_4 .= len (B * (ColVec2Mx x)) by A1, A2, A3, A6, MATRIX_3:def_4 ; A8: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A6, MATRIX_3:def_4 .= 1 by A4, MATRIXR1:45 ; A9: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A6, MATRIX_3:def_4 .= width (B * (ColVec2Mx x)) by A1, A3, A6, MATRIX_3:def_4 ; thus (A - B) * x = Col (((A * (ColVec2Mx x)) - (B * (ColVec2Mx x))),1) by A1, A2, A3, A4, A5, A6, Th16 .= (A * x) - (B * x) by A7, A9, A8, Th26 ; ::_thesis: verum end; theorem Th56: :: MATRIXR2:56 for x being FinSequence of REAL for A being Matrix of REAL st len A = len x holds (LineVec2Mx x) * A = LineVec2Mx (x * A) proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x holds (LineVec2Mx x) * A = LineVec2Mx (x * A) let A be Matrix of REAL; ::_thesis: ( len A = len x implies (LineVec2Mx x) * A = LineVec2Mx (x * A) ) A1: len (LineVec2Mx (x * A)) = 1 by MATRIXR1:def_10; assume A2: len A = len x ; ::_thesis: (LineVec2Mx x) * A = LineVec2Mx (x * A) then A3: width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A) by MATRIXR1:def_10; width (LineVec2Mx (x * A)) = len (x * A) by MATRIXR1:def_10; then A4: width (LineVec2Mx (x * A)) = width A by A2, MATRIXR1:62; A5: len (x * A) = width A by A2, MATRIXR1:62; then A6: width (MXR2MXF (LineVec2Mx (x * A))) = width (MXR2MXF A) by MATRIXR1:def_10; A7: width (LineVec2Mx x) = len x by MATRIXR1:def_10; A8: for i, j being Nat st [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) holds (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) proof len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = len (MXR2MXF (LineVec2Mx x)) by A3, MATRIX_3:def_4; then len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = 1 by MATRIXR1:def_10; then A9: 1 in Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) ; let i, j be Nat; ::_thesis: ( [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) implies (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) ) A10: width ((LineVec2Mx x) * A) = width A by A2, A7, MATRIX_3:def_4; assume A11: [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) ; ::_thesis: (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) then A12: j in Seg (width A) by A4, ZFMISC_1:87; then j in dom (x * A) by A5, FINSEQ_1:def_3; then A13: (Line (((LineVec2Mx x) * A),1)) . j = (LineVec2Mx (x * A)) * (1,j) by MATRIXR1:def_10; Indices (LineVec2Mx (x * A)) = [:(Seg 1),(Seg (width A)):] by A1, A4, FINSEQ_1:def_3; then i in Seg 1 by A11, ZFMISC_1:87; then ( 1 <= i & i <= 1 ) by FINSEQ_1:1; then A14: i = 1 by XXREAL_0:1; width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = width A by A3, MATRIX_3:def_4; then [1,j] in [:(Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))),(Seg (width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))):] by A12, A9, ZFMISC_1:87; then A15: [1,j] in Indices ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) by FINSEQ_1:def_3; width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A) by A2, MATRIXR1:def_10; then ((LineVec2Mx x) * A) * (1,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) by A14, A15, MATRIX_3:def_4; hence (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) by A12, A14, A13, A10, MATRIX_1:def_7; ::_thesis: verum end; len (MXR2MXF (LineVec2Mx (x * A))) = len (MXR2MXF (LineVec2Mx x)) by A1, MATRIXR1:def_10; hence (LineVec2Mx x) * A = LineVec2Mx (x * A) by A6, A3, A8, MATRIX_3:def_4; ::_thesis: verum end; theorem Th57: :: MATRIXR2:57 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = len A & width A = len B holds x * (A * B) = (x * A) * B proof let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len x = len A & width A = len B holds x * (A * B) = (x * A) * B let A, B be Matrix of REAL; ::_thesis: ( len x = len A & width A = len B implies x * (A * B) = (x * A) * B ) assume that A1: len x = len A and A2: width A = len B ; ::_thesis: x * (A * B) = (x * A) * B width (LineVec2Mx x) = len x by MATRIXR1:def_10; hence x * (A * B) = Line ((((LineVec2Mx x) * A) * B),1) by A1, A2, MATRIX_3:33 .= (x * A) * B by A1, Th56 ; ::_thesis: verum end; theorem Th58: :: MATRIXR2:58 for x being FinSequence of REAL for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds A * (ColVec2Mx x) = ColVec2Mx (A * x) proof let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds A * (ColVec2Mx x) = ColVec2Mx (A * x) let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 & len A > 0 implies A * (ColVec2Mx x) = ColVec2Mx (A * x) ) assume that A1: width A = len x and A2: len x > 0 and A3: len A > 0 ; ::_thesis: A * (ColVec2Mx x) = ColVec2Mx (A * x) A4: len (ColVec2Mx x) = len x by A2, MATRIXR1:def_9; A5: len (MXR2MXF (ColVec2Mx x)) = width (MXR2MXF A) by A1, A2, MATRIXR1:def_9; then A6: width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = width (ColVec2Mx x) by MATRIX_3:def_4 .= 1 by A2, MATRIXR1:def_9 ; A7: len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = len A by A5, MATRIX_3:def_4; A8: len (A * x) = len A by A1, A2, MATRIXR1:61; then A9: width (ColVec2Mx (A * x)) = 1 by A3, MATRIXR1:def_9; A10: len (ColVec2Mx (A * x)) = len A by A3, A8, MATRIXR1:def_9; A11: len (ColVec2Mx (A * x)) = len (A * x) by A3, A8, MATRIXR1:def_9; A12: for i, j being Nat st [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) holds (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) implies (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) ) A13: ( 1 in Seg 1 & Indices (ColVec2Mx (A * x)) = [:(Seg (len (ColVec2Mx (A * x)))),(Seg 1):] ) by A9, FINSEQ_1:def_3; assume A14: [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) ; ::_thesis: (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) then A15: j in Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A9, A6, ZFMISC_1:87; A16: Indices (ColVec2Mx (A * x)) = [:(Seg (len A)),(Seg 1):] by A8, A11, A9, FINSEQ_1:def_3; then A17: i in Seg (len A) by A14, ZFMISC_1:87; then A18: i in dom (A * x) by A8, FINSEQ_1:def_3; i in Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A7, A14, A16, ZFMISC_1:87; then [i,j] in [:(Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))),(Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))):] by A15, ZFMISC_1:87; then A19: [i,j] in Indices ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:def_3; j in Seg 1 by A9, A14, ZFMISC_1:87; then ( 1 <= j & j <= 1 ) by FINSEQ_1:1; then A20: j = 1 by XXREAL_0:1; i in Seg (len (ColVec2Mx (A * x))) by A10, A14, A16, ZFMISC_1:87; then [i,1] in Indices (ColVec2Mx (A * x)) by A13, ZFMISC_1:87; then A21: ex p2 being FinSequence of REAL st ( p2 = (ColVec2Mx (A * x)) . i & (ColVec2Mx (A * x)) * (i,1) = p2 . 1 ) by MATRIX_1:def_5; A22: (Col ((A * (ColVec2Mx x)),1)) . i = <*((A * x) . i)*> . 1 by FINSEQ_1:40 .= (ColVec2Mx (A * x)) * (i,1) by A3, A8, A18, A21, MATRIXR1:def_9 ; len (A * (ColVec2Mx x)) = len A by A1, A4, MATRIX_3:def_4; then i in dom (A * (ColVec2Mx x)) by A17, FINSEQ_1:def_3; then (Col ((A * (ColVec2Mx x)),1)) . i = (A * (ColVec2Mx x)) * (i,j) by A20, MATRIX_1:def_8; hence (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) by A5, A20, A22, A19, MATRIX_3:def_4; ::_thesis: verum end; A23: len (MXR2MXF (ColVec2Mx (A * x))) = len (MXR2MXF A) by A3, A8, MATRIXR1:def_9; width (MXR2MXF (ColVec2Mx (A * x))) = 1 by A3, A8, MATRIXR1:def_9 .= width (MXR2MXF (ColVec2Mx x)) by A2, MATRIXR1:def_9 ; hence A * (ColVec2Mx x) = ColVec2Mx (A * x) by A23, A5, A12, MATRIX_3:def_4; ::_thesis: verum end; theorem Th59: :: MATRIXR2:59 for x being FinSequence of REAL for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds (A * B) * x = A * (B * x) proof let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds (A * B) * x = A * (B * x) let A, B be Matrix of REAL; ::_thesis: ( len x = width B & width A = len B & len x > 0 & len B > 0 implies (A * B) * x = A * (B * x) ) assume that A1: len x = width B and A2: width A = len B and A3: len x > 0 and A4: len B > 0 ; ::_thesis: (A * B) * x = A * (B * x) len (ColVec2Mx x) = len x by A3, MATRIXR1:def_9; hence (A * B) * x = Col ((A * (B * (ColVec2Mx x))),1) by A1, A2, MATRIX_3:33 .= A * (B * x) by A1, A3, A4, Th58 ; ::_thesis: verum end; theorem :: MATRIXR2:60 for n, m, k being Element of NAT for B being Matrix of n,m, REAL for A being Matrix of m,k, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j proof let n, m, k be Element of NAT ; ::_thesis: for B being Matrix of n,m, REAL for A being Matrix of m,k, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j let B be Matrix of n,m, REAL ; ::_thesis: for A being Matrix of m,k, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j let A be Matrix of m,k, REAL ; ::_thesis: ( n > 0 implies for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j ) assume A1: n > 0 ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j then A2: width B = m by MATRIX_1:23; let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (B * A) implies (B * A) * (i,j) = ((Line (B,i)) * A) . j ) A3: len A = m by MATRIX_1:def_2; then A4: len A = len (Line (B,i)) by A2, MATRIX_1:def_7; assume A5: [i,j] in Indices (B * A) ; ::_thesis: (B * A) * (i,j) = ((Line (B,i)) * A) . j then A6: j in Seg (width (B * A)) by ZFMISC_1:87; width B = len A by A1, A3, MATRIX_1:23; then A7: (B * A) * (i,j) = (Line (B,i)) "*" (Col (A,j)) by A5, MATRPROB:39; width A = width (B * A) by A3, A2, MATRPROB:39; then j in Seg (len ((Line (B,i)) * A)) by A6, A4, MATRIXR1:62; hence (B * A) * (i,j) = ((Line (B,i)) * A) . j by A7, A4, MATRPROB:40; ::_thesis: verum end; theorem Th61: :: MATRIXR2:61 for n being Element of NAT for A, B being Matrix of n, REAL for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j proof let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j let A, B be Matrix of n, REAL ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices (B * A) holds (B * A) * (i,j) = ((Line (B,i)) * A) . j let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (B * A) implies (B * A) * (i,j) = ((Line (B,i)) * A) . j ) assume A1: [i,j] in Indices (B * A) ; ::_thesis: (B * A) * (i,j) = ((Line (B,i)) * A) . j then A2: j in Seg (width (B * A)) by ZFMISC_1:87; A3: len A = n by MATRIX_1:def_2; then width B = len A by MATRIX_1:24; then A4: (B * A) * (i,j) = (Line (B,i)) "*" (Col (A,j)) by A1, MATRPROB:39; A5: width B = n by MATRIX_1:24; then A6: len A = len (Line (B,i)) by A3, MATRIX_1:def_7; width A = width (B * A) by A3, A5, MATRPROB:39; then j in Seg (len ((Line (B,i)) * A)) by A2, A6, MATRIXR1:62; hence (B * A) * (i,j) = ((Line (B,i)) * A) . j by A4, A6, MATRPROB:40; ::_thesis: verum end; theorem :: MATRIXR2:62 for n being Element of NAT for A, B being Matrix of n, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (A * B) holds (A * B) * (i,j) = (A * (Col (B,j))) . i proof let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL st n > 0 holds for i, j being Element of NAT st [i,j] in Indices (A * B) holds (A * B) * (i,j) = (A * (Col (B,j))) . i let A, B be Matrix of n, REAL ; ::_thesis: ( n > 0 implies for i, j being Element of NAT st [i,j] in Indices (A * B) holds (A * B) * (i,j) = (A * (Col (B,j))) . i ) assume A1: n > 0 ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices (A * B) holds (A * B) * (i,j) = (A * (Col (B,j))) . i let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (A * B) implies (A * B) * (i,j) = (A * (Col (B,j))) . i ) A2: width A = n by MATRIX_1:24; assume A3: [i,j] in Indices (A * B) ; ::_thesis: (A * B) * (i,j) = (A * (Col (B,j))) . i then i in dom (A * B) by ZFMISC_1:87; then A4: i in Seg (len (A * B)) by FINSEQ_1:def_3; A5: len B = n by MATRIX_1:def_2; then A6: width A = len (Col (B,j)) by A2, MATRIX_1:def_8; width A = len B by A5, MATRIX_1:24; then A7: (A * B) * (i,j) = (Line (A,i)) "*" (Col (B,j)) by A3, MATRPROB:39; ( len (A * B) = n & len A = n ) by MATRIX_1:24; then i in Seg (len (A * (Col (B,j)))) by A1, A4, A2, A6, MATRIXR1:61; hence (A * B) * (i,j) = (A * (Col (B,j))) . i by A1, A2, A7, A6, MATRPROB:41; ::_thesis: verum end; begin definition let n be Element of NAT ; func 1_Rmatrix n -> Matrix of n, REAL equals :: MATRIXR2:def 2 MXF2MXR (1. (F_Real,n)); correctness coherence MXF2MXR (1. (F_Real,n)) is Matrix of n, REAL ; ; end; :: deftheorem defines 1_Rmatrix MATRIXR2:def_2_:_ for n being Element of NAT holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n)); theorem Th63: :: MATRIXR2:63 for n being Element of NAT holds ( ( for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds (1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n) * (i,j) = 0 ) ) proof let n be Element of NAT ; ::_thesis: ( ( for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds (1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n) * (i,j) = 0 ) ) set K = F_Real ; thus for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds (1_Rmatrix n) * (i,i) = 1 ::_thesis: for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n) * (i,j) = 0 proof let i be Element of NAT ; ::_thesis: ( [i,i] in Indices (1_Rmatrix n) implies (1_Rmatrix n) * (i,i) = 1 ) assume [i,i] in Indices (1_Rmatrix n) ; ::_thesis: (1_Rmatrix n) * (i,i) = 1 hence (1_Rmatrix n) * (i,i) = 1_ F_Real by MATRIX_1:def_11 .= 1 ; ::_thesis: verum end; let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (1_Rmatrix n) & i <> j implies (1_Rmatrix n) * (i,j) = 0 ) assume ( [i,j] in Indices (1_Rmatrix n) & i <> j ) ; ::_thesis: (1_Rmatrix n) * (i,j) = 0 hence (1_Rmatrix n) * (i,j) = 0. F_Real by MATRIX_1:def_11 .= 0 ; ::_thesis: verum end; theorem Th64: :: MATRIXR2:64 for n being Element of NAT holds (1_Rmatrix n) @ = 1_Rmatrix n proof let n be Element of NAT ; ::_thesis: (1_Rmatrix n) @ = 1_Rmatrix n percases ( n > 0 or n = 0 ) ; supposeA1: n > 0 ; ::_thesis: (1_Rmatrix n) @ = 1_Rmatrix n A2: len (1_Rmatrix n) = n by MATRIX_1:24; A3: Indices (1_Rmatrix n) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: for i, j being Nat st [i,j] in Indices (1_Rmatrix n) holds (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (1_Rmatrix n) implies (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) ) reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12; assume A5: [i,j] in Indices (1_Rmatrix n) ; ::_thesis: (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) then ( i in Seg n & j in Seg n ) by A3, ZFMISC_1:87; then A6: [j,i] in Indices (1_Rmatrix n) by A3, ZFMISC_1:87; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) hence (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) by A5, MATRIX_1:def_6; ::_thesis: verum end; suppose i <> j ; ::_thesis: (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) then ( (1_Rmatrix n) * (i0,j0) = 0 & (1_Rmatrix n) * (j0,i0) = 0 ) by A5, A6, Th63; hence (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) by A6, MATRIX_1:def_6; ::_thesis: verum end; end; end; A7: width (1_Rmatrix n) = n by MATRIX_1:24; then ( len ((1_Rmatrix n) @) = width (1_Rmatrix n) & width ((1_Rmatrix n) @) = len (1_Rmatrix n) ) by A1, MATRIX_2:10; hence (1_Rmatrix n) @ = 1_Rmatrix n by A7, A2, A4, MATRIX_1:21; ::_thesis: verum end; suppose n = 0 ; ::_thesis: (1_Rmatrix n) @ = 1_Rmatrix n hence (1_Rmatrix n) @ = 1_Rmatrix n by MATRIX_1:35; ::_thesis: verum end; end; end; theorem Th65: :: MATRIXR2:65 for n, m being Element of NAT st n > 0 holds (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) proof let n, m be Element of NAT ; ::_thesis: ( n > 0 implies (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) ) assume A1: n > 0 ; ::_thesis: (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) then ( width (0_Rmatrix (n,m)) = m & len (0_Rmatrix (n,m)) = n ) by MATRIX_1:23; then (0 + 0) * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) by A1, MATRIXR1:44; hence (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) by Th12; ::_thesis: verum end; theorem :: MATRIXR2:66 for n, m being Element of NAT for a being Real st n > 0 holds a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) proof let n, m be Element of NAT ; ::_thesis: for a being Real st n > 0 holds a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) let a be Real; ::_thesis: ( n > 0 implies a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) ) A1: ( len (a * (0_Rmatrix (n,m))) = len (0_Rmatrix (n,m)) & width (a * (0_Rmatrix (n,m))) = width (0_Rmatrix (n,m)) ) by MATRIXR1:27; assume A2: n > 0 ; ::_thesis: a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) then A3: ( width (0_Rmatrix (n,m)) = m & len (0_Rmatrix (n,m)) = n ) by MATRIX_1:23; a * (0_Rmatrix (n,m)) = a * ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) by A2, Th65 .= (a * (0_Rmatrix (n,m))) + (a * (0_Rmatrix (n,m))) by A3, MATRIXR1:43 ; hence a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) by A3, A1, MATRIXR1:37; ::_thesis: verum end; theorem Th67: :: MATRIXR2:67 for K being Field for A being Matrix of K holds A * (1. (K,(width A))) = A proof let K be Field; ::_thesis: for A being Matrix of K holds A * (1. (K,(width A))) = A let A be Matrix of K; ::_thesis: A * (1. (K,(width A))) = A set n = width A; set B = 1. (K,(width A)); A1: width (1. (K,(width A))) = width A by MATRIX_1:24; A2: len (1. (K,(width A))) = width A by MATRIX_1:24; then A3: width (A * (1. (K,(width A)))) = width (1. (K,(width A))) by MATRIX_3:def_4; A4: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_*_(1._(K,(width_A))))_holds_ (A_*_(1._(K,(width_A))))_*_(i,j)_=_A_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices (A * (1. (K,(width A)))) implies (A * (1. (K,(width A)))) * (i,j) = A * (i,j) ) assume A5: [i,j] in Indices (A * (1. (K,(width A)))) ; ::_thesis: (A * (1. (K,(width A)))) * (i,j) = A * (i,j) then A6: j in Seg (width (1. (K,(width A)))) by A3, ZFMISC_1:87; then j in Seg (len (Line (A,i))) by A1, MATRIX_1:def_7; then A7: j in dom (Line (A,i)) by FINSEQ_1:def_3; A8: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Col_((1._(K,(width_A))),j))_&_k_<>_j_holds_ (Col_((1._(K,(width_A))),j))_._k_=_0._K let k be Nat; ::_thesis: ( k in dom (Col ((1. (K,(width A))),j)) & k <> j implies (Col ((1. (K,(width A))),j)) . k = 0. K ) assume that A9: k in dom (Col ((1. (K,(width A))),j)) and A10: k <> j ; ::_thesis: (Col ((1. (K,(width A))),j)) . k = 0. K k in Seg (len (Col ((1. (K,(width A))),j))) by A9, FINSEQ_1:def_3; then k in Seg (len (1. (K,(width A)))) by MATRIX_1:def_8; then k in dom (1. (K,(width A))) by FINSEQ_1:def_3; then [k,j] in Indices (1. (K,(width A))) by A6, ZFMISC_1:87; hence (Col ((1. (K,(width A))),j)) . k = 0. K by A10, MATRIX_3:16; ::_thesis: verum end; A11: j in Seg (width A) by A1, A3, A5, ZFMISC_1:87; then j in dom (1. (K,(width A))) by A2, FINSEQ_1:def_3; then [j,j] in Indices (1. (K,(width A))) by A1, A11, ZFMISC_1:87; then A12: (Col ((1. (K,(width A))),j)) . j = 1_ K by MATRIX_3:16; j in Seg (len (Col ((1. (K,(width A))),j))) by A2, A1, A6, MATRIX_1:def_8; then A13: j in dom (Col ((1. (K,(width A))),j)) by FINSEQ_1:def_3; thus (A * (1. (K,(width A)))) * (i,j) = (Line (A,i)) "*" (Col ((1. (K,(width A))),j)) by A2, A5, MATRIX_3:def_4 .= (Col ((1. (K,(width A))),j)) "*" (Line (A,i)) by FVSUM_1:90 .= Sum (mlt ((Col ((1. (K,(width A))),j)),(Line (A,i)))) by FVSUM_1:def_9 .= (Line (A,i)) . j by A13, A7, A8, A12, MATRIX_3:17 .= A * (i,j) by A11, MATRIX_1:def_7 ; ::_thesis: verum end; len (A * (1. (K,(width A)))) = len A by A2, MATRIX_3:def_4; hence A * (1. (K,(width A))) = A by A1, A3, A4, MATRIX_1:21; ::_thesis: verum end; theorem Th68: :: MATRIXR2:68 for K being Field for A being Matrix of K holds (1. (K,(len A))) * A = A proof let K be Field; ::_thesis: for A being Matrix of K holds (1. (K,(len A))) * A = A let A be Matrix of K; ::_thesis: (1. (K,(len A))) * A = A set n = len A; set B = 1. (K,(len A)); A1: len (1. (K,(len A))) = len A by MATRIX_1:24; A2: width (1. (K,(len A))) = len A by MATRIX_1:24; then A3: len ((1. (K,(len A))) * A) = len (1. (K,(len A))) by MATRIX_3:def_4; A4: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((1._(K,(len_A)))_*_A)_holds_ ((1._(K,(len_A)))_*_A)_*_(i,j)_=_A_*_(i,j) A5: dom A = Seg (len A) by FINSEQ_1:def_3; let i, j be Nat; ::_thesis: ( [i,j] in Indices ((1. (K,(len A))) * A) implies ((1. (K,(len A))) * A) * (i,j) = A * (i,j) ) assume A6: [i,j] in Indices ((1. (K,(len A))) * A) ; ::_thesis: ((1. (K,(len A))) * A) * (i,j) = A * (i,j) A7: dom ((1. (K,(len A))) * A) = Seg (len ((1. (K,(len A))) * A)) by FINSEQ_1:def_3; then A8: i in Seg (width (1. (K,(len A)))) by A1, A2, A3, A6, ZFMISC_1:87; then i in Seg (len (Line ((1. (K,(len A))),i))) by MATRIX_1:def_7; then A9: i in dom (Line ((1. (K,(len A))),i)) by FINSEQ_1:def_3; A10: dom (1. (K,(len A))) = Seg (len (1. (K,(len A)))) by FINSEQ_1:def_3; then A11: i in dom (1. (K,(len A))) by A3, A6, A7, ZFMISC_1:87; then [i,i] in Indices (1. (K,(len A))) by A8, ZFMISC_1:87; then A12: (Line ((1. (K,(len A))),i)) . i = 1_ K by MATRIX_3:15; i in Seg (len (Col (A,j))) by A2, A8, MATRIX_1:def_8; then A13: i in dom (Col (A,j)) by FINSEQ_1:def_3; A14: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Line_((1._(K,(len_A))),i))_&_k_<>_i_holds_ (Line_((1._(K,(len_A))),i))_._k_=_0._K let k be Nat; ::_thesis: ( k in dom (Line ((1. (K,(len A))),i)) & k <> i implies (Line ((1. (K,(len A))),i)) . k = 0. K ) assume that A15: k in dom (Line ((1. (K,(len A))),i)) and A16: k <> i ; ::_thesis: (Line ((1. (K,(len A))),i)) . k = 0. K k in Seg (len (Line ((1. (K,(len A))),i))) by A15, FINSEQ_1:def_3; then k in Seg (width (1. (K,(len A)))) by MATRIX_1:def_7; then [i,k] in Indices (1. (K,(len A))) by A11, ZFMISC_1:87; hence (Line ((1. (K,(len A))),i)) . k = 0. K by A16, MATRIX_3:15; ::_thesis: verum end; thus ((1. (K,(len A))) * A) * (i,j) = (Line ((1. (K,(len A))),i)) "*" (Col (A,j)) by A2, A6, MATRIX_3:def_4 .= Sum (mlt ((Line ((1. (K,(len A))),i)),(Col (A,j)))) by FVSUM_1:def_9 .= (Col (A,j)) . i by A9, A13, A14, A12, MATRIX_3:17 .= A * (i,j) by A1, A5, A10, A11, MATRIX_1:def_8 ; ::_thesis: verum end; width ((1. (K,(len A))) * A) = width A by A2, MATRIX_3:def_4; hence (1. (K,(len A))) * A = A by A1, A3, A4, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIXR2:69 for n, m being Element of NAT for A being Matrix of REAL holds ( ( n = width A implies A * (1_Rmatrix n) = A ) & ( m = len A implies (1_Rmatrix m) * A = A ) ) by Th67, Th68; theorem Th70: :: MATRIXR2:70 for n being Element of NAT for A being Matrix of n, REAL holds (1_Rmatrix n) * A = A proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL holds (1_Rmatrix n) * A = A let A be Matrix of n, REAL ; ::_thesis: (1_Rmatrix n) * A = A n = len A by MATRIX_1:def_2; hence (1_Rmatrix n) * A = A by Th68; ::_thesis: verum end; theorem Th71: :: MATRIXR2:71 for n being Element of NAT for A being Matrix of n, REAL holds A * (1_Rmatrix n) = A proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL holds A * (1_Rmatrix n) = A let A be Matrix of n, REAL ; ::_thesis: A * (1_Rmatrix n) = A A1: n = len A by MATRIX_1:def_2; now__::_thesis:_(_(_n_<>_0_&_n_=_width_A_)_or_(_n_=_0_&_n_=_width_A_)_) percases ( n <> 0 or n = 0 ) ; case n <> 0 ; ::_thesis: n = width A hence n = width A by A1, MATRIX_1:20; ::_thesis: verum end; case n = 0 ; ::_thesis: n = width A hence n = width A by A1, MATRIX_1:def_3; ::_thesis: verum end; end; end; hence A * (1_Rmatrix n) = A by Th67; ::_thesis: verum end; theorem Th72: :: MATRIXR2:72 for n being Element of NAT holds Det (1_Rmatrix n) = 1 proof let n be Element of NAT ; ::_thesis: Det (1_Rmatrix n) = 1 percases ( n >= 1 or n < 1 ) ; suppose n >= 1 ; ::_thesis: Det (1_Rmatrix n) = 1 hence Det (1_Rmatrix n) = 1_ F_Real by MATRIX_7:16 .= 1 ; ::_thesis: verum end; suppose n < 1 ; ::_thesis: Det (1_Rmatrix n) = 1 then n = 0 by NAT_1:25; hence Det (1_Rmatrix n) = 1. F_Real by Th41 .= 1 ; ::_thesis: verum end; end; end; definition let n be Element of NAT ; func 0_Rmatrix n -> Matrix of n, REAL equals :: MATRIXR2:def 3 0_Rmatrix (n,n); correctness coherence 0_Rmatrix (n,n) is Matrix of n, REAL ; ; end; :: deftheorem defines 0_Rmatrix MATRIXR2:def_3_:_ for n being Element of NAT holds 0_Rmatrix n = 0_Rmatrix (n,n); theorem :: MATRIXR2:73 for n being Element of NAT st n > 0 holds Det (0_Rmatrix n) = 0 proof let n be Element of NAT ; ::_thesis: ( n > 0 implies Det (0_Rmatrix n) = 0 ) set K = F_Real ; assume n > 0 ; ::_thesis: Det (0_Rmatrix n) = 0 then n >= 0 + 1 by NAT_1:13; then Det (0_Rmatrix n) = 0. F_Real by MATRIX_7:15 .= 0 ; hence Det (0_Rmatrix n) = 0 ; ::_thesis: verum end; definition let n, i be Nat; func Base_FinSeq (n,i) -> FinSequence of REAL equals :: MATRIXR2:def 4 (n |-> 0) +* (i,1); coherence (n |-> 0) +* (i,1) is FinSequence of REAL proof reconsider n = n as Element of NAT by ORDINAL1:def_12; (n |-> 0) +* (i,1) = Replace ((n |-> 0),i,1) ; hence (n |-> 0) +* (i,1) is FinSequence of REAL ; ::_thesis: verum end; end; :: deftheorem defines Base_FinSeq MATRIXR2:def_4_:_ for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1); theorem Th74: :: MATRIXR2:74 for n, i being Nat holds len (Base_FinSeq (n,i)) = n proof let n, i be Nat; ::_thesis: len (Base_FinSeq (n,i)) = n len ((n |-> 0) +* (i,1)) = len (n |-> 0) by FUNCT_7:97 .= n by CARD_1:def_7 ; hence len (Base_FinSeq (n,i)) = n ; ::_thesis: verum end; theorem Th75: :: MATRIXR2:75 for i, n being Nat st 1 <= i & i <= n holds (Base_FinSeq (n,i)) . i = 1 proof let i, n be Nat; ::_thesis: ( 1 <= i & i <= n implies (Base_FinSeq (n,i)) . i = 1 ) A1: len (n |-> 0) = n by CARD_1:def_7; assume ( 1 <= i & i <= n ) ; ::_thesis: (Base_FinSeq (n,i)) . i = 1 then i in dom (n |-> 0) by A1, FINSEQ_3:25; hence (Base_FinSeq (n,i)) . i = 1 by FUNCT_7:31; ::_thesis: verum end; theorem Th76: :: MATRIXR2:76 for j, n, i being Nat st 1 <= j & j <= n & i <> j holds (Base_FinSeq (n,i)) . j = 0 proof let j, n, i be Nat; ::_thesis: ( 1 <= j & j <= n & i <> j implies (Base_FinSeq (n,i)) . j = 0 ) assume that A1: ( 1 <= j & j <= n ) and A2: i <> j ; ::_thesis: (Base_FinSeq (n,i)) . j = 0 A3: j in Seg n by A1, FINSEQ_1:1; thus (Base_FinSeq (n,i)) . j = (n |-> 0) . j by A2, FUNCT_7:32 .= 0 by A3, FINSEQ_2:57 ; ::_thesis: verum end; theorem :: MATRIXR2:77 ( Base_FinSeq (1,1) = <*1*> & Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> ) proof thus Base_FinSeq (1,1) = Replace (<*0*>,1,1) by FINSEQ_2:59 .= <*1*> by FINSEQ_7:12 ; ::_thesis: ( Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> ) thus Base_FinSeq (2,1) = Replace (<*0,0*>,1,1) by FINSEQ_2:61 .= <*1,0*> by FINSEQ_7:13 ; ::_thesis: ( Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> ) thus Base_FinSeq (2,2) = Replace (<*0,0*>,2,1) by FINSEQ_2:61 .= <*0,1*> by FINSEQ_7:14 ; ::_thesis: ( Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> ) thus Base_FinSeq (3,1) = Replace (<*0,0,0*>,1,1) by FINSEQ_2:62 .= <*1,0,0*> by FINSEQ_7:15 ; ::_thesis: ( Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> ) thus Base_FinSeq (3,2) = Replace (<*0,0,0*>,2,1) by FINSEQ_2:62 .= <*0,1,0*> by FINSEQ_7:16 ; ::_thesis: Base_FinSeq (3,3) = <*0,0,1*> thus Base_FinSeq (3,3) = Replace (<*0,0,0*>,3,1) by FINSEQ_2:62 .= <*0,0,1*> by FINSEQ_7:17 ; ::_thesis: verum end; theorem Th78: :: MATRIXR2:78 for i being Nat for n being Element of NAT st 1 <= i & i <= n holds (1_Rmatrix n) . i = Base_FinSeq (n,i) proof let i be Nat; ::_thesis: for n being Element of NAT st 1 <= i & i <= n holds (1_Rmatrix n) . i = Base_FinSeq (n,i) let n be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies (1_Rmatrix n) . i = Base_FinSeq (n,i) ) assume A1: ( 1 <= i & i <= n ) ; ::_thesis: (1_Rmatrix n) . i = Base_FinSeq (n,i) then 1 <= n by XXREAL_0:2; then A2: 1 in Seg n ; i in NAT by ORDINAL1:def_12; then i in Seg n by A1; then [i,1] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:87; then [i,1] in Indices (1. (F_Real,n)) by MATRIX_1:24; then consider q being FinSequence of REAL such that A3: q = (1_Rmatrix n) . i and (1_Rmatrix n) * (i,1) = q . 1 by MATRIX_1:def_5; len (1_Rmatrix n) = n by MATRIX_1:24; then i in dom (1_Rmatrix n) by A1, FINSEQ_3:25; then q in rng (1_Rmatrix n) by A3, FUNCT_1:def_3; then A4: len q = n by MATRIX_1:def_2; A5: for j being Nat st 1 <= j & j <= n holds q . j = (Base_FinSeq (n,i)) . j proof i in NAT by ORDINAL1:def_12; then A6: i in Seg n by A1; let j be Nat; ::_thesis: ( 1 <= j & j <= n implies q . j = (Base_FinSeq (n,i)) . j ) assume A7: ( 1 <= j & j <= n ) ; ::_thesis: q . j = (Base_FinSeq (n,i)) . j j in NAT by ORDINAL1:def_12; then j in Seg n by A7; then [i,j] in [:(Seg n),(Seg n):] by A6, ZFMISC_1:87; then A8: [i,j] in Indices (1. (F_Real,n)) by MATRIX_1:24; then A9: ex q0 being FinSequence of REAL st ( q0 = (1_Rmatrix n) . i & (1_Rmatrix n) * (i,j) = q0 . j ) by MATRIX_1:def_5; percases ( i = j or i <> j ) ; supposeA10: i = j ; ::_thesis: q . j = (Base_FinSeq (n,i)) . j then (1. (F_Real,n)) * (i,i) = 1_ F_Real by A8, MATRIX_1:def_11; hence q . j = (Base_FinSeq (n,i)) . j by A1, A3, A9, A10, Th75; ::_thesis: verum end; supposeA11: i <> j ; ::_thesis: q . j = (Base_FinSeq (n,i)) . j then (1. (F_Real,n)) * (i,j) = 0. F_Real by A8, MATRIX_1:def_11; hence q . j = (Base_FinSeq (n,i)) . j by A3, A7, A9, A11, Th76; ::_thesis: verum end; end; end; len (Base_FinSeq (n,i)) = n by Th74; hence (1_Rmatrix n) . i = Base_FinSeq (n,i) by A3, A4, A5, FINSEQ_1:14; ::_thesis: verum end; begin definition let n be Element of NAT ; let A be Matrix of n, REAL ; attrA is invertible means :Def5: :: MATRIXR2:def 5 ex B being Matrix of n, REAL st ( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ); end; :: deftheorem Def5 defines invertible MATRIXR2:def_5_:_ for n being Element of NAT for A being Matrix of n, REAL holds ( A is invertible iff ex B being Matrix of n, REAL st ( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) ); definition let n be Element of NAT ; let A be Matrix of n, REAL ; assume A1: A is invertible ; func Inv A -> Matrix of n, REAL means :Def6: :: MATRIXR2:def 6 ( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n ); existence ex b1 being Matrix of n, REAL st ( b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n ) by A1, Def5; uniqueness for b1, b2 being Matrix of n, REAL st b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n & b2 * A = 1_Rmatrix n & A * b2 = 1_Rmatrix n holds b1 = b2 proof let B1, B2 be Matrix of n, REAL ; ::_thesis: ( B1 * A = 1_Rmatrix n & A * B1 = 1_Rmatrix n & B2 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n implies B1 = B2 ) assume that B1 * A = 1_Rmatrix n and A2: A * B1 = 1_Rmatrix n and A3: B2 * A = 1_Rmatrix n and A * B2 = 1_Rmatrix n ; ::_thesis: B1 = B2 A4: ( len A = n & width A = n ) by MATRIX_1:24; ( len B1 = n & width B2 = n ) by MATRIX_1:24; then (B2 * A) * B1 = B2 * (1_Rmatrix n) by A2, A4, MATRIX_3:33; then B1 = B2 * (1_Rmatrix n) by A3, Th70; hence B1 = B2 by Th71; ::_thesis: verum end; end; :: deftheorem Def6 defines Inv MATRIXR2:def_6_:_ for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds for b3 being Matrix of n, REAL holds ( b3 = Inv A iff ( b3 * A = 1_Rmatrix n & A * b3 = 1_Rmatrix n ) ); registration let n be Element of NAT ; cluster 1_Rmatrix n -> invertible ; coherence 1_Rmatrix n is invertible proof (1_Rmatrix n) * (1_Rmatrix n) = 1_Rmatrix n by Th70; hence 1_Rmatrix n is invertible by Def5; ::_thesis: verum end; end; theorem :: MATRIXR2:79 for n being Element of NAT holds Inv (1_Rmatrix n) = 1_Rmatrix n proof let n be Element of NAT ; ::_thesis: Inv (1_Rmatrix n) = 1_Rmatrix n (1_Rmatrix n) * (1_Rmatrix n) = 1_Rmatrix n by Th70; hence Inv (1_Rmatrix n) = 1_Rmatrix n by Def6; ::_thesis: verum end; theorem Th80: :: MATRIXR2:80 for n being Element of NAT for A, B1, B2 being Matrix of n, REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds ( B1 = B2 & A is invertible ) proof let n be Element of NAT ; ::_thesis: for A, B1, B2 being Matrix of n, REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds ( B1 = B2 & A is invertible ) let A, B1, B2 be Matrix of n, REAL ; ::_thesis: ( B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n implies ( B1 = B2 & A is invertible ) ) assume that A1: B1 * A = 1_Rmatrix n and A2: A * B2 = 1_Rmatrix n ; ::_thesis: ( B1 = B2 & A is invertible ) A3: (B1 * A) * B2 = B1 * (A * B2) by Th28 .= B1 by A2, Th71 ; hence B1 = B2 by A1, Th70; ::_thesis: A is invertible (B1 * A) * B2 = B2 by A1, Th70; hence A is invertible by A1, A2, A3, Def5; ::_thesis: verum end; theorem :: MATRIXR2:81 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds Det (Inv A) = (Det A) " proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds Det (Inv A) = (Det A) " let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies Det (Inv A) = (Det A) " ) assume A is invertible ; ::_thesis: Det (Inv A) = (Det A) " then A * (Inv A) = 1_Rmatrix n by Def6; then Det (A * (Inv A)) = 1 by Th72; then A1: (Det A) * (Det (Inv A)) = 1 by Th46; percases ( Det A <> 0 or Det A = 0 ) ; suppose Det A <> 0 ; ::_thesis: Det (Inv A) = (Det A) " hence Det (Inv A) = (Det A) " by A1, XCMPLX_0:def_7; ::_thesis: verum end; suppose Det A = 0 ; ::_thesis: Det (Inv A) = (Det A) " hence Det (Inv A) = (Det A) " by A1; ::_thesis: verum end; end; end; theorem :: MATRIXR2:82 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds Det A <> 0 proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds Det A <> 0 let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies Det A <> 0 ) assume A is invertible ; ::_thesis: Det A <> 0 then A * (Inv A) = 1_Rmatrix n by Def6; then Det (A * (Inv A)) = 1 by Th72; then (Det A) * (Det (Inv A)) = 1 by Th46; hence Det A <> 0 ; ::_thesis: verum end; theorem :: MATRIXR2:83 for n being Element of NAT for A, B being Matrix of n, REAL st A is invertible & B is invertible holds ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) proof let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL st A is invertible & B is invertible holds ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) let A, B be Matrix of n, REAL ; ::_thesis: ( A is invertible & B is invertible implies ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) ) assume that A1: A is invertible and A2: B is invertible ; ::_thesis: ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) A3: ((Inv B) * (Inv A)) * (A * B) = (((Inv B) * (Inv A)) * A) * B by Th28 .= ((Inv B) * ((Inv A) * A)) * B by Th28 .= ((Inv B) * (1_Rmatrix n)) * B by A1, Def6 .= (Inv B) * B by Th71 .= 1_Rmatrix n by A2, Def6 ; A4: (A * B) * ((Inv B) * (Inv A)) = A * (B * ((Inv B) * (Inv A))) by Th28 .= A * ((B * (Inv B)) * (Inv A)) by Th28 .= A * ((1_Rmatrix n) * (Inv A)) by A2, Def6 .= (A * (1_Rmatrix n)) * (Inv A) by Th28 .= A * (Inv A) by Th71 .= 1_Rmatrix n by A1, Def6 ; hence A * B is invertible by A3, Def5; ::_thesis: Inv (A * B) = (Inv B) * (Inv A) hence Inv (A * B) = (Inv B) * (Inv A) by A3, A4, Def6; ::_thesis: verum end; theorem :: MATRIXR2:84 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds Inv (Inv A) = A proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds Inv (Inv A) = A let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies Inv (Inv A) = A ) assume A is invertible ; ::_thesis: Inv (Inv A) = A then A1: ( (Inv A) * A = 1_Rmatrix n & A * (Inv A) = 1_Rmatrix n ) by Def6; then Inv A is invertible by Def5; hence Inv (Inv A) = A by A1, Def6; ::_thesis: verum end; theorem :: MATRIXR2:85 ( 1_Rmatrix 0 = 0_Rmatrix 0 & 1_Rmatrix 0 = {} ) proof A1: len (1_Rmatrix 0) = 0 by MATRIX_1:24; len (0_Rmatrix 0) = 0 by MATRIX_1:24; then 0_Rmatrix 0 = {} ; hence 1_Rmatrix 0 = 0_Rmatrix 0 by A1; ::_thesis: 1_Rmatrix 0 = {} thus 1_Rmatrix 0 = {} by A1; ::_thesis: verum end; theorem Th86: :: MATRIXR2:86 for n being Element of NAT for x being FinSequence of REAL st len x = n & n > 0 holds (1_Rmatrix n) * x = x proof let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n & n > 0 holds (1_Rmatrix n) * x = x let x be FinSequence of REAL ; ::_thesis: ( len x = n & n > 0 implies (1_Rmatrix n) * x = x ) assume that A1: len x = n and A2: n > 0 ; ::_thesis: (1_Rmatrix n) * x = x A3: len (ColVec2Mx x) = len x by A1, A2, MATRIXR1:def_9; A4: len (Col ((ColVec2Mx x),1)) = len (ColVec2Mx x) by MATRIX_1:def_8; A5: for k being Nat st 1 <= k & k <= len (Col ((ColVec2Mx x),1)) holds (Col ((ColVec2Mx x),1)) . k = x . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) implies (Col ((ColVec2Mx x),1)) . k = x . k ) assume A6: ( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) ) ; ::_thesis: (Col ((ColVec2Mx x),1)) . k = x . k k in NAT by ORDINAL1:def_12; then A7: k in Seg (len (ColVec2Mx x)) by A4, A6; then A8: k in dom (ColVec2Mx x) by FINSEQ_1:def_3; then A9: (Col ((ColVec2Mx x),1)) . k = (ColVec2Mx x) * (k,1) by MATRIX_1:def_8; ( 1 in Seg 1 & Indices (ColVec2Mx x) = [:(dom (ColVec2Mx x)),(Seg 1):] ) by A1, A2, MATRIXR1:def_9; then [k,1] in Indices (ColVec2Mx x) by A8, ZFMISC_1:87; then consider p being FinSequence of REAL such that A10: p = (ColVec2Mx x) . k and A11: (ColVec2Mx x) * (k,1) = p . 1 by MATRIX_1:def_5; k in dom x by A3, A7, FINSEQ_1:def_3; then p = <*(x . k)*> by A1, A2, A10, MATRIXR1:def_9; hence (Col ((ColVec2Mx x),1)) . k = x . k by A9, A11, FINSEQ_1:40; ::_thesis: verum end; (1_Rmatrix n) * x = Col ((MXF2MXR (MXR2MXF (ColVec2Mx x))),1) by A1, A3, Th68 .= x by A3, A4, A5, FINSEQ_1:14 ; hence (1_Rmatrix n) * x = x ; ::_thesis: verum end; theorem Th87: :: MATRIXR2:87 for n being Element of NAT for x, y being FinSequence of REAL for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds ( A * x = y iff x = (Inv A) * y ) proof let n be Element of NAT ; ::_thesis: for x, y being FinSequence of REAL for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds ( A * x = y iff x = (Inv A) * y ) let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds ( A * x = y iff x = (Inv A) * y ) let A be Matrix of n, REAL ; ::_thesis: ( A is invertible & len x = n & len y = n & n > 0 implies ( A * x = y iff x = (Inv A) * y ) ) assume that A1: A is invertible and A2: len x = n and A3: len y = n and A4: n > 0 ; ::_thesis: ( A * x = y iff x = (Inv A) * y ) A5: ( width A = n & width (Inv A) = n ) by MATRIX_1:24; A6: len A = n by MATRIX_1:24; thus ( A * x = y implies x = (Inv A) * y ) ::_thesis: ( x = (Inv A) * y implies A * x = y ) proof assume A7: A * x = y ; ::_thesis: x = (Inv A) * y thus x = (1_Rmatrix n) * x by A2, A4, Th86 .= ((Inv A) * A) * x by A1, Def6 .= (Inv A) * y by A2, A4, A6, A5, A7, Th59 ; ::_thesis: verum end; A8: len (Inv A) = n by MATRIX_1:24; ( x = (Inv A) * y implies A * x = y ) proof assume A9: x = (Inv A) * y ; ::_thesis: A * x = y thus y = (1_Rmatrix n) * y by A3, A4, Th86 .= (A * (Inv A)) * y by A1, Def6 .= A * x by A3, A4, A8, A5, A9, Th59 ; ::_thesis: verum end; hence ( x = (Inv A) * y implies A * x = y ) ; ::_thesis: verum end; theorem Th88: :: MATRIXR2:88 for n being Element of NAT for x being FinSequence of REAL st len x = n holds x * (1_Rmatrix n) = x proof let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n holds x * (1_Rmatrix n) = x let x be FinSequence of REAL ; ::_thesis: ( len x = n implies x * (1_Rmatrix n) = x ) A1: width (LineVec2Mx x) = len x by MATRIXR1:def_10; assume len x = n ; ::_thesis: x * (1_Rmatrix n) = x then x * (1_Rmatrix n) = Line ((MXF2MXR (MXR2MXF (LineVec2Mx x))),1) by A1, Th67 .= x by MATRIXR1:48 ; hence x * (1_Rmatrix n) = x ; ::_thesis: verum end; theorem Th89: :: MATRIXR2:89 for n being Element of NAT for x, y being FinSequence of REAL for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds ( x * A = y iff x = y * (Inv A) ) proof let n be Element of NAT ; ::_thesis: for x, y being FinSequence of REAL for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds ( x * A = y iff x = y * (Inv A) ) let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds ( x * A = y iff x = y * (Inv A) ) let A be Matrix of n, REAL ; ::_thesis: ( A is invertible & len x = n & len y = n implies ( x * A = y iff x = y * (Inv A) ) ) assume that A1: A is invertible and A2: len x = n and A3: len y = n ; ::_thesis: ( x * A = y iff x = y * (Inv A) ) A4: ( len A = n & len (Inv A) = n ) by MATRIX_1:24; A5: width A = n by MATRIX_1:24; thus ( x * A = y implies x = y * (Inv A) ) ::_thesis: ( x = y * (Inv A) implies x * A = y ) proof assume A6: x * A = y ; ::_thesis: x = y * (Inv A) thus x = x * (1_Rmatrix n) by A2, Th88 .= x * (A * (Inv A)) by A1, Def6 .= y * (Inv A) by A2, A5, A4, A6, Th57 ; ::_thesis: verum end; assume A7: x = y * (Inv A) ; ::_thesis: x * A = y A8: width (Inv A) = n by MATRIX_1:24; thus y = y * (1_Rmatrix n) by A3, Th88 .= y * ((Inv A) * A) by A1, Def6 .= x * A by A3, A4, A8, A7, Th57 ; ::_thesis: verum end; theorem :: MATRIXR2:90 for n being Element of NAT for A being Matrix of n, REAL st n > 0 & A is invertible holds for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st n > 0 & A is invertible holds for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & A is invertible implies for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) assume that A1: n > 0 and A2: A is invertible ; ::_thesis: for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) assume A3: len y = n ; ::_thesis: ex x being FinSequence of REAL st ( len x = n & A * x = y ) reconsider x0 = (Inv A) * y as FinSequence of REAL ; ( len (Inv A) = n & width (Inv A) = n ) by MATRIX_1:24; then A4: len x0 = n by A1, A3, MATRIXR1:61; then A * x0 = y by A1, A2, A3, Th87; hence ex x being FinSequence of REAL st ( len x = n & A * x = y ) by A4; ::_thesis: verum end; theorem :: MATRIXR2:91 for n being Element of NAT for A being Matrix of n, REAL st A is invertible holds for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) assume A1: A is invertible ; ::_thesis: for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) assume A2: len y = n ; ::_thesis: ex x being FinSequence of REAL st ( len x = n & x * A = y ) reconsider x0 = y * (Inv A) as FinSequence of REAL ; len (Inv A) = n by MATRIX_1:24; then A3: len x0 = width (Inv A) by A2, MATRIXR1:62 .= n by MATRIX_1:24 ; then x0 * A = y by A1, A2, Th89; hence ex x being FinSequence of REAL st ( len x = n & x * A = y ) by A3; ::_thesis: verum end; theorem :: MATRIXR2:92 for n being Element of NAT for A being Matrix of n, REAL for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds for j being Element of NAT st 1 <= j & j <= n holds y . j = |(x,(Col (A,j)))| proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds for j being Element of NAT st 1 <= j & j <= n holds y . j = |(x,(Col (A,j)))| let A be Matrix of n, REAL ; ::_thesis: for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds for j being Element of NAT st 1 <= j & j <= n holds y . j = |(x,(Col (A,j)))| let x, y be FinSequence of REAL ; ::_thesis: ( len x = n & len y = n & x * A = y implies for j being Element of NAT st 1 <= j & j <= n holds y . j = |(x,(Col (A,j)))| ) assume that A1: len x = n and A2: len y = n and A3: x * A = y ; ::_thesis: for j being Element of NAT st 1 <= j & j <= n holds y . j = |(x,(Col (A,j)))| let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies y . j = |(x,(Col (A,j)))| ) assume ( 1 <= j & j <= n ) ; ::_thesis: y . j = |(x,(Col (A,j)))| then j in Seg (len (x * A)) by A2, A3; hence y . j = |(x,(Col (A,j)))| by A1, A3, MATRIX_1:24, MATRPROB:40; ::_thesis: verum end; theorem Th93: :: MATRIXR2:93 for n being Element of NAT for A being Matrix of n, REAL st ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) holds ex B being Matrix of n, REAL st B * A = 1_Rmatrix n proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) holds ex B being Matrix of n, REAL st B * A = 1_Rmatrix n let A be Matrix of n, REAL ; ::_thesis: ( ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) implies ex B being Matrix of n, REAL st B * A = 1_Rmatrix n ) defpred S1[ set , set ] means for s being Element of NAT for q being FinSequence of REAL st s = $1 & q = $2 holds ( len q = n & q * A = Base_FinSeq (n,s) ); assume A1: for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) ; ::_thesis: ex B being Matrix of n, REAL st B * A = 1_Rmatrix n A2: for i being Nat ex x being FinSequence of REAL st ( len x = n & x * A = Base_FinSeq (n,i) ) proof let i be Nat; ::_thesis: ex x being FinSequence of REAL st ( len x = n & x * A = Base_FinSeq (n,i) ) len (Base_FinSeq (n,i)) = n by Th74; hence ex x being FinSequence of REAL st ( len x = n & x * A = Base_FinSeq (n,i) ) by A1; ::_thesis: verum end; A3: for j being Nat st j in Seg n holds ex d being Element of REAL * st S1[j,d] proof let j be Nat; ::_thesis: ( j in Seg n implies ex d being Element of REAL * st S1[j,d] ) assume j in Seg n ; ::_thesis: ex d being Element of REAL * st S1[j,d] consider x being FinSequence of REAL such that A4: ( len x = n & x * A = Base_FinSeq (n,j) ) by A2; reconsider d0 = x as Element of REAL * by FINSEQ_1:def_11; for s being Element of NAT for q being FinSequence of REAL st s = j & q = d0 holds ( len q = n & q * A = Base_FinSeq (n,s) ) by A4; hence ex d being Element of REAL * st S1[j,d] ; ::_thesis: verum end; consider f being FinSequence of REAL * such that A5: ( len f = n & ( for j being Nat st j in Seg n holds S1[j,f /. j] ) ) from FINSEQ_4:sch_1(A3); for x being set st x in rng f holds ex p being FinSequence of REAL st ( x = p & len p = n ) proof let x be set ; ::_thesis: ( x in rng f implies ex p being FinSequence of REAL st ( x = p & len p = n ) ) assume x in rng f ; ::_thesis: ex p being FinSequence of REAL st ( x = p & len p = n ) then consider z being set such that A6: z in dom f and A7: f . z = x by FUNCT_1:def_3; reconsider j0 = z as Element of NAT by A6; reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def_11; z in Seg (len f) by A6, FINSEQ_1:def_3; then A8: len q0 = n by A5; q0 = x by A6, A7, PARTFUN1:def_6; hence ex p being FinSequence of REAL st ( x = p & len p = n ) by A8; ::_thesis: verum end; then reconsider M = f as Matrix of REAL by MATRIX_1:9; for p being FinSequence of REAL st p in rng M holds len p = n proof let p be FinSequence of REAL ; ::_thesis: ( p in rng M implies len p = n ) assume p in rng M ; ::_thesis: len p = n then consider z being set such that A9: z in dom f and A10: M . z = p by FUNCT_1:def_3; reconsider j0 = z as Element of NAT by A9; reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def_11; ( z in Seg (len f) & q0 = p ) by A9, A10, FINSEQ_1:def_3, PARTFUN1:def_6; hence len p = n by A5; ::_thesis: verum end; then reconsider B = M as Matrix of n, REAL by A5, MATRIX_1:def_2; for i4, j4 being Nat st [i4,j4] in Indices (B * A) holds (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) proof let i4, j4 be Nat; ::_thesis: ( [i4,j4] in Indices (B * A) implies (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) ) reconsider i = i4, j = j4 as Element of NAT by ORDINAL1:def_12; consider n2 being Nat such that A11: for x being set st x in rng (M * A) holds ex p being FinSequence of REAL st ( x = p & len p = n2 ) by MATRIX_1:9; assume A12: [i4,j4] in Indices (B * A) ; ::_thesis: (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) then j in Seg (width (M * A)) by ZFMISC_1:87; then A13: ( 1 <= j & j <= width (M * A) ) by FINSEQ_1:1; i in dom (M * A) by A12, ZFMISC_1:87; then A14: (M * A) . i in rng (M * A) by FUNCT_1:def_3; then consider p2 being FinSequence of REAL such that A15: (M * A) . i = p2 and A16: len p2 = n2 by A11; A17: len B = n by MATRIX_1:24; A18: [i,j] in [:(Seg n),(Seg n):] by A12, MATRIX_1:24; then [i,j] in Indices (1_Rmatrix n) by MATRIX_1:24; then A19: ex p3 being FinSequence of REAL st ( p3 = (1_Rmatrix n) . i & (1_Rmatrix n) * (i,j) = p3 . j ) by MATRIX_1:def_5; A20: width (B * A) = n by MATRIX_1:24; j in Seg n by A18, ZFMISC_1:87; then A21: ( 1 <= j & j <= n ) by FINSEQ_1:1; A22: i in Seg n by A18, ZFMISC_1:87; then A23: ( 1 <= i & i <= n ) by FINSEQ_1:1; A24: ( len (B * A) = n & ( for p being FinSequence of REAL st p in rng (B * A) holds len p = n ) ) by MATRIX_1:def_2; now__::_thesis:_(_(_i_=_j_&_(1_Rmatrix_n)_*_(i,j)_=_p2_._j_)_or_(_i_<>_j_&_(1_Rmatrix_n)_*_(i,j)_=_p2_._j_)_) percases ( i = j or i <> j ) ; caseA25: i = j ; ::_thesis: (1_Rmatrix n) * (i,j) = p2 . j reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def_11; A26: g * A = Base_FinSeq (n,i) by A5, A22; len B = n by MATRIX_1:24; then f /. i = M . i by A23, FINSEQ_4:15; then A27: g = Line (B,i) by A23, A17, Lm2; A28: (1_Rmatrix n) * (i,j) = (Base_FinSeq (n,i)) . i by A19, A23, A25, Th78 .= 1 by A23, Th75 ; p2 . j = (B * A) * (i,j) by A24, A14, A15, A16, A13, A23, A20, Th2 .= (Base_FinSeq (n,i)) . j by A12, A26, A27, Th61 .= 1 by A23, A25, Th75 ; hence (1_Rmatrix n) * (i,j) = p2 . j by A28; ::_thesis: verum end; caseA29: i <> j ; ::_thesis: (1_Rmatrix n) * (i,j) = p2 . j reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def_11; len B = n by MATRIX_1:24; then f /. i = M . i by A23, FINSEQ_4:15; then g = Line (B,i) by A23, A17, Lm2; then A30: (Line (B,i)) * A = Base_FinSeq (n,i) by A5, A22; A31: (1_Rmatrix n) * (i,j) = (Base_FinSeq (n,i)) . j by A19, A23, Th78 .= 0 by A21, A29, Th76 ; p2 . j = (B * A) * (i,j) by A24, A14, A15, A16, A13, A23, A20, Th2 .= (Base_FinSeq (n,i)) . j by A12, A30, Th61 .= 0 by A21, A29, Th76 ; hence (1_Rmatrix n) * (i,j) = p2 . j by A31; ::_thesis: verum end; end; end; hence (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) by A12, A15, MATRIX_1:def_5; ::_thesis: verum end; hence ex B being Matrix of n, REAL st B * A = 1_Rmatrix n by MATRIX_1:27; ::_thesis: verum end; theorem :: MATRIXR2:94 for n being Element of NAT for x being FinSequence of REAL for A being Matrix of n, REAL st n > 0 & len x = n holds (A @) * x = x * A proof let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL for A being Matrix of n, REAL st n > 0 & len x = n holds (A @) * x = x * A let x be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st n > 0 & len x = n holds (A @) * x = x * A let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & len x = n implies (A @) * x = x * A ) A1: ( len A = n & width A = n ) by MATRIX_1:24; assume ( n > 0 & len x = n ) ; ::_thesis: (A @) * x = x * A hence (A @) * x = x * A by A1, MATRIXR1:52; ::_thesis: verum end; theorem Th95: :: MATRIXR2:95 for n being Element of NAT for x being FinSequence of REAL for A being Matrix of n, REAL st n > 0 & len x = n holds x * (A @) = A * x proof let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL for A being Matrix of n, REAL st n > 0 & len x = n holds x * (A @) = A * x let x be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st n > 0 & len x = n holds x * (A @) = A * x let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & len x = n implies x * (A @) = A * x ) A1: ( len A = n & width A = n ) by MATRIX_1:24; assume ( n > 0 & len x = n ) ; ::_thesis: x * (A @) = A * x hence x * (A @) = A * x by A1, MATRIXR1:53; ::_thesis: verum end; theorem Th96: :: MATRIXR2:96 for n being Element of NAT for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) holds ex B being Matrix of n, REAL st A * B = 1_Rmatrix n proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) holds ex B being Matrix of n, REAL st A * B = 1_Rmatrix n let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) implies ex B being Matrix of n, REAL st A * B = 1_Rmatrix n ) assume that A1: n > 0 and A2: for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) ; ::_thesis: ex B being Matrix of n, REAL st A * B = 1_Rmatrix n for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * (A @) = y ) proof let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st ( len x = n & x * (A @) = y ) ) assume len y = n ; ::_thesis: ex x being FinSequence of REAL st ( len x = n & x * (A @) = y ) then consider x0 being FinSequence of REAL such that A3: len x0 = n and A4: A * x0 = y by A2; x0 * (A @) = A * x0 by A1, A3, Th95; hence ex x being FinSequence of REAL st ( len x = n & x * (A @) = y ) by A3, A4; ::_thesis: verum end; then consider B being Matrix of n, REAL such that A5: B * (A @) = 1_Rmatrix n by Th93; (B * (A @)) @ = 1_Rmatrix n by A5, Th64; then ((A @) @) * (B @) = 1_Rmatrix n by Th30; then A * (B @) = 1_Rmatrix n by Th29; hence ex B being Matrix of n, REAL st A * B = 1_Rmatrix n ; ::_thesis: verum end; theorem :: MATRIXR2:97 for n being Element of NAT for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds A is invertible proof let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds A is invertible let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & ( for y being FinSequence of REAL st len y = n holds ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) implies A is invertible ) assume that A1: n > 0 and A2: for y being FinSequence of REAL st len y = n holds ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ; ::_thesis: A is invertible for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & x * A = y ) proof let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st ( len x = n & x * A = y ) ) assume len y = n ; ::_thesis: ex x being FinSequence of REAL st ( len x = n & x * A = y ) then ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A2; hence ex x being FinSequence of REAL st ( len x = n & x * A = y ) ; ::_thesis: verum end; then A3: ex B1 being Matrix of n, REAL st B1 * A = 1_Rmatrix n by Th93; for y being FinSequence of REAL st len y = n holds ex x being FinSequence of REAL st ( len x = n & A * x = y ) proof let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st ( len x = n & A * x = y ) ) assume len y = n ; ::_thesis: ex x being FinSequence of REAL st ( len x = n & A * x = y ) then ex x1, x2 being FinSequence of REAL st ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A2; hence ex x being FinSequence of REAL st ( len x = n & A * x = y ) ; ::_thesis: verum end; then ex B2 being Matrix of n, REAL st A * B2 = 1_Rmatrix n by A1, Th96; hence A is invertible by A3, Th80; ::_thesis: verum end;