environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, VECTSP_1, STRUCT_0, EUCLID, FINSEQ_1, FINSEQ_2, SUPINF_2, RELAT_1, ALGSTR_0, ARYTM_3, ARYTM_1, RVSUM_1, FUNCT_1, PARTFUN1, TARSKI, ZFMISC_1, NAT_1, XXREAL_0, GROUP_1, ORDINAL4, CARD_1, FVSUM_1, CARD_3, MATRIX_1, PRALG_1, MESFUNC1, MATRIX_6, TREES_1, MATRIXR2, AFINSQ_1, FUNCOP_1, QC_LANG1, FINSOP_1, INCSP_1, FUNCT_7, RFINSEQ, MATRIX_3, MATRIX14;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, RELAT_1, FUNCT_1, BINOP_1, ALGSTR_0, ZFMISC_1, MATRIX_0, FVSUM_1, PARTFUN1, FUNCT_3, ORDINAL1, NUMBERS, FINSEQ_7, FUNCT_2, FUNCOP_1, FINSEQ_1, STRUCT_0, GROUP_1, MATRIX_1, MATRIX_3, MATRIX_6, XCMPLX_0, NAT_1, NAT_D, VECTSP_1, FINSEQ_2, FINSOP_1, RFINSEQ;
definitions ;
theorems MATRIX_3, VECTSP_1, MATRIX_0, MATRIX_4, GROUP_1, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_7, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, FUNCT_2, XBOOLE_0, ZFMISC_1, MATRIX_7, MATRIXR1, FINSEQ_3, XXREAL_0, ORDINAL1, FINSEQ_4, MATRIXR2, XREAL_1, FUNCOP_1, RLVECT_1, MATRIX_6, MATRIX12, POLYNOM1, PARTFUN1, NAT_D, CARD_1, MATRIX_1;
schemes NAT_1, MATRIX_0;
registrations FINSEQ_2, XREAL_0, NAT_1, FUNCOP_1, STRUCT_0, VECTSP_1, ORDINAL1, RELAT_1, CARD_1, FINSEQ_1, MATRIX_6, MATRIX_0;
constructors HIDDEN, FUNCT_3, FINSEQ_7, SETWISEO, FINSOP_1, JORDAN3, RFINSEQ, MATRIX_6, NAT_D, RELSET_1, FVSUM_1, MATRIX_1, MATRIX_3, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, MATRIX_0, MATRIX_1, ALGSTR_0;
expansions ;
theorem Th37:
for
n being
Element of
NAT for
K being
Field for
a being
Element of
K for
P,
Q being
Matrix of
n,
K st
n > 0 &
a <> 0. K &
P * (1,1)
= a " & ( for
i being
Element of
NAT st 1
< i &
i <= n holds
P . i = Base_FinSeq (
K,
n,
i) ) &
Q * (1,1)
= a & ( for
j being
Element of
NAT st 1
< j &
j <= n holds
Q * (1,
j)
= - (a * (P * (1,j))) ) & ( for
i being
Element of
NAT st 1
< i &
i <= n holds
Q . i = Base_FinSeq (
K,
n,
i) ) holds
(
P is
invertible &
Q = P ~ )
theorem Th43:
for
K being
Field for
n being
Element of
NAT for
i0 being
Nat for
A being
Matrix of
n,
K st 1
<= i0 &
i0 <= n &
A = SwapDiagonal (
K,
n,
i0) holds
for
i,
j being
Nat st 1
<= i &
i <= n & 1
<= j &
j <= n &
i0 <> 1 holds
( (
i = 1 &
j = i0 implies
A * (
i,
j)
= 1. K ) & (
i = i0 &
j = 1 implies
A * (
i,
j)
= 1. K ) & (
i = 1 &
j = 1 implies
A * (
i,
j)
= 0. K ) & (
i = i0 &
j = i0 implies
A * (
i,
j)
= 0. K ) & ( ( ( not
i = 1 & not
i = i0 ) or ( not
j = 1 & not
j = i0 ) ) implies ( (
i = j implies
A * (
i,
j)
= 1. K ) & (
i <> j implies
A * (
i,
j)
= 0. K ) ) ) )
theorem Th47:
for
K being
Field for
n,
i0 being
Element of
NAT for
A being
Matrix of
n,
K st 1
<= i0 &
i0 <= n &
i0 <> 1 & ( for
i,
j being
Nat st 1
<= i &
i <= n & 1
<= j &
j <= n holds
( (
i = 1 &
j = i0 implies
A * (
i,
j)
= 1. K ) & (
i = i0 &
j = 1 implies
A * (
i,
j)
= 1. K ) & (
i = 1 &
j = 1 implies
A * (
i,
j)
= 0. K ) & (
i = i0 &
j = i0 implies
A * (
i,
j)
= 0. K ) & ( ( ( not
i = 1 & not
i = i0 ) or ( not
j = 1 & not
j = i0 ) ) implies ( (
i = j implies
A * (
i,
j)
= 1. K ) & (
i <> j implies
A * (
i,
j)
= 0. K ) ) ) ) ) holds
A = SwapDiagonal (
K,
n,
i0)
theorem Th48:
for
n being
Element of
NAT for
K being
Field for
A being
Matrix of
n,
K for
i0 being
Element of
NAT st 1
<= i0 &
i0 <= n holds
( ( for
j being
Element of
NAT st 1
<= j &
j <= n holds
(
((SwapDiagonal (K,n,i0)) * A) * (
i0,
j)
= A * (1,
j) &
((SwapDiagonal (K,n,i0)) * A) * (1,
j)
= A * (
i0,
j) ) ) & ( for
i,
j being
Element of
NAT st
i <> 1 &
i <> i0 & 1
<= i &
i <= n & 1
<= j &
j <= n holds
((SwapDiagonal (K,n,i0)) * A) * (
i,
j)
= A * (
i,
j) ) )
theorem Th51:
for
n being
Element of
NAT for
K being
Field for
A being
Matrix of
n,
K for
j0 being
Element of
NAT st 1
<= j0 &
j0 <= n holds
( ( for
i being
Element of
NAT st 1
<= i &
i <= n holds
(
(A * (SwapDiagonal (K,n,j0))) * (
i,
j0)
= A * (
i,1) &
(A * (SwapDiagonal (K,n,j0))) * (
i,1)
= A * (
i,
j0) ) ) & ( for
i,
j being
Element of
NAT st
j <> 1 &
j <> j0 & 1
<= i &
i <= n & 1
<= j &
j <= n holds
(A * (SwapDiagonal (K,n,j0))) * (
i,
j)
= A * (
i,
j) ) )