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 = ( N matToPolyMat R )
	mat2pmatfval.a	|- A = ( N Mat R )
	mat2pmatfval.b	|- B = ( Base ` A )
	mat2pmatfval.p	|- P = ( Poly1 ` R )
	mat2pmatfval.s	|- S = ( algSc ` P )
Assertion	mat2pmatvalel	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> ( X ( T ` M ) Y ) = ( S ` ( X M Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatfval.t	|- T = ( N matToPolyMat R )
2		mat2pmatfval.a	|- A = ( N Mat R )
3		mat2pmatfval.b	|- B = ( Base ` A )
4		mat2pmatfval.p	|- P = ( Poly1 ` R )
5		mat2pmatfval.s	|- S = ( algSc ` P )
6	1 2 3 4 5	mat2pmatval	|- ( ( N e. Fin /\ R e. V /\ M e. B ) -> ( T ` M ) = ( x e. N , y e. N |-> ( S ` ( x M y ) ) ) )
7	6	adantr	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> ( T ` M ) = ( x e. N , y e. N |-> ( S ` ( x M y ) ) ) )
8		oveq12	|- ( ( x = X /\ y = Y ) -> ( x M y ) = ( X M Y ) )
9	8	fveq2d	|- ( ( x = X /\ y = Y ) -> ( S ` ( x M y ) ) = ( S ` ( X M Y ) ) )
10	9	adantl	|- ( ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) /\ ( x = X /\ y = Y ) ) -> ( S ` ( x M y ) ) = ( S ` ( X M Y ) ) )
11		simprl	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> X e. N )
12		simprr	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> Y e. N )
13		fvexd	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> ( S ` ( X M Y ) ) e. _V )
14	7 10 11 12 13	ovmpod	|- ( ( ( N e. Fin /\ R e. V /\ M e. B ) /\ ( X e. N /\ Y e. N ) ) -> ( X ( T ` M ) Y ) = ( S ` ( X M Y ) ) )