Metamath Proof Explorer

Theorem cpm2mfval

Description: Value of the inverse matrix transformation. (Contributed by AV, 14-Dec-2019)

		Ref	Expression
	Hypotheses	cpm2mfval.i	\|- I = ( N cPolyMatToMat R )
		cpm2mfval.s	\|- S = ( N ConstPolyMat R )
	Assertion	cpm2mfval	\|- ( ( N e. Fin /\ R e. V ) -> I = ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cpm2mfval.i	\|- I = ( N cPolyMatToMat R )
2		cpm2mfval.s	\|- S = ( N ConstPolyMat R )
3		df-cpmat2mat	\|- cPolyMatToMat = ( n e. Fin , r e. _V \|-> ( m e. ( n ConstPolyMat r ) \|-> ( x e. n , y e. n \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
4	3	a1i	\|- ( ( N e. Fin /\ R e. V ) -> cPolyMatToMat = ( n e. Fin , r e. _V \|-> ( m e. ( n ConstPolyMat r ) \|-> ( x e. n , y e. n \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) ) )
5		oveq12	\|- ( ( n = N /\ r = R ) -> ( n ConstPolyMat r ) = ( N ConstPolyMat R ) )
6	5 2	eqtr4di	\|- ( ( n = N /\ r = R ) -> ( n ConstPolyMat r ) = S )
7		simpl	\|- ( ( n = N /\ r = R ) -> n = N )
8		eqidd	\|- ( ( n = N /\ r = R ) -> ( ( coe1 ` ( x m y ) ) ` 0 ) = ( ( coe1 ` ( x m y ) ) ` 0 ) )
9	7 7 8	mpoeq123dv	\|- ( ( n = N /\ r = R ) -> ( x e. n , y e. n \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) = ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) )
10	6 9	mpteq12dv	\|- ( ( n = N /\ r = R ) -> ( m e. ( n ConstPolyMat r ) \|-> ( x e. n , y e. n \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) = ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
11	10	adantl	\|- ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> ( m e. ( n ConstPolyMat r ) \|-> ( x e. n , y e. n \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) = ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
12		simpl	\|- ( ( N e. Fin /\ R e. V ) -> N e. Fin )
13		elex	\|- ( R e. V -> R e. _V )
14	13	adantl	\|- ( ( N e. Fin /\ R e. V ) -> R e. _V )
15	2	ovexi	\|- S e. _V
16		mptexg	\|- ( S e. _V -> ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) e. _V )
17	15 16	mp1i	\|- ( ( N e. Fin /\ R e. V ) -> ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) e. _V )
18	4 11 12 14 17	ovmpod	\|- ( ( N e. Fin /\ R e. V ) -> ( N cPolyMatToMat R ) = ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )
19	1 18	syl5eq	\|- ( ( N e. Fin /\ R e. V ) -> I = ( m e. S \|-> ( x e. N , y e. N \|-> ( ( coe1 ` ( x m y ) ) ` 0 ) ) ) )