Can the Symbolic Math Toolbox Be Used to Prove Matrix Identities?

With the following defintions

syms s
A = symmatrix('A',3);
B = symmatrix('B',[3 1]);
C = symmatrix('C',[1 3]);
L = symmatrix('L',[3 1]);
I = sym(eye(3));
LHS = inv(s*I - A + L*C)*B + inv(s*I - A + L*C)*L*C*inv(s*I - A)*B;
RHS = inv(s*I - A)*B;

I'd like to prove the following identity

ident = LHS == RHS

ident = 

Is there any other way to have the software verify that ident is always true besides subbing in symbolic values for the matrix elements?

isAlways(symmatrix2sym(ident))

ans = 3×1 logical array
   1
   1
   1

Answer 1

[Walter Roberson]

No.

[Paul]

Too bad the even children doesn't work. Oh well.

syms s
A = symmatrix('A',3);
B = symmatrix('B',[3 1]);
C = symmatrix('C',[1 3]);
L = symmatrix('L',[3 1]);
I = sym(eye(3));
LHS = inv(s*I - A + L*C)*B + inv(s*I - A + L*C)*L*C*inv(s*I - A)*B;
RHS = inv(s*I - A)*B;
ident = LHS == RHS

ident = 

children(LHS)

Incorrect number or types of inputs or outputs for function children.

[John D'Errico]

Certainly there will be issues with the inverses, which need not even exist.

[Paul]

I don't understand why that would be an issue. It appears that the inverse is assumed to exist. Is there an "assumptions" type of thing for symmatrix objects where one could could change that assumption?

A = symmatrix('A',[3 3]);
A*inv(A)

ans = 

[Walter Roberson]

Although children does not appear to be defined for symmatrix you can work around that using internal calls that are deliberately no longer documented.

syms s
A = symmatrix('A',3);
B = symmatrix('B',[3 1]);
C = symmatrix('C',[1 3]);
L = symmatrix('L',[3 1]);
I = sym(eye(3));
LHS = inv(s*I - A + L*C)*B + inv(s*I - A + L*C)*L*C*inv(s*I - A)*B;
RHS = inv(s*I - A)*B;
ident = LHS == RHS

ident = 

feval(symengine, 'op', LHS, 0)

ans = 

feval(symengine, 'op', LHS).'

ans = 

feval(symengine, 'op', RHS, 0)

ans = 

feval(symengine, 'op', RHS).'

ans = 

whos

  Name        Size            Bytes  Class        Attributes

  A           3x3                 8  symmatrix              
  B           3x1                 8  symmatrix              
  C           1x3                 8  symmatrix              
  I           3x3                 8  sym                    
  L           3x1                 8  symmatrix              
  LHS         3x1                 8  symmatrix              
  RHS         3x1                 8  symmatrix              
  ans         2x1                 8  sym                    
  cmdout      1x33               66  char                   
  ident       3x1                 8  symmatrix              
  s           1x1                 8  sym                    

[Walter Roberson]

syms s
A = symmatrix('A',3);
B = symmatrix('B',[3 1]);
C = symmatrix('C',[1 3]);
L = symmatrix('L',[3 1]);
I = sym(eye(3));
LHS = inv(s*I - A + L*C)*B + inv(s*I - A + L*C)*L*C*inv(s*I - A)*B;
RHS = inv(s*I - A)*B;
ident = LHS == RHS

ident = 

feval(symengine, 'coerce', ident, 'DOM_STRING')

ans = 

"Dom::SymbolicMatrix("L", 3, 1)*Dom::SymbolicMatrix("C", 1, 3) + Dom::SymbolicMatrix("s", 1, 1)*Dom::SymbolicMatrix::eye(3) - Dom::SymbolicMatrix("A", 3, 3)^-1*Dom::SymbolicMatrix("L", 3, 1)*Dom::SymbolicMatrix("C", 1, 3)*Dom::SymbolicMatrix("s", 1, 1)*Dom::SymbolicMatrix::eye(3) - Dom::SymbolicMatrix("A", 3, 3)^-1*Dom::SymbolicMatrix("B", 3, 1) + Dom::SymbolicMatrix("L", 3, 1)*Dom::SymbolicMatrix("C", 1, 3) + Dom::SymbolicMatrix("s", 1, 1)*Dom::SymbolicMatrix::eye(3) - Dom::SymbolicMatrix("A", 3, 3)^-1*Dom::SymbolicMatrix("B", 3, 1) == Dom::SymbolicMatrix("s", 1, 1)*Dom::SymbolicMatrix::eye(3) - Dom::SymbolicMatrix("A", 3, 3)^-1*Dom::SymbolicMatrix("B", 3, 1)"