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 Fin R V I = m S x N , y N coe 1 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 Fin , r V m n ConstPolyMat r x n , y n coe 1 x m y 0
4 3 a1i N Fin R V cPolyMatToMat = n Fin , r V m n ConstPolyMat r x n , y n coe 1 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 coe 1 x m y 0 = coe 1 x m y 0
9 7 7 8 mpoeq123dv n = N r = R x n , y n coe 1 x m y 0 = x N , y N coe 1 x m y 0
10 6 9 mpteq12dv n = N r = R m n ConstPolyMat r x n , y n coe 1 x m y 0 = m S x N , y N coe 1 x m y 0
11 10 adantl N Fin R V n = N r = R m n ConstPolyMat r x n , y n coe 1 x m y 0 = m S x N , y N coe 1 x m y 0
12 simpl N Fin R V N Fin
13 elex R V R V
14 13 adantl N Fin R V R V
15 2 ovexi S V
16 mptexg S V m S x N , y N coe 1 x m y 0 V
17 15 16 mp1i N Fin R V m S x N , y N coe 1 x m y 0 V
18 4 11 12 14 17 ovmpod N Fin R V N cPolyMatToMat R = m S x N , y N coe 1 x m y 0
19 1 18 syl5eq N Fin R V I = m S x N , y N coe 1 x m y 0