let K be Field; for a, b being Element of K
for A being Matrix of K holds
( (1_ K) * A = A & a * (b * A) = (a * b) * A )
let a, b be Element of K; for A being Matrix of K holds
( (1_ K) * A = A & a * (b * A) = (a * b) * A )
let A be Matrix of K; ( (1_ K) * A = A & a * (b * A) = (a * b) * A )
set 1A = (1_ K) * A;
set bA = b * A;
set ab = a * b;
set abA = (a * b) * A;
A1:
now for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = ((1_ K) * A) * (i,j)let i,
j be
Nat;
( [i,j] in Indices A implies A * (i,j) = ((1_ K) * A) * (i,j) )assume A2:
[i,j] in Indices A
;
A * (i,j) = ((1_ K) * A) * (i,j)thus A * (
i,
j) =
(1_ K) * (A * (i,j))
.=
((1_ K) * A) * (
i,
j)
by A2, MATRIX_3:def 5
;
verum end;
A3: len (a * (b * A)) =
len (b * A)
by MATRIX_3:def 5
.=
len A
by MATRIX_3:def 5
.=
len ((a * b) * A)
by MATRIX_3:def 5
;
A4:
now for i, j being Nat st [i,j] in Indices (a * (b * A)) holds
(a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)A5:
Indices (b * A) = Indices A
by MATRIXR1:18;
A6:
Indices (a * (b * A)) = Indices (b * A)
by MATRIXR1:18;
let i,
j be
Nat;
( [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))
;
(a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)thus (a * (b * A)) * (
i,
j) =
a * ((b * A) * (i,j))
by A7, A6, MATRIX_3:def 5
.=
a * (b * (A * (i,j)))
by A7, A6, A5, MATRIX_3:def 5
.=
(a * b) * (A * (i,j))
by GROUP_1:def 3
.=
((a * b) * A) * (
i,
j)
by A7, A6, A5, MATRIX_3:def 5
;
verum end;
A8: width (a * (b * A)) =
width (b * A)
by MATRIX_3:def 5
.=
width A
by MATRIX_3:def 5
.=
width ((a * b) * A)
by MATRIX_3:def 5
;
( len ((1_ K) * A) = len A & width ((1_ K) * A) = width A )
by MATRIX_3:def 5;
hence
( (1_ K) * A = A & a * (b * A) = (a * b) * A )
by A1, A3, A8, A4, MATRIX_0:21; verum