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=NmatToPolyMatR
d1mat2pmat.b ⊢B=BaseNMatR
d1mat2pmat.p ⊢P=Poly1⁡R
d1mat2pmat.s ⊢S=algSc⁡P
Assertion d1mat2pmat ⊢R∈V∧N=A∧A∈V∧M∈B→T⁡M=AAS⁡AMA

Proof

Step Hyp Ref Expression
1 d1mat2pmat.t ⊢T=NmatToPolyMatR
2 d1mat2pmat.b ⊢B=BaseNMatR
3 d1mat2pmat.p ⊢P=Poly1⁡R
4 d1mat2pmat.s ⊢S=algSc⁡P
5 snfi ⊢A∈Fin
6 eleq1 ⊢N=A→N∈Fin↔A∈Fin
7 5 6 mpbiri ⊢N=A→N∈Fin
8 7 adantr ⊢N=A∧A∈V→N∈Fin
9 8 3ad2ant2 ⊢R∈V∧N=A∧A∈V∧M∈B→N∈Fin
10 simp1 ⊢R∈V∧N=A∧A∈V∧M∈B→R∈V
11 simp3 ⊢R∈V∧N=A∧A∈V∧M∈B→M∈B
12 eqid ⊢NMatR=NMatR
13 1 12 2 3 4 mat2pmatval ⊢N∈Fin∧R∈V∧M∈B→T⁡M=i∈N,j∈N⟼S⁡iMj
14 9 10 11 13 syl3anc ⊢R∈V∧N=A∧A∈V∧M∈B→T⁡M=i∈N,j∈N⟼S⁡iMj
15 id ⊢A∈V→A∈V
16 fvexd ⊢A∈V→S⁡AMA∈V
17 15 15 16 3jca ⊢A∈V→A∈V∧A∈V∧S⁡AMA∈V
18 17 adantl ⊢N=A∧A∈V→A∈V∧A∈V∧S⁡AMA∈V
19 18 3ad2ant2 ⊢R∈V∧N=A∧A∈V∧M∈B→A∈V∧A∈V∧S⁡AMA∈V
20 eqid ⊢i∈A,j∈A⟼S⁡iMj=i∈A,j∈A⟼S⁡iMj
21 fvoveq1 ⊢i=A→S⁡iMj=S⁡AMj
22 oveq2 ⊢j=A→AMj=AMA
23 22 fveq2d ⊢j=A→S⁡AMj=S⁡AMA
24 20 21 23 mposn ⊢A∈V∧A∈V∧S⁡AMA∈V→i∈A,j∈A⟼S⁡iMj=AAS⁡AMA
25 19 24 syl ⊢R∈V∧N=A∧A∈V∧M∈B→i∈A,j∈A⟼S⁡iMj=AAS⁡AMA
26 mpoeq12 ⊢N=A∧N=A→i∈N,j∈N⟼S⁡iMj=i∈A,j∈A⟼S⁡iMj
27 26 eqeq1d ⊢N=A∧N=A→i∈N,j∈N⟼S⁡iMj=AAS⁡AMA↔i∈A,j∈A⟼S⁡iMj=AAS⁡AMA
28 27 anidms ⊢N=A→i∈N,j∈N⟼S⁡iMj=AAS⁡AMA↔i∈A,j∈A⟼S⁡iMj=AAS⁡AMA
29 28 adantr ⊢N=A∧A∈V→i∈N,j∈N⟼S⁡iMj=AAS⁡AMA↔i∈A,j∈A⟼S⁡iMj=AAS⁡AMA
30 29 3ad2ant2 ⊢R∈V∧N=A∧A∈V∧M∈B→i∈N,j∈N⟼S⁡iMj=AAS⁡AMA↔i∈A,j∈A⟼S⁡iMj=AAS⁡AMA
31 25 30 mpbird ⊢R∈V∧N=A∧A∈V∧M∈B→i∈N,j∈N⟼S⁡iMj=AAS⁡AMA
32 14 31 eqtrd ⊢R∈V∧N=A∧A∈V∧M∈B→T⁡M=AAS⁡AMA