let l, n, k be Nat; :: thesis: for K being Field
for a being Element of K st l in dom (1. K,n) & k in dom (1. K,n) & k <> l holds
( RLineXS (1. K,n),l,k,a is invertible & (RLineXS (1. K,n),l,k,a) ~ = RLineXS (1. K,n),l,k,(- a) )
let K be Field; :: thesis: for a being Element of K st l in dom (1. K,n) & k in dom (1. K,n) & k <> l holds
( RLineXS (1. K,n),l,k,a is invertible & (RLineXS (1. K,n),l,k,a) ~ = RLineXS (1. K,n),l,k,(- a) )
let a be Element of K; :: thesis: ( l in dom (1. K,n) & k in dom (1. K,n) & k <> l implies ( RLineXS (1. K,n),l,k,a is invertible & (RLineXS (1. K,n),l,k,a) ~ = RLineXS (1. K,n),l,k,(- a) ) )
assume that
A1: ( l in dom (1. K,n) & k in dom (1. K,n) ) and
A2: k <> l ; :: thesis: ( RLineXS (1. K,n),l,k,a is invertible & (RLineXS (1. K,n),l,k,a) ~ = RLineXS (1. K,n),l,k,(- a) )
set B = RLineXS (1. K,n),l,k,(- a);
for i, j being Nat st [i,j] in Indices (1. K,n) holds
(1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a) * i,j by A1, A2, Lm4;
then A3: 1. K,n = RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a by MATRIX_1:28;
set b = - a;
set A = RLineXS (1. K,n),l,k,a;
a + (- a) = 0. K by RLVECT_1:def 11;
then a = - (- a) by RLVECT_1:19;
then for i, j being Nat st [i,j] in Indices (1. K,n) holds
(1. K,n) * i,j = (RLineXS (RLineXS (1. K,n),l,k,a),l,k,(- a)) * i,j by A1, A2, Lm4;
then A4: 1. K,n = RLineXS (RLineXS (1. K,n),l,k,a),l,k,(- a) by MATRIX_1:28;
( (RLineXS (1. K,n),l,k,a) * (RLineXS (1. K,n),l,k,(- a)) = RLineXS (RLineXS (1. K,n),l,k,(- a)),l,k,a & (RLineXS (1. K,n),l,k,(- a)) * (RLineXS (1. K,n),l,k,a) = RLineXS (RLineXS (1. K,n),l,k,a),l,k,(- a) ) by A1, Th8;
then A5: RLineXS (1. K,n),l,k,(- a) is_reverse_of RLineXS (1. K,n),l,k,a by A3, A4, MATRIX_6:def 2;
then RLineXS (1. K,n),l,k,a is invertible by MATRIX_6:def 3;
hence ( RLineXS (1. K,n),l,k,a is invertible & (RLineXS (1. K,n),l,k,a) ~ = RLineXS (1. K,n),l,k,(- a) ) by A5, MATRIX_6:def 4; :: thesis: verum