let I1, I2 be invertible Matrix of n,F_Real; :: thesis: ( I1 * (i,i) = cos r & I1 * (j,j) = cos r & I1 * (i,j) = sin r & I1 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices I1 holds
( ( k = m & k <> i & k <> j implies I1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I1 * (k,m) = 0. F_Real ) ) ) & I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices I2 holds
( ( k = m & k <> i & k <> j implies I2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I2 * (k,m) = 0. F_Real ) ) ) implies I1 = I2 )
assume that
A4: ( I1 * (i,i) = cos r & I1 * (j,j) = cos r & I1 * (i,j) = sin r & I1 * (j,i) = - (sin r) ) and
A5: for k, m being Nat st [k,m] in Indices I1 holds
( ( k = m & k <> i & k <> j implies I1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I1 * (k,m) = 0. F_Real ) ) and
A6: ( I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) ) and
A7: for k, m being Nat st [k,m] in Indices I2 holds
( ( k = m & k <> i & k <> j implies I2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I2 * (k,m) = 0. F_Real ) ) ; :: thesis: I1 = I2
for k, m being Nat st [k,m] in Indices I1 holds
I1 * (k,m) = I2 * (k,m)
proof
let k, m be Nat; :: thesis: ( [k,m] in Indices I1 implies I1 * (k,m) = I2 * (k,m) )
assume A8: [k,m] in Indices I1 ; :: thesis: I1 * (k,m) = I2 * (k,m)
then A9: [k,m] in Indices I2 by MATRIX_0:26;
per cases ( ( k = m & ( k = i or k = j ) ) or ( k <> m & ( ( k = i & m = j ) or ( k = j & m = i ) ) ) or ( k = m & k <> i & k <> j ) or ( k <> m & ( ( k = i & m <> j ) or ( k = j & m <> i ) or ( m = i & k <> j ) or ( m = j & k <> i ) or ( k <> i & k <> j & m <> i & m <> j ) ) ) ) ;
suppose ( ( k = m & ( k = i or k = j ) ) or ( k <> m & ( ( k = i & m = j ) or ( k = j & m = i ) ) ) ) ; :: thesis: I1 * (k,m) = I2 * (k,m)
hence I1 * (k,m) = I2 * (k,m) by A4, A6; :: thesis: verum
end;
suppose A10: ( k = m & k <> i & k <> j ) ; :: thesis: I1 * (k,m) = I2 * (k,m)
then I1 * (k,m) = 1. F_Real by A5, A8;
hence I1 * (k,m) = I2 * (k,m) by A7, A9, A10; :: thesis: verum
end;
suppose A11: ( k <> m & ( ( k = i & m <> j ) or ( k = j & m <> i ) or ( m = i & k <> j ) or ( m = j & k <> i ) or ( k <> i & k <> j & m <> i & m <> j ) ) ) ; :: thesis: I1 * (k,m) = I2 * (k,m)
then A12: {k,m} <> {i,j} by ZFMISC_1:6;
then I1 * (k,m) = 0. F_Real by A5, A8, A11;
hence I1 * (k,m) = I2 * (k,m) by A7, A9, A11, A12; :: thesis: verum
end;
end;
end;
hence I1 = I2 by MATRIX_0:27; :: thesis: verum