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 = ( N Mat R )
matval.g 
|- G = ( R freeLMod ( N X. N ) )
matval.t 
|- .x. = ( R maMul <. N , N , N >. )
Assertion matval 
|- ( ( N e. Fin /\ R e. V ) -> A = ( G sSet <. ( .r ` ndx ) , .x. >. ) )

Proof

Step Hyp Ref Expression
1 matval.a 
 |-  A = ( N Mat R )
2 matval.g 
 |-  G = ( R freeLMod ( N X. N ) )
3 matval.t 
 |-  .x. = ( R maMul <. N , N , N >. )
4 elex 
 |-  ( R e. V -> R e. _V )
5 id 
 |-  ( r = R -> r = R )
6 id 
 |-  ( n = N -> n = N )
7 6 sqxpeqd 
 |-  ( n = N -> ( n X. n ) = ( N X. N ) )
8 5 7 oveqan12rd 
 |-  ( ( n = N /\ r = R ) -> ( r freeLMod ( n X. n ) ) = ( R freeLMod ( N X. N ) ) )
9 8 2 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( r freeLMod ( n X. n ) ) = G )
10 6 6 6 oteq123d 
 |-  ( n = N -> <. n , n , n >. = <. N , N , N >. )
11 5 10 oveqan12rd 
 |-  ( ( n = N /\ r = R ) -> ( r maMul <. n , n , n >. ) = ( R maMul <. N , N , N >. ) )
12 11 3 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( r maMul <. n , n , n >. ) = .x. )
13 12 opeq2d 
 |-  ( ( n = N /\ r = R ) -> <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. = <. ( .r ` ndx ) , .x. >. )
14 9 13 oveq12d 
 |-  ( ( n = N /\ r = R ) -> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) = ( G sSet <. ( .r ` ndx ) , .x. >. ) )
15 df-mat 
 |-  Mat = ( n e. Fin , r e. _V |-> ( ( r freeLMod ( n X. n ) ) sSet <. ( .r ` ndx ) , ( r maMul <. n , n , n >. ) >. ) )
16 ovex 
 |-  ( G sSet <. ( .r ` ndx ) , .x. >. ) e. _V
17 14 15 16 ovmpoa 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( N Mat R ) = ( G sSet <. ( .r ` ndx ) , .x. >. ) )
18 4 17 sylan2 
 |-  ( ( N e. Fin /\ R e. V ) -> ( N Mat R ) = ( G sSet <. ( .r ` ndx ) , .x. >. ) )
19 1 18 eqtrid 
 |-  ( ( N e. Fin /\ R e. V ) -> A = ( G sSet <. ( .r ` ndx ) , .x. >. ) )