Metamath Proof Explorer

Theorem d1mat2pmat

Description: The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses d1mat2pmat.t 
|- T = ( N matToPolyMat R )
d1mat2pmat.b 
|- B = ( Base ` ( N Mat R ) )
d1mat2pmat.p 
|- P = ( Poly1 ` R )
d1mat2pmat.s 
|- S = ( algSc ` P )
Assertion d1mat2pmat 
|- ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( T ` M ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } )

Proof

Step Hyp Ref Expression
1 d1mat2pmat.t 
 |-  T = ( N matToPolyMat R )
2 d1mat2pmat.b 
 |-  B = ( Base ` ( N Mat R ) )
3 d1mat2pmat.p 
 |-  P = ( Poly1 ` R )
4 d1mat2pmat.s 
 |-  S = ( algSc ` P )
5 snfi 
 |-  { A } e. Fin
6 eleq1 
 |-  ( N = { A } -> ( N e. Fin <-> { A } e. Fin ) )
7 5 6 mpbiri 
 |-  ( N = { A } -> N e. Fin )
8 7 adantr 
 |-  ( ( N = { A } /\ A e. V ) -> N e. Fin )
9 8 3ad2ant2 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> N e. Fin )
10 simp1 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> R e. V )
11 simp3 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> M e. B )
12 eqid 
 |-  ( N Mat R ) = ( N Mat R )
13 1 12 2 3 4 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( T ` M ) = ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) )
14 9 10 11 13 syl3anc 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( T ` M ) = ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) )
15 id 
 |-  ( A e. V -> A e. V )
16 fvexd 
 |-  ( A e. V -> ( S ` ( A M A ) ) e. _V )
17 15 15 16 3jca 
 |-  ( A e. V -> ( A e. V /\ A e. V /\ ( S ` ( A M A ) ) e. _V ) )
18 17 adantl 
 |-  ( ( N = { A } /\ A e. V ) -> ( A e. V /\ A e. V /\ ( S ` ( A M A ) ) e. _V ) )
19 18 3ad2ant2 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( A e. V /\ A e. V /\ ( S ` ( A M A ) ) e. _V ) )
20 eqid 
 |-  ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) )
21 fvoveq1 
 |-  ( i = A -> ( S ` ( i M j ) ) = ( S ` ( A M j ) ) )
22 oveq2 
 |-  ( j = A -> ( A M j ) = ( A M A ) )
23 22 fveq2d 
 |-  ( j = A -> ( S ` ( A M j ) ) = ( S ` ( A M A ) ) )
24 20 21 23 mposn 
 |-  ( ( A e. V /\ A e. V /\ ( S ` ( A M A ) ) e. _V ) -> ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } )
25 19 24 syl 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } )
26 mpoeq12 
 |-  ( ( N = { A } /\ N = { A } ) -> ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) = ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) )
27 26 eqeq1d 
 |-  ( ( N = { A } /\ N = { A } ) -> ( ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } <-> ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } ) )
28 27 anidms 
 |-  ( N = { A } -> ( ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } <-> ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } ) )
29 28 adantr 
 |-  ( ( N = { A } /\ A e. V ) -> ( ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } <-> ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } ) )
30 29 3ad2ant2 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } <-> ( i e. { A } , j e. { A } |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } ) )
31 25 30 mpbird 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( i e. N , j e. N |-> ( S ` ( i M j ) ) ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } )
32 14 31 eqtrd 
 |-  ( ( R e. V /\ ( N = { A } /\ A e. V ) /\ M e. B ) -> ( T ` M ) = { <. <. A , A >. , ( S ` ( A M A ) ) >. } )