let K be Field; :: thesis: 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; :: thesis: for A being Matrix of K holds

( (1_ K) * A = A & a * (b * A) = (a * b) * A )

let A be Matrix of K; :: thesis: ( (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;

.= len A by MATRIX_3:def 5

.= len ((a * 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; :: thesis: verum

for A being Matrix of K holds

( (1_ K) * A = A & a * (b * A) = (a * b) * A )

let a, b be Element of K; :: thesis: for A being Matrix of K holds

( (1_ K) * A = A & a * (b * A) = (a * b) * A )

let A be Matrix of K; :: thesis: ( (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 :: thesis: for i, j being Nat st [i,j] in Indices A holds

A * (i,j) = ((1_ K) * A) * (i,j)

A3: len (a * (b * A)) =
len (b * A)
by MATRIX_3:def 5
A * (i,j) = ((1_ K) * A) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = ((1_ K) * A) * (i,j) )

assume A2: [i,j] in Indices A ; :: thesis: 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 ; :: thesis: verum

end;assume A2: [i,j] in Indices A ; :: thesis: 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 ; :: thesis: verum

.= len A by MATRIX_3:def 5

.= len ((a * b) * A) by MATRIX_3:def 5 ;

A4: now :: thesis: for i, j being Nat st [i,j] in Indices (a * (b * A)) holds

(a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)

A8: width (a * (b * A)) =
width (b * A)
by MATRIX_3:def 5
(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; :: 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)

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 ; :: thesis: verum

end;A6: Indices (a * (b * A)) = Indices (b * A) by MATRIXR1:18;

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)

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 ; :: thesis: verum

.= 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; :: thesis: verum