Metamath Proof Explorer


Theorem matval

Description: Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matval.a A=NMatR
matval.g G=RfreeLModN×N
matval.t ·˙=RmaMulNNN
Assertion matval NFinRVA=GsSetndx·˙

Proof

Step Hyp Ref Expression
1 matval.a A=NMatR
2 matval.g G=RfreeLModN×N
3 matval.t ·˙=RmaMulNNN
4 elex RVRV
5 id r=Rr=R
6 id n=Nn=N
7 6 sqxpeqd n=Nn×n=N×N
8 5 7 oveqan12rd n=Nr=RrfreeLModn×n=RfreeLModN×N
9 8 2 eqtr4di n=Nr=RrfreeLModn×n=G
10 6 6 6 oteq123d n=Nnnn=NNN
11 5 10 oveqan12rd n=Nr=RrmaMulnnn=RmaMulNNN
12 11 3 eqtr4di n=Nr=RrmaMulnnn=·˙
13 12 opeq2d n=Nr=RndxrmaMulnnn=ndx·˙
14 9 13 oveq12d n=Nr=RrfreeLModn×nsSetndxrmaMulnnn=GsSetndx·˙
15 df-mat Mat=nFin,rVrfreeLModn×nsSetndxrmaMulnnn
16 ovex GsSetndx·˙V
17 14 15 16 ovmpoa NFinRVNMatR=GsSetndx·˙
18 4 17 sylan2 NFinRVNMatR=GsSetndx·˙
19 1 18 eqtrid NFinRVA=GsSetndx·˙