reconsider rr = 1 + 1 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider e3 = ((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) as Element of F_Complex ;
let M be Matrix of COMPLEX; (M + M) + M = 3 * M
A1:
( len M = len (COMPLEX2Field M) & width M = width (COMPLEX2Field M) )
;
A2: (1_ F_Complex) + (1_ F_Complex) =
the addF of F_Complex . ((1_ F_Complex),(1_ F_Complex))
by RLVECT_1:2
.=
addcomplex . (1r,1r)
by COMPLFLD:8, COMPLFLD:def 1
.=
1 + 1
by BINOP_2:def 3, COMPLEX1:def 4
;
((1_ F_Complex) + (1_ F_Complex)) + (1_ F_Complex) =
the addF of F_Complex . (((1_ F_Complex) + (1_ F_Complex)),(1_ F_Complex))
by RLVECT_1:2
.=
addcomplex . ((1 + 1),1)
by A2, COMPLFLD:def 1
.=
rr + 1
by BINOP_2:def 3
.=
3
;
then 3 * M =
Field2COMPLEX (e3 * (COMPLEX2Field M))
by Def7
.=
Field2COMPLEX (((1_ F_Complex) * (COMPLEX2Field M)) + (((1_ F_Complex) + (1_ F_Complex)) * (COMPLEX2Field M)))
by Th12
.=
Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex) + (1_ F_Complex)) * (COMPLEX2Field M)))
by Th9
.=
Field2COMPLEX ((COMPLEX2Field M) + (((1_ F_Complex) * (COMPLEX2Field M)) + ((1_ F_Complex) * (COMPLEX2Field M))))
by Th12
.=
Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + ((1_ F_Complex) * (COMPLEX2Field M))))
by Th9
.=
Field2COMPLEX ((COMPLEX2Field M) + ((COMPLEX2Field M) + (COMPLEX2Field M)))
by Th9
.=
Field2COMPLEX (((COMPLEX2Field M) + (COMPLEX2Field M)) + (COMPLEX2Field M))
by A1, MATRIX_3:3
;
hence
(M + M) + M = 3 * M
; verum