Metamath Proof Explorer


Theorem mat2pmatvalel

Description: A (matrix) element of the result of a matrix transformation. (Contributed by AV, 31-Jul-2019)

Ref Expression
Hypotheses mat2pmatfval.t T=NmatToPolyMatR
mat2pmatfval.a A=NMatR
mat2pmatfval.b B=BaseA
mat2pmatfval.p P=Poly1R
mat2pmatfval.s S=algScP
Assertion mat2pmatvalel NFinRVMBXNYNXTMY=SXMY

Proof

Step Hyp Ref Expression
1 mat2pmatfval.t T=NmatToPolyMatR
2 mat2pmatfval.a A=NMatR
3 mat2pmatfval.b B=BaseA
4 mat2pmatfval.p P=Poly1R
5 mat2pmatfval.s S=algScP
6 1 2 3 4 5 mat2pmatval NFinRVMBTM=xN,yNSxMy
7 6 adantr NFinRVMBXNYNTM=xN,yNSxMy
8 oveq12 x=Xy=YxMy=XMY
9 8 fveq2d x=Xy=YSxMy=SXMY
10 9 adantl NFinRVMBXNYNx=Xy=YSxMy=SXMY
11 simprl NFinRVMBXNYNXN
12 simprr NFinRVMBXNYNYN
13 fvexd NFinRVMBXNYNSXMYV
14 7 10 11 12 13 ovmpod NFinRVMBXNYNXTMY=SXMY